=Paper=
{{Paper
|id=None
|storemode=property
|title=Synthesis of General Petri Nets with Localities
|pdfUrl=https://ceur-ws.org/Vol-827/13_MaciejKoutny_article.pdf
|volume=Vol-827
|dblpUrl=https://dblp.org/rec/conf/acsd/KoutnyP10
}}
==Synthesis of General Petri Nets with Localities==
https://ceur-ws.org/Vol-827/13_MaciejKoutny_article.pdf
Synthesis of General Petri Nets with Localities
Maciej Koutny and Marta Pietkiewicz-Koutny
School of Computing Science
Newcastle University
Newcastle upon Tyne, NE1 7RU
United Kingdom
{maciej.koutny,marta.koutny}@newcastle.ac.uk
Abstract. There is a growing need to introduce and develop computa-
tional 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 hardware
GALS systems to systems of cells within which biochemical reactions
happen in synchronised pulses. One way of capturing the resulting intri-
cate 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 localities are an in-
stance 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.
Keywords: theory of concurrency, Petri nets, localities, analysis and
synthesis, step sequence semantics, conflict, theory of regions, transition
systems.
1 Introduction
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). Examples
can be found in hardware design, where a VLSI chip may contain multiple clocks
responsible for synchronising different subsets of gates [6], and in biologically
inspired membrane systems representing cells within which biochemical reac-
tions happen in synchronised pulses [15]. To capture such systems in a formal
manner, [9] introduced Place/Transition-nets with localities (PTL-nets), where
each locality identifies a distinct set of transitions which must be executed syn-
chronously, i.e., in a maximally concurrent manner (akin to local maximal con-
currency). The expressiveness of PTL-nets (even after enhancing them with
Recent Advances in Petri Nets and Concurrency, S. Donatelli, J. Kleijn, R.J. Machado, J.M. Fernandes
(eds.), CEUR Workshop Proceedings, ISSN 1613-0073, Jan/2012, pp. 161–174.
162 Petri Nets & Concurrency Koutny and Pietkiewicz-Koutny
inhibitor and activator arcs in [8]) was constrained by the fact that each transi-
tion belonged to a unique locality, and so the localities were all non-overlapping.
In this paper, we drop this restriction aiming at a net model which we believe
should provide a greater scope for faithful (or direct) modelling features im-
plied by the complex nature of, for example, modern VLSI systems or biological
systems.
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 some
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 neigh-
bourhood 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 neighbour-
hoods 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 repre-
sents 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 } t3 stimulated
{t2 , t3 , t4 , t5 } t3 and t4 stimulated
{t2 , t3 , t4 , t5 , t8 , t9 , t10 } 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 [2] which encap-
sulate a majority of Petri net classes for which the synthesis problem has been
investigated. In fact, the task of defining τ -nets with (potentially) overlapping
localities is straightforward, as the resulting model of τ -nets with localities turns
out to be an instance of the general framework of τ -nets with policies introduced
in [4].
After introducing the new model of nets, we turn our attention to their auto-
matic synthesis from behavioural specifications given in terms of step transition
Synthesis of PNs with localities Petri Nets & Concurrency – 163
systems. Since τ -nets with localities are an instance of a more general scheme
treated in [4], we directly import synthesis results presented there which are
based on the regions of a transition system studied in other contexts, in partic-
ular, in [1–3, 7, 13, 14, 16, 10, 11].
The results in [4] assume that policies are given which, in our case, means
that we know exactly the localities associated with all the net transitions. This
may be difficult to guarantee in practice, and so in the second part of the paper
we outline our initial ideas concerning net synthesis when this is not the case,
extending our previous work on non-overlapping localities reported in [12].
2 Preliminaries
In this section, we recall some basic notions concerning τ -nets, policies and the
synthesis problem as presented in [4].
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) > P0, and denote by supp(α) the set of all t ∈ α. The size of α is
given by |α| = t∈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 satisfy-
df
ing δ(q, 0) = q for all q ∈ Q. An initialised transition system T = (Q, S, δ, q0 )
has in addition an initial state q0 ∈ Q from which every other state is reach-
able. For every state q of a (non-initialised or initialised) transition system TS ,
df
enbld TS (q) = {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. Non-
initialised transition systems τ over arbitrary abelian monoids — called net-types
— will provide ways to define various classes of nets. Throughout the 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.
164 Petri Nets & Concurrency Koutny and Pietkiewicz-Koutny
– 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 (markings) 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 (∆).
df
Definition 1 (τ -net). A τ -net system is a tuple N = (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
df P
step α ∈ hT i, F (p, α) = t∈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)) .
We denote this by α ∈ enbld N (M ). The firing of such a step produces the mark-
ing M ′ such that, for every p ∈ P :
M ′ (p) = ∆(M (p), F (p, α)) .
df
Step firing policies are means of controlling and constraining the huge num-
ber 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) = ∅.
2. If X is finite then, for every Y ⊆ X:
(a) cds(X) ⊆ X;
(b) cds(Y ) ⊆ cds(X); and
(c) X ∈ Xτ and X \ cds(X) ⊆ Y imply cds(X) ∩ Y ⊆ cds(Y ).
We will now discuss further step firing policies and their effect on net be-
haviour.
Synthesis of PNs with localities Petri Nets & Concurrency – 165
Definition 4 (τ -net with policy). Let cds be a bounded step firing policy for
df
τ -nets over hT i. A tuple N P = (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
M are:
df
Enbld N P (M ) = enbld N (M ) \ cds(enbld N (M )).
df
Moreover, let enbld N P (M ) = enbld N (M ) be the set of resource enabled steps of
N P at marking M . The effect of executions of enabled steps in N P is the same
as in N .
We will denote by CRG(N P) the step transition system with the initial state
M0 formed by firing inductively from M0 all possible control 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 [4]. By
solving a synthesis problem we mean finding a procedure for building a net of
a certain class with the desired behaviour (in our case, concurrent reachability
graph). In our case the problem can be defined as follows.
synthesis problem
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
preserving the initial states and transition labels).
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, α)) .
For every state q of Q, we denote by enbld T ,τ (q) the set of all steps α such that
η(α) ∈ enbld τ (σ(q)), for all τ -regions (σ, η) of T .
We then have the following general result from [4].
Theorem 1. T can be realised by a τ -net system with a (bounded step firing)
policy cds iff the following two regional axioms are satisfied:
axiom i: state separation
For any pair of states q 6= r of T , there is a τ -region (σ, η) of T such
that σ(q) 6= σ(r).
axiom ii: forward closure with policies
For every state q of T , enbld T (q) = enbld T ,τ (q) \ cds(enbld T ,τ (q)). ⊓
⊔
166 Petri Nets & Concurrency Koutny and Pietkiewicz-Koutny
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 [5]. A suitable τ -net system with policy cds, N P WR = (P, T, F, M0 , cds),
can be then constructed with P = WR and, for any place p = (σ, η) in P and
every t ∈ T , F (p, t) = η(t) and M0 (p) = σ(q0 ) (recall that q0 is the initial state
of T , and T ⊆ hT i).
3 τ -nets with localities
We will now introduce a general class of Petri nets with localities, based on a
specific class of control disabled steps mappings.
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
the induced control disabled steps mapping is
cds ℓ : 2hT i → 2hT i\{0}
such that, for all X ⊆ hT i:
df {α ∈ X | ∃t ∈ α ∀l ∈ ℓ(t) ∃α + β ∈ X : l ∈ ℓ(β)} if X is finite
cds ℓ (X) =
∅ otherwise .
Proposition 1. cds ℓ is a bounded step firing policy.
Proof. All we need to prove is that if X ∈ Xτ is finite and Y ⊆ X and X \
cds ℓ (X) ⊆ Y and α ∈ cds ℓ (X) ∩ Y , then α ∈ cds ℓ (Y ).
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 ).
⊔
⊓
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
axiom ii are satisfied for T with policy cds = cds ℓ .
Proposition 2. Let M be a marking of a τ /ℓ-net system N P such that the set
enbld N P (M ) is finite. A step α ∈ enbld N P (M ) belongs to Enbld N P (M ) iff for
every t ∈ α there is l ∈ ℓ(t) such that:
l ∈ ℓ(t′ ) =⇒ α + t′ ∈
/ enbld N P (M ) ,
for every transition t′ .
Proof. Follows from max≤ (enbld N P (M )) ⊆ Enbld N P (M ), and the fact that
γ ≤ δ and δ ∈ enbld N P (M ) together imply γ ∈ enbld N P (M ). ⊔
⊓
Synthesis of PNs with localities Petri Nets & Concurrency – 167
We obtain an immediate solution to the synthesis problem for τ /ℓ-nets.
Theorem 2. A finite step transition system T can be realised by a τ /ℓ-net sys-
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 (and with
or without inhibitor and read arcs) have been investigated in [10–12]. For such
nets, the locality mapping ℓ has the property that |ℓ(t)| = 1, for all t ∈ T . Such
an ℓ defines localities which are mutually disjoint or non-overlapping. In this
paper, we allow fully general, i.e., possibly overlapping localities.
As to the effective construction of synthesised net, it has been demonstrated
in [10–12] that this can be easily done for net classes with non-overlapping locali-
ties mentioned above. Similar argument can be applied also in the general setting
of overlapping localities and τ -nets corresponding to PT-nets and EN-systems
with localities. We omit details.
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 syn-
thesis procedure would be a suitable (or good ) locality mapping. Clearly, what
really matters in a locality mapping is the identification of (possibly overlap-
ping) 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 could simply enu-
merate them and then check one-by-one using Theorem 2. This, however, 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.
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
τ -net with localities (see axiom ii and Theorem 2).
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.
– minSteps q 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 allSteps q .
– clusters ℓq is the set of all sets {t ∈ Tq | l ∈ ℓ(t)}, for every l ∈ ℓ(Tq ).
168 Petri Nets & Concurrency Koutny and Pietkiewicz-Koutny
′
– ℓ 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 co-
located transitions in each individual node of the step transition system.
Proposition 3. Let ℓ and ℓ′ be two node-consistent locality mappings. Then T
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)
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 ℓ′
are node-consistent, (1) holds. ⊔
⊓
As a consequence, a good locality mapping can be arbitrarily modified to
yield another good locality mapping as long as the two mappings are node-
consistent (there is no need to re-check the two axioms involved in Theorem 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).
The construction of a good locality mapping could be seen as modular pro-
cess, 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
df
mappings. Each such cluster-set clSet = {C1 , . . . , Ck } is composed of non-empty
subsets of Tq so that C1 ∪ . . . ∪ Ck = Tq and:
enbld T (q) = enbld T ,τ (q) \ cds clSet (enbld T ,τ (q))
where
cds clSet (X) = {α ∈ X | ∃t ∈ α ∀i ≤ k : (t ∈ Ci ⇒ ∃t′ ∈ Ci : α + t′ ∈ X)} .
df
Similarly, one may produce, for each state q, a characterisation of inadmissible
clustering of transitions. We can then select different cluster-sets (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 [12] to construct
‘canonical’ locality mappings for the case of non-overlapping localities (and the
combining of cluster-sets was based on the operation of transitive closure).
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).
Synthesis of PNs with localities Petri Nets & Concurrency – 169
4.1 Localised conflicts
Intuitively, localities and conflicts may have opposite effects on step enabled-
ness. 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 interesting what sim-
plifications, if any, one might obtain if conflicts were constrained to exist between
transitions sharing localities.
In the paper [12] we looked at this issue in the context of PTL-nets and ENL-
nets, coming up with the notion of nets with localised conflicts. For the synthesis
problem for such nets, it turned out that for each state q there was at most
one cluster-set to be considered, providing particularly pleasant simplification of
the original problem. In the rest of this section, we provide some initial results
towards extending this to the case of nets with overlapping localities. Below, for
df
a step α and locality l we denote α|l = α|{t∈T |l∈ℓ(t)} assuming that ℓ is given.
Moreover, Enbld min
df
N P (M ) = min≤ {α ∈ Enbld N P (M ) | α 6= ∅}.
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:
df
satlocalities M (α) = {l ∈ ℓ(α) | ¬ ∃ α + β ∈ enbld N P (M ) : l ∈ ℓ(β)} .
Intuitively, saturated localities are those which have been ‘active’ during 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:
df
satclusters q (α) = {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 (α) } ⊆ satclusters M (α) .
The following definition is our first attempt to generalise the notion of nets
with localised conflicts investigated in [12].
Definition 6 (localised conflicts). A τ /ℓ-net system N P has partially lo-
calised 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 ) .
170 Petri Nets & Concurrency Koutny and Pietkiewicz-Koutny
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.
Proposition 4. Let N P be a τ /ℓ-net system with partially localised conflicts
and M be its reachable marking.
If α ∈ Enbld N P (M ) then α|l ∈ Enbld N P (M ), for all l ∈ satlocalities M (α).
Proof. Suppose that e l ∈ satlocalities M (α) and α|el ∈/ Enbld N P (M ).
Since α|el ≤ α ∈ Enbld N P (M ), we have α|el ∈ enbld N P (M ). Hence there
is e
t ∈ α|el such that, for all l ∈ ℓ(e t), there is α|el + t′ ∈ enbld N P (M ) with
′ e
l ∈ ℓ(t ). In particular, since l ∈ ℓ(et), there is α|el + b
t ∈ enbld N P (M ) such that
e
l ∈ ℓ(bt). Hence bt ∈ enbld N P (M ), and so we can use Definition 6 to infer that
α+b t ∈ enbld N P (M ), producing a contradiction with e l ∈ satlocalities M (α). ⊓
⊔
Thus in terms of selecting clusters in the construction outlined in the previous
section, if C has been selected at a state q then, for every α such that C ∈
satclusters q (α), it must be the case that α|C ∈ allSteps q .
Proposition 5. Let N P be a τ /ℓ-net system with partially localised conflicts
and M be its reachable marking.
If α ∈ Enbld min
N P (M ) then α = α|l , for all l ∈ satlocalities M (α).
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 α
is a minimal non-empty step in Enbld N P (M ), we have α = α|l . ⊔
⊓
Thus in terms of selecting clusters in the construction outlined in the previous
section, if C has been selected at a state q then, for every α ∈ minSteps q such
that C ∈ satclusters q (α), it must be the case that α|C = α.
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.
Proposition 6. Let N P be a τ /ℓ-net system with partially localised conflicts
and M be its reachable marking. Then, for all α ∈ Enbld min
N P (M ):
\
satlocalities M (α) ⊆ {ℓ(t) | t ∈ α} .
Proof. Let l ∈ satlocalities M (α). By Proposition 5, we have α = α|l . Hence
l ∈ ℓ(t), for all t ∈ α. ⊔
⊓
Corollary 1. Let N P be a τ /ℓ-net system with partially localised conflicts and
M be its reachable marking. Then, for all α ∈ Enbld min
N P (M ):
\
{ℓ(t) | t ∈ α} 6= ∅ .
Synthesis of PNs with localities Petri Nets & Concurrency – 171
Proof. By α ∈ Enbld N P (M ), satlocalities M (α)∩ℓ(t) 6= ∅, for every t ∈ α. Hence
satlocalities M (α) 6= ∅ and the result follows from Proposition 6. ⊔
⊓
We will now need the following auxiliary fact.
Proposition 7. Let N P be a τ /ℓ-net system with partially localised conflicts
and M be its reachable marking. If α, β ∈ Enbld N P (M ) and α ≤ β then
satlocalities M (α) ⊆ satlocalities M (β).
Proof. Suppose l ∈ satlocalities M (α) \ satlocalities M (β).
From l ∈ satlocalities M (α) we have that l ∈ ℓ(α) and:
∀ t : l ∈ ℓ(t) =⇒ α + t ∈
/ enbld N P (M ) . (2)
From l ∈/ satlocalities M (β) we have that either l ∈
/ ℓ(β), or l ∈ ℓ(β) and there is
e
t such that:
l ∈ ℓ(e
t) ∧ β + et ∈ enbld N P (M ) . (3)
Only the latter is possible, because l ∈ ℓ(α) and α ≤ β. From (2) and (3) we
have that α + et ∈/ enbld N P (M ) and β + e
t ∈ enbld N P (M ), which produces a
contradiction with α + et ≤ β +et. ⊔
⊓
Proposition 8. Let N P be a τ /ℓ-net system with partially localised conflicts
and M be its reachable marking. Moreover, let α ∈ Enbld N P (M ) and e l ∈
satlocalities M (α) be such that α|l 6< α|el , for all l ∈ satlocalities M (α) \ {e
l}.
Then α|el ∈ Enbld min
N P (M ).
Proof. From Proposition 4 we have that α|el ∈ Enbld N P (M ). Suppose there is a
non-empty step β ∈ Enbld N P (M ) such that β < α|el . From Proposition 7 and
α|el ≤ α, it follows that
satlocalities M (β) ⊆ satlocalities M (α|el ) ⊆ satlocalities M (α) .
As β 6= ∅ and β ∈ Enbld N P (M ) we obtain
satlocalities M (β) 6= ∅ .
We have that e l∈/ satlocalities M (β) as β < α|el . Let bl ∈ satlocalities M (β). Since
b
satlocalities M (β) ⊆ satlocalities M (α), we have l ∈ satlocalities M (α). Hence, by
Proposition 4, α|bl ∈ Enbld N P (M ). By the assumption we made, α|bl 6< α|el as
b
l 6= e
l. So, there is bt such that α|bl (b
t) ≥ α|el (b
t) > β(b
t), producing a contradiction
with b l ∈ satlocalities M (β). ⊔
⊓
Let N P be a τ /ℓ-net system with partially localised conflicts and M be its
reachable marking. Then:
maxind M
df
t = max{α(t) | α ∈ Enbld N P (M )} ,
for every net transition t which is resource enabled at M .
172 Petri Nets & Concurrency Koutny and Pietkiewicz-Koutny
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 e
l. Then exactly one of the
following holds:
– There is no step α ∈ Enbld N P (M ) such that e
l ∈ satlocalities M (α) and
maxind M M
t + maxind u = α(t) + α(u) (4)
and, for all l ∈ satlocalities M (α) \ {e
l}, we have α|l 6< α|el .
– There is α ∈ Enbld min
N P (M ) such that t, u ∈ α.
Proof. We have e l ∈ ℓ(t) ∩ ℓ(u). Suppose that there is α ∈ Enbld N P (M ) such
that (4) holds and e l ∈ satlocalities M (α) and for all l ∈ satlocalities M (α) \ {e
l},
α|l 6< α|el . Since t and u are resource enabled at M and (4) holds, we have
α(t) ≥ 1 and α(u) ≥ 1. On the other hand, e l ∈ ℓ(t) ∩ ℓ(u). Then, t, u ∈ α|el . We
can see that all the conditions of Proposition 8 are satisfied for α and e l, and so
we obtain that α|el ∈ Enbld min
NP (M ). ⊔
⊓
Unique and minimal step covers It is not possible to reverse the inclusion
in Proposition 6, i.e., there can be α ∈ Enbld min
N P (M ) such that:
\
{ℓ(t) | t ∈ α} ⊆ satlocalities M (α)
does no hold. As an example, we can take a PT-net with two concurrent tran-
sitions, 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}
belongs to Enbld min
N P (M0 ) yet:
\
{ℓ(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-operation. 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
been active during its execution, as both L = {l} and L′ = {l, l′} could be taken.
We will now investigate the role of such sets of localities.
Definition 7 (step covers). A (locality) cover of a step α is a set of localities L
such that: [
supp(α) = {supp(α|l ) | l ∈ L} ,
Synthesis of PNs with localities Petri Nets & Concurrency – 173
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′ }.
Example 1. Let ℓ(a) = {l, l′} and ℓ(b) = {l}. Then L = {l, l′ } is not a minimal
cover for α = {a} as L′ = {l′ } is also a cover.
Example 2. Let ℓ(a) = ℓ(b) = {l, l′}. Then there are two minimal covers for
α = {a, b}, L = {l} and L′ = {l′ }, which are not unique.
Example 3. Let ℓ(a) = {l, l′ }, ℓ(b) = {l} and ℓ(c) = {l′ }. Then L = {l, l′} is a
unique cover for α = {a, b, c}.
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′ =
{l3 , l4 }.
Equipped with the concept of a unique minimal cover, we can reverse the
inclusion in Proposition 6.
Proposition 10. Let N P be a τ /ℓ-net system with partially localised conflicts
and M be its reachable marking. If α ∈ Enbld min
N P (M ) and all its minimal covers
are unique, then:
\
satlocalities M (α) = {ℓ(t) | t ∈ α} .
Proof. We need to show the (⊇) inclusion as the opposite one follows from
T
Proposition 6. Suppose that e l ∈ {ℓ(t) | t ∈ α} \ satlocalities M (α).
T
From el ∈ {ℓ(t) | t ∈ α} we have α = α|el . Since α ∈ Enbld min N P (M ), we have
b
satlocalities M (α) ∩ ℓ(t) 6= ∅, for all t ∈ α. Suppose l ∈ satlocalities M (α) ∩ ℓ(et),
for some e t ∈ α. Notice that b l 6= e
l as e
l∈/ satlocalities M (α). From Proposition 4,
α|bl ∈ Enbld N P (M ).
We have α|bl ≤ α = α|el . We cannot have α|bl = α|el , because then both {e l}
b
and {l} would be two different minimal covers for α, and so neither of them be
unique. Hence α|bl < α, producing a contradiction with the minimality of α. ⊓ ⊔
Thus in terms of selecting clusters in the construction outlined earlier on, if
C has been selected at a state q then, for every α ∈ minSteps q , we must have
C ∈ satclusters q (α) iff α|C = α.
5 Concluding remarks
In this paper, we only initiated the investigation of intricate relationships be-
tween 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.
174 Petri Nets & Concurrency Koutny and Pietkiewicz-Koutny
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.
References
1. Badouel, E., Bernardinello, L., Darondeau, Ph.: The Synthesis Problem for Ele-
mentary Net Systems is NP-complete. Theoretical Computer Science 186 (1997)
107–134
2. Badouel, E., Darondeau, Ph.: Theory of Regions. In: Reisig, W., Rozenberg, G.
(eds.): Lectures on Petri Nets I: Basic Models, Advances in Petri Nets. Lecture
Notes in Computer Science 1491. Springer-Verlag, Berlin Heidelberg New York
(1998) 529–586
3. Bernardinello, L.: Synthesis of Net Systems In: Marsan, M.A. (ed.): Application
and Theory of Petri Nets 1993. Lecture Notes in Computer Science 691. Springer-
Verlag, Berlin Heidelberg New York (1993) 89–105
4. Darondeau, P., Koutny, M., Pietkiewicz-Koutny, M., Yakovlev, A.: Synthesis of
Nets with Step Firing Policies. Fundamenta Informaticae 94 (2009) 275–303
5. Desel, J., Reisig, W.: The Synthesis Problem of Petri Nets. Acta Informatica 33
(1996) 297–315
6. Dasgupta, S., Potop-Butucaru, D., Caillaud, B., Yakovlev, A.: Moving from Weakly
Endochronous Systems to Delay-Insensitive Circuits. Electronic Notes in Theoret-
ical Computer Science 146 (2006) 81–103
7. Desel, J., Reisig, W.: The Synthesis Problem of Petri Nets. Acta Informatica 33
(1996) 297–315
8. Kleijn, J., Koutny, M.: Processes of Membrane systems with Promoters and In-
hibitors. Theoretical Computer Science 404 (2008) 112–126
9. Kleijn, H.C.M., Koutny, M., Rozenberg, G.: Towards a Petri Net Semantics for
Membrane Systems. In: Freund, R., Paun, G., Rozenberg, G., Salomaa, A. (eds.):
WMC 2005. Lecture Notes in Computer Science 3850. Springer-Verlag, Berlin
Heidelberg New York (2006) 292–309
10. Koutny, M., Pietkiewicz-Koutny, M.: Transition Systems of Elementary Net Sys-
tems with Localities. In: Baier, C., Hermanns, H. (eds.): CONCUR 2006. Lecture
Notes in Computer Science 4137. Springer-Verlag, Berlin Heidelberg New York
(2006) 173–187
11. Koutny, M., Pietkiewicz-Koutny, M.: Synthesis of Elementary Net Systems with
Context Arcs and Localities. Fundamenta Informaticae 88 (2008) 307–328
12. Koutny, M., Pietkiewicz-Koutny, M.: Synthesis of Petri Nets with Localities. Sci-
entific Annals of Computer Science 19 (2009) 1–23
13. Mukund, M.: Petri Nets and Step Transition Systems. International Journal of
Foundations of Computer Science 3 (1992) 443–478
14. Nielsen, M., Rozenberg, G., Thiagarajan, P.S.: Elementary transition systems. The-
oretical Compututer Science 96 (1992) 3–33
15. Păun, G.: Membrane Computing, An Introduction. Springer-Verlag, Berlin Heidel-
berg New York (2002)
16. Pietkiewicz-Koutny, M.: The Synthesis Problem for Elementary Net Systems with
Inhibitor Arcs. Fundamenta Informaticae 40 (1999) 251–283