There is a growing need to introduce and develop computational models capable of faithfully modelling systems whose behaviour combines synchrony with asynchrony in a variety of complicated ways. Examples of such real-life systems can be found from VLSI har dware GALS systems to systems of cells within which biochemical reactions happen in synchronised pulses. One way of capturing the resulting intricate behaviours is to use Petri nets with localities where transitions are partitioned into disjoint groups within which execution is synchronous and maximally concurrent. In this paper, we generalise this type of nets by allowing each transition to belong to several localities. Moreover, we define this extension in a generic way for all classes of nets defined by net-types. We show that Petri nets with overlapping localit ies are an instance of the general model of nets with policies. Thanks to this fact, it is possible to automatically construct nets with localities from behavioural specifications given in terms of finite step transition systems. After that we outline our initial ideas concerning net synthesis when the association of transition to localities is not given and has to be determined by the synthesis algorithm.
In the formal modelling of computational systems there is a growing need to
faithfully capture real-life systems exhibiting behaviour which can be described
as ‘globally asynchronous locally (maximally) synchronous’ (GALS). E xamples
can be found in hardware design, where a VLSI chip may contain multiple clocks
responsible for synchronising different subsets of gates [
To explain the basic idea behind nets with overlapping localities, let us consider an array of n transitions ti (0 ≤ i ≤ n − 1) which are arranged in a circular manner, i.e., ti is adjacent to t(i+n−1) mod n and t(i+1) mod n which form its ‘neighbourhood’. Each of the transitions belongs to so me subsystem which is left unspecified. What is important from our point of view is that to be executed, ti needs, in addition to being enabled by its subsystem, to receive an external stimulus (e.g., an electric charge when transitions represent biological cells) which then spreads to its neighbourhood forcing the execution of transition t(i+n−1) mod n and t(i+1) mod n provided they are enabled by their subsystems. Thus, stimulating a transition amounts to stimulating its neighbourhood, and neighbourhoods can overlap which means that a given transition can be triggered in possibly many ways. To model such a scenario in a direct way we can use a Petri net augmented with a locality mapping ℓ such that ℓ(ti) = { (i + n − 1) mod n, i, (i + 1) mod n} , where each integer represents a distinct locality, and assuming that a transition may be executed only if it belongs to some stimulated neighbourhood. For example, if all the transitions ti are enabled by their subsystems, then the following are examples of legal steps of the Petri net: { t2, t3, t4} { t2, t3, t4, t5} { t2, t3, t4, t5, t8, t9, t10} t3 stimulated t3 and t4 stimulated t3, t4 and t9 stimulated and two examples of illegal steps are { t2, t3} and { t2, t3, t4, t6} .
In the abstract capture of the underlying mechanisms like that above, we will demand that an executed transition belongs to at least one saturated locality, i.e., it is not possible to additionally execute any more transitions associated with that locality.
Rather than introducing nets with overlapping localities for PT-nets or their
extensions, we will move straight to the general case of τ -nets [
After introducing the new model of nets, we turn our attention to their
automatic synthesis from behavioural specifications given in terms of step transition
systems. Since τ -nets with localities are an instance of a more general scheme
treated in [
The results in [
In this section, we recall some basic notions concerning τ -nets, policies and the
synthesis problem as presented in [
An abelian monoid is a set S with a commutative and associative binary (composition) operation + on S, and a neutral element 0. The monoid element resulting from composing n copies of s ∈ S will be denoted by n · s, and so 0 = 0 · s and s = 1 · s.
A specific abelian monoid, hT i, is the free abelian monoid generated by a set (of transitions) T . It can be seen as the set of all the multisets over T . We will use α, β, γ, . . . to range over the elements of hT i. Moreover, for all t ∈ T and α ∈ hT i, we will use α(t) to denote the multiplicity of t in α. We will write t ∈ α whenever α(t) > 0, and denote by supp(α) the set of all t ∈ α. The size of α is given by | α| = Pt∈T α(t).
We denote α ≤ β whenever α(t) ≤ β(t) for all t ∈ T (and α < β if α ≤ β and α 6= β). For X ⊆ hT i, we denote by max≤(X) the set of all ≤-maximal elements of X, and by min≤(X) the set of all non-empty ≤-minimal elements of X.
If T ′ ⊆ T then α| T ′ is a multiset α′ such that α′(t) = α(t) if t ∈ T ′ and otherwise α′(t) = 0. The sum of two multisets, α and β, will be denoted by α + β, and a singleton multiset { t} simply by t.
A transition system over an abelian monoid S is a triple (Q, S, δ) such that Q is a set of states, and δ : Q × S → Q a partial transition function1 satisfying δ(q, 0) = q for all q ∈ Q. An initialised transition system T =df (Q, S, δ, q0) has in addition an initial state q0 ∈ Q from which every other state is reachable. For every state q of a (non-initialised or initialised) transition system TS , enbld TS (q) =df { s ∈ S | δ(q, s) is defined} .
Initialised transition systems T over free abelian monoids — called step transition systems — will represent concurrent behaviours of Petri nets. Noninitialised transition systems τ over arbitrary abelian monoids — called net-types — will provide ways to define various classes of nets. Throughout th e paper, we will assume that: – T is a fixed finite set (of net transitions); – Loc is a fixed finite set (of net transitions’ localities); 1 Transition functions and net transitions are unrelated notions. – T = (Q, S, δ, q0) is a fixed step transition system over S = hT i. – τ = (Q, S, Δ) is a fixed net-type over an abelian monoid S. In this paper, we will assume that τ is substep closed which means that, for every state q ∈ Q, if α + β ∈ enbld τ (q) then also α ∈ enbld τ (q). This will imply that substeps of resource enabled steps are also resource enabled which is a condition usually satisfied in practice.
The net-type defines a class of nets, by specifying the values (mar kings) that can be stored in net places (Q), the operations and tests (inscriptions on the arcs) that a net transition may perform on these values (S), and the enabling condition and the newly generated values for steps of transitions (Δ). Definition 1 (τ -net). A τ -net system is a tuple N =df (P, T , F, M0), where P and T are disjoint sets of places and transitions, respectively; F : (P × T ) → S is a flow mapping; and M0 : P → Q is an initial marking.
In general, any mapping M : P → Q is a marking. For each place p ∈ P and step α ∈ hT i, F (p, α) =df Pt∈T α(t) · F (p, t).
Definition 2 (step semantics). Given a τ -net system N = (P, T , F, M0), a step α ∈ hT i is (resource) enabled at a marking M if, for every place p ∈ P :
F (p, α) ∈ enbld τ (M (p)) .
M ′(p) =df Δ(M (p), F (p, α)) .
Step firing policies are means of controlling and constraining the huge number of execution paths resulting from the concurrent nature of a majority of computing systems.
Let Xτ be the family of all sets of steps enabled at some reachable marking M of some τ -net N with the set of transitions T .
Definition 3 (bounded step firing policy). A bounded step firing policy for τ -nets over hT i is given by a control disabled steps mapping cds : 2hT i → 2hT i\{ 0} such that, for all X ⊆ hT i, the following hold: 1. If X is infinite then cds (X) = ∅.
We will now discuss further step firing policies and their effect on net behaviour. M are: as in N .
τ -nets over hT i. A tuple N P =df (P, T , F, M0, cds) is a τ -net system with policy if N = (P, T , F, M0) is a τ -net and the (control) enabled steps of N P at a marking
Enbld N P (M ) =df enbld N (M ) \ cds(enbld N (M )).
Moreover, let enbld N P (M ) =df enbld N
(M ) be the set of resource enabled steps of
N P , and call it concurrent reachability graph of N P .
In this paper our concern will be to find a general solution to the synthesis
problem for τ -nets with localities. Since they are special kinds of τ -nets with
policies we will be able to use the theory developed for those nets in [
Let T be a given finite step transition system. Provide necessary and sufficient conditions for T to be realised by some τ -net system with policy N P (i.e., T
∼= CRG(N P ) where ∼= is transition system isomorphism
The solution of the synthesis problem is based on the idea of a region of a transition system.
Definition 5 (τ -region). A τ -region of T is a pair of mappings (σ : Q → Q , η : hT i → S) such that η is a morphism of monoids and, for all q ∈ Q and α ∈ enbld T (q): η(α) ∈ enbld τ (σ(q)) and Δ(σ(q), η(α)) = σ(δ(q, α)) . η(α) ∈ enbld τ (σ(q)), for all τ -regions (σ, η) of T .
We then have the following general result from [
axiom i: state separation axiom ii: forward closure with policies that σ(q) 6= σ(r).
For any pair of states q 6= r of T , there is a τ -region (σ, η) of T such For every state q of T , enbld T (q) = enbld T ,τ (q) \ cds(enbld T ,τ (q)). ⊔⊓ of T , and T ⊆ hT i).
A solution to the synthesis problem is obtained if one can compute a finite
set WR of τ -regions of T witnessing the satisfaction of all instances of axioms i
and ii [
τ n-ets with localities We will now introduce a general class of Petri nets with localities, based on a specific class of control disabled steps mappings. the induced control disabled steps mapping is
A locality mapping for the transition set T is any ℓ : T → 2Loc such that ℓ(t) 6= ∅ for all t ∈ T . (Below we will denote l ∈ ℓ(α), for every step α and a locality l ∈ Loc, whenever there is a transition t ∈ α such that l ∈ ℓ(t).) Then cdsℓ : 2hT i → 2hT i\{ 0} such that, for all X ⊆ hT i:
∅ cdsℓ(X) =df { α ∈ X | ∃ t ∈ α ∀l ∈ ℓ(t) ∃α + β ∈ X : l ∈ ℓ(β)} if X is finite otherwise .
cdsℓ(X) ⊆ Y and α ∈ cdsℓ(X) ∩ Y , then α ∈ cdsℓ(Y ).
Proof. All we need to prove is that if X ∈ Xτ is finite and Y ⊆ X and X \
We first observe that max≤(X) ∩ cdsℓ(X) = ∅ and so max≤(X) ⊆ X \ cdsℓ(X) ⊆ Y . Then we observe that since X is finite and α ∈ cds ℓ(X), there is t ∈ α such that for all l ∈ ℓ(t) there exists α + β ∈ max≤(X) ⊆ Y satisfying l ∈ ℓ(β). This and the fact that Y is finite (as Y ⊆ X) means that α ∈ cdsℓ(Y ). axiom ii are satisfied for T with policy cds = cdsℓ.
We will call a τ -net system with a policy cdsℓ a τ /ℓ-net system (or τ -net with localities). Moreover, we will call T a τ /ℓ-transition system if axiom i and every t ∈ α there is l ∈ ℓ(t) such that:
enbld N P (M ) is finite. A step α ∈ enbld N P (M ) belongs to Enbld N P (M ) iff for
l ∈ ℓ(t′) =⇒ α + t′ ∈/ enbld N P (M ) , for every transition t′. γ ≤ δ and δ ∈ enbld N P (M ) together imply γ ∈ enbld N P (M ). Proof. Follows from max≤(enbld N P (M )) ⊆ Enbld N P (M ), and the fact that ⊔⊓ ⊔⊓
We obtain an immediate solution to the synthesis problem for τ /ℓ-nets. tem iff T is a τ /ℓ-transition system.
Proof. Follows from Theorem 1 and Proposition 1. ⊔⊓
The synthesis problem for PT-nets and EN-systems with localities (a nd with
or without inhibitor and read arcs) have been investigated in [
As to the effective construction of synthesised net, it has been demonstrated
in [
Finally, it is interesting to observe that in the (previously considered) case of non-overlapping localities, cdsℓ can be defined through a pre-order on steps. This is no longer the case for the general locality mappings. 4
Towards synthesis with unknown localities The synthesis result presented in the previous section was obtained assuming that the locality mapping was given. However, in practice such a mapping might be unknown (or partially known), and part of the outcome of a successful synthesis procedure would be a suitable (or good ) locality mapping. Clearly, what really matters in a locality mapping is the identification of (possibly overlapping) clusters of transitions, each cluster containing all transitions sharing a locality. Since there are only finitely many clusters, there are also finitely many non-equivalent locality mappings, and the synthesis procedure cou ld simply enumerate them and then check one-by-one using Theorem 2. This, ho wever, would be highly impractical as the number of clusters is exponential in the number of transitions. We will now present some initial ideas and results aimed at reducing the number of checks. τ -net with localities (see axiom ii and Theorem 2).
From now on we will assume that T is finite. We will also assume that we have checked that, for every state q of T , the set of steps enbld T ,τ (q) is finite; otherwise T could not be isomorphic to the concurrent reachability graph of any
In the rest of this section, for every state q of T and locality mappings ℓ, ℓ′: – allSteps q is the set of all steps labelling arcs outgoing from q. – minStepsq is the set of all non-empty steps α ∈ allSteps q for which there is no non-empty β ∈ allSteps q such that β < α. – Tq is the set of all net transitions occurring in the steps of allStepsq. – clustersℓq is the set of all sets { t ∈ Tq | l ∈ ℓ(t)} , for every l ∈ ℓ(Tq). – ℓ and ℓ′ are node-consistent if clustersℓr = clustersℓr′ , for every state r of T .
A general result concerning locality mappings is that they are equally suitable for being good locality mapping whenever they induce the same clusters of colocated transitions in each individual node of the step transition system. is τ /ℓ-transition system iff T is τ /ℓ′-transition system.
Proof. Suppose that T is τ /ℓ-transition system. First we notice that axiom i does not depend on the locality mapping. For axiom ii and ℓ′ it suffices to show that, for each state q of T : cdsℓ(enbld T ,τ (q)) = cdsℓ′ (enbld T ,τ (q)) . (1) ⊔⊓ are node-consistent, (1) holds.
We observe that the steps from enbld T ,τ (q) have transitions belonging to Tq (as the maximal steps in enbld T ,τ (q) never belong to cdsℓ(enbld T ,τ (q)) and axiom ii holds for ℓ), and thus according to the definition of cdsℓ(X) the influence of each locality l ∈ ℓ(Tq) and l′ ∈ ℓ′(Tq) can be accurately represented by the clusters { t ∈ Tq | l ∈ ℓ(t)} and { t′ ∈ Tq | l′ ∈ ℓ′(t′)} , respectively. Hence, since ℓ and ℓ′
As a consequence, a good locality mapping can be arbitrarily modified to yield another good locality mapping as long as the two mappings are nodeconsistent (there is no need to re-check the two axioms involved in T heorem 2). This should allow one to search for an optimal good locality mapping starting from some initial choice (for example, one might prefer to have as few localities per transition as possible). subsets of Tq so that C1 ∪ . . . ∪ Ck = Tq and:
The construction of a good locality mapping could be seen as modular process, in the following way. First, separately for each state q, we produce a list of possible cluster-sets of transitions in Tq induced by hypothetical good locality mappings. Each such cluster-set clSet =df { C1, . . . , Ck} is composed of non-empty enbld T (q) = enbld T ,τ (q) \ cdsclSet (enbld T ,τ (q)) where
cdsclSet (X) =df { α ∈ X | ∃ t ∈ α ∀i ≤ k : (t ∈ Ci ⇒ ∃t′ ∈ Ci : α + t′ ∈ X)} .
Similarly, one may produce, for each state q, a characterisation of inadmissible
clustering of transitions. We can then select different cluster-set s (one per each
state of the step transition system) and check whether combining them together
yields a good locality mapping. Such a procedure was used in [
The search for a good locality mapping outlined above can be improved if one looks for solutions in a specific class of nets, or if the locality mapping is partially known or constrained (for example, that two specific transitions cannot share a locality). 4.1
Localised conflicts Intuitively, localities and conflicts may have opposite effects on step enabledness. Whereas joining two localities may reduce the number of control enabled steps, adding a conflict between transitions with shared localities may turn a non-enabled step into a control enabled one. It is therefore inter esting what simplifications, if any, one might obtain if conflicts were constrained to exist between transitions sharing localities.
In the paper [
To start with, the set of saturated localities of a step α which is resource enabled at some marking M of a τ /ℓ-net N P is defined as: satlocalities M (α) =df { l ∈ ℓ(α) | ¬ ∃ α + β ∈ enbld N P (M ) : l ∈ ℓ(β)} .
Intuitively, saturated localities are those which have been ‘active’ d uring the execution of a step α. It is immediate to see that if α ∈ Enbld N P (M ) then, for all t ∈ α:
satlocalities M (α) ∩ ℓ(t) 6= ∅ .
Moreover, the above intersection may contain more than one active localities which are ‘responsible’ for the execution of transition t. At the level of potential clusters of a step transition system (i.e., groups of transitions which share a locality), we can define saturated clusters in a state q as:
satclustersq(α) =df { C ⊆ Tq | α| C 6= ∅ ∧ ∀ α + β ∈ allSteps q : β| C = ∅} . Note that if T is the concurrent reachability graph of a τ /ℓ-net N P, and M is a reachable marking of N P, then: { { t ∈ TM | l ∈ ℓ(t)} |
l ∈ satlocalities M (α) } ⊆ satclustersM (α) .
The following definition is our first attempt to generalise the notion of nets
with localised conflicts investigated in [
Definition 6 (localised conflicts). A τ /ℓ-net system N P has partially localised conflicts if for all reachable markings M and non-empty steps α belonging to enbld N P (M ),
t ∈ enbld N P (M ) and α + t ∈/ enbld N P (M ) implies satlocalities M (α) 6= ∅ and
∀ l ∈ ℓ(t) ∩ satlocalities M (α) : α| l + t ∈/ enbld N P (M ) .
Intuitively, if there is a (global) conflict between a transition and a step, then this conflict can also be witnessed locally. We will now be concerned with the synthesis problem aimed at constructing τ /ℓ-net systems with partially localised conflicts. and M be its reachable marking.
Proof. Suppose that el∈ satlocalities M (α) and α| el ∈/ Enbld N P (M ).
Since α | el ≤ α ∈ Enbld N P (M ), we have α | el ∈ enbld N P (M ). Hence there is et ∈ α| el such that, for all l ∈ ℓ(et), there is α| el + t′ ∈ enbld N P (M ) with l ∈ ℓ(t′). In particular, since el ∈ ℓ(et), there is α| el + bt ∈ enbld N P (M ) such that el ∈ ℓ(bt). Hence bt ∈ enbld N P
(M ), and so we can use Definition 6 to infer that α + bt ∈ enbld N P (M ), producing a contradiction with el∈ satlocalities M (α). ⊔⊓
Thus in terms of selecting clusters in the construction outlined in the previous satclustersq(α), it must be the case that α| C ∈ allSteps q. section, if C has been selected at a state q then, for every α such that C ∈ and M be its reachable marking.
If α ∈ Enbld NmiPn (M ) then α = α| l, for all l ∈ satlocalities M (α).
is a minimal non-empty step in Enbld N P (M ), we have α = α| l.
Proof. By Proposition 4, we have α| l ∈ Enbld N P (M ), and by definition of α| l, we have that α| l ≤ α. Moreover, α| l ≤ α and α| l 6= ∅ (as l ∈ ℓ(α)). Hence, as α ⊔⊓
Thus in terms of selecting clusters in the construction outlined in the previous that C ∈ satclustersq(α), it must be the case that α| C = α. section, if C has been selected at a state q then, for every α ∈ minStepsq such
We will now present a series of results which can all be useful in the selection of clusters in the construction outlined in the previous section. and M be its reachable marking. Then, for all α ∈ Enbld NmiPn (M ):
\{ ℓ(t) | t ∈ α} . l ∈ ℓ(t), for all t ∈ α.
Proof. Let l ∈ satlocalities M (α). By Proposition 5, we have α = α| l. Hence ⊔⊓ M be its reachable marking. Then, for all α ∈ Enbld NmiPn (M ):
\{ ℓ(t) | t ∈ α} 6 = ∅ . satlocalities M (α) 6= ∅ and the result follows from Proposition 6.
(M ), satlocalities M (α)∩ℓ(t) 6= ∅, for every t ∈ α. Hence We will now need the following auxiliary fact. and M satlocalities M (α) ⊆ satlocalities M (β).
From l ∈ satlocalities M (α) we have that l ∈ ℓ(α) and: ∀ t : l ∈ ℓ(t) =⇒
α + t ∈/ enbld N P (M ) . l ∈ ℓ(et) ∧
β + et ∈ enbld N P (M ) . et such that:
From l ∈/ satlocalities M (β) we have that either l ∈/ ℓ(β), or l ∈ ℓ(β) and there is (2) (3) ⊔⊓ contradiction with α + et ≤ β + et.
Only the latter is possible, because l ∈ ℓ(α) and α ≤ β. From (2) and (3) we have that α + et ∈/ enbld N P (M ) and β + et ∈ enbld N P (M ), which produces a Then α| el ∈ Enbld NmiPn (M ).
and M be its reachable marking. Moreover, let α ∈ Enbld N P (M ) and el ∈ satlocalities M (α) be such that α| l 6< α| el, for all l ∈ satlocalities M (α) \ { el} . α
| el ≤ α, it follows that Proof. From Proposition 4 we have that α| el ∈ Enbld N P non-empty step β ∈ Enbld N P (M ) such that β < α| el. From Proposition 7 and (M ). Suppose there is a satlocalities M (β) ⊆ satlocalities M (α| el) ⊆ satlocalities M (α) .
As β 6= ∅ and β ∈ Enbld N P (M ) we obtain
satlocalities M (β) 6= ∅ .
We have that el ∈/ satlocalities M (β) as β < α| el. Let bl ∈ satlocalities M (β). Since satlocalities M (β) ⊆ satlocalities M (α), we have bl ∈ satlocalities M (α). Hence, by Proposition 4, α| bl ∈ Enbld N P (M ). By the assumption we made, α| bl 6< α| el as bl 6= el. So, there is bt such that α| bl(bt) ≥ α| el(bt) > β(bt), producing a contradiction
Let N P be a τ /ℓ-net system with partially localised conflicts and M be its with bl∈ satlocalities M (β). reachable marking. Then:
maxind tM =df max{ α(t) | α ∈ Enbld N P (M )} , for every net transition t which is resource enabled at M . following holds: Proposition 9. Let N P be a τ /ℓ-net system with partially localised conflicts and M be its reachable marking. Moreover, let t and u be distinct transitions which are resource enabled at M and share a locality el. Then exactly one of the – There is no step α ∈ Enbld N P (M ) such that el∈ satlocalities M (α) and (4) ⊔⊓ maxind tM + maxind uM = α(t) + α(u) – There is α ∈ Enbld NmiPn (M ) such that t, u ∈ α.
and, for all l ∈ satlocalities M (α) \ { el} , we have α| l 6< α| el. we obtain that α| el ∈ Enbld NmiPn (M ).
Proof. We have el ∈ ℓ(t) ∩ ℓ(u). Suppose that there is α ∈ Enbld N P (M ) such that (4) holds and el ∈ satlocalities M (α) and for all l ∈ satlocalities M (α) \ { el} , α| l 6< α| l. Since t and u are resource enabled at M and (4) holds, we have e α(t) ≥ 1 and α(u) ≥ 1. On the other hand, el ∈ ℓ(t) ∩ ℓ(u). Then, t, u ∈ α| el. We can see that all the conditions of Proposition 8 are satisfied for α and el, and so in Proposition 6, i.e., there can be α ∈ Enbld NmiPn (M ) such that: Unique and minimal step covers It is not possible to reverse the inclusion \{ ℓ(t) | t ∈ α} ⊆ satlocalities M (α) belongs to Enbld NmiPn (M0) yet: does no hold. As an example, we can take a PT-net with two concurre nt transitions, a and b, each having one pre-place marked with a single token and no post-places, satisfying ℓ(a) = { l, l′} and ℓ(b) = { l} . Then the step α = { a} \{ ℓ(t) | t ∈ α} = { l, l′} 6⊆ { l′} = satlocalities M0 (α) .
Looking at the last example, one can make a comment about the advantages of allowing a single transition to have more than one locality. In such a situation, different localities can define different modes of engagement/co-op eration. For transition a, the locality l could be interpreted as defining a ‘co-operative mode’, while l′ a ‘self-sufficient’ mode. In this way, some localities may force big sets of transitions to work in synchrony, while other localities may allow smaller sets to be synchronised, or even single transitions to be executed alone. Intuitively, we can model different ‘circles of co-operations’ for net transitions.
If we take again the last two transitions, and this time consider the step { a, b} , then one may observe that there is certain ambiguity as to which localities have We will now investigate the role of such sets of localities. been active during its execution, as both L = { l} and L′ = { l, l′} could be taken.
such that:
supp(α) = [{ supp(α| l) | l ∈ L} , and it is minimal if no proper subset of L is a locality cover of α. Moreover, a minimal locality cover L is unique if there is no other minimal locality cover L′ for α such that { α| l | l ∈ L} = { α| l′ | l′ ∈ L′} . cover for α = { a} as L′ = { l′} is also a cover.
Example 1. Let ℓ(a) = { l, l′} and ℓ(b) = { l} . Then L = { l, l′} is not a minimal α = { a, b} , L = { l} and L′ = { l′} , which are not unique.
Example 2. Let ℓ(a) = ℓ(b) = { l, l′} . Then there are two minimal covers for unique cover for α = { a, b, c} .
Example 3. Let ℓ(a) = { l, l′} , ℓ(b) = { l} and ℓ(c) = { l′} . Then L = { l, l′} is a { l3, l4} .
Example 4. Let ℓ(a) = { l1, l3} , ℓ(b) = { l1, l4} , ℓ(c) = { l2, l3} and ℓ(d) = { l2, l4} . Then α = { a, b, c, d} has two unique minimal covers: L = { l1, l2} and L′ =
Equipped with the concept of a unique minimal cover, we can reverse the inclusion in Proposition 6. are unique, then:
and M be its reachable marking. If α ∈ Enbld NmiPn (M ) and all its minimal covers satlocalities M (α) = \{ ℓ(t) | t ∈ α} . α
| bl ∈ Enbld N P (M ).
Proposition 6. Suppose that el∈ T{ ℓ(t) | t ∈ α} \ satlocalities M (α). Proof. We need to show the (⊇) inclusion as the opposite one follows from
From el ∈ T{ ℓ(t) | t ∈ α} we have α = α| el. Since α ∈ Enbld NmiPn (M ), we have satlocalities M (α) ∩ ℓ(t) 6= ∅, for all t ∈ α. Suppose bl ∈ satlocalities M (α) ∩ ℓ(et), for some et ∈ α. Notice that bl 6= el as el ∈/ satlocalities M (α). From Proposition 4,
We have α| bl ≤ α = α| el. We cannot have α| bl = α| el, because then both { el} and { bl} would be two different minimal covers for α, and so neither of them be unique. Hence α| l < α, producing a contradiction with the minimality of α. b ⊔⊓ C ∈ satclustersq(α) iff α| C = α.
Thus in terms of selecting clusters in the construction outlined earlier on, if C has been selected at a state q then, for every α ∈ minStepsq, we must have 5
In this paper, we only initiated the investigation of intricate relationships between localities, conflicts and step covers. In the future research we plan to develop stronger results on this topic, aiming at an efficient synthesis procedure of τ -nets with localities with unknown locality mappings. Acknowledgement We would like to thank Piotr Chrzastowski-Wachtel for his suggestion to investigate nets with overlapping localities. We are also grateful to the reviewers for their detailed and helpful comments. This research was supported by the Rae&Epsrc Davac Verdad projects, and Nsfc Grants 60910004 and 2010CB328102.