This paper introduces properties preset-equality for equalconflict Petri nets and enabling-equivalence for their reachability graphs. It explores the relation between these properties and shows its use for synthesis of equal-conflict Petri nets from labelled transition systems. ? Supported by DFG (German Research Foundation) through grant Be 1267/15-1 ARS (Algorithms for Reengineering and Synthesis).
The task in Petri net synthesis is to construct a Petri net whose reachability
graph is isomorphic to a given labelled transition system (lts). The theory behind
Petri net synthesis is based on regions of the lts and goes back to [
In this paper, we investigate the synthesis of equal-conflict Petri nets. Equalconflictness is a combination of two other properties: All transitions consuming tokens from a place consume the same number of tokens (homogeneous) and transitions with non-disjoint presets have equal presets (weighted free-choice).
Our approach has two phases: First we identify structural constraints on the
desired Petri net based on the lts. Then a predicate is formulated that restricts
regions so that only equal-conflict solutions are found. This predicate can then
be used in the framework of [
Figure 1 shows that equal-conflict Petri nets are less expressive than general Petri nets. It shows an lts A and a Petri net N so that RG(N ) ∼= A, but no equal-conflict Petri net can generate A, as will be shown later.
After the preliminaries in section 2, section 3 defines the predicate announced above and shows its correctness. Section 4 extends this result to plain and pure Petri nets and Section 5 concludes this paper.
A (finite, initially marked, place-transition, arc-weighted, unlabelled) Petri net is a tuple (P, T, F, M0) such that P is a finite set of places, T is a finite set of transitions, with P ∩ T = ∅, F is a flow function F : ((P × T ) ∪ (T × P )) → N, and M0 is the initial marking, where a marking is a mapping M : P → N, indicating the number of tokens in each place. F (p, t) = w > 0 (resp. F (t, p) = w > 0) means that there is an arc from p to t (resp. from t to p) with arc weight w. A transition t ∈ T is enabled by a marking M , denoted by M [ti, if for all places p ∈ P , M (p) ≥ F (p, t). If t is enabled at M , then t can occur (or fire ) in M , leading to the marking M 0 defined by ∀p ∈ P : M 0(p) = M (p) − F (p, t) + F (t, p) (notation: M [tiM 0). We denote by [M0i the set of markings, which are reachable from M0 by (repeated) firing. For a place p of a Petri net N = (P, T, F, M0), let •p = {t ∈ T | F (t, p) > 0} be its preset, and p• = {t ∈ T | F (p, t) > 0} its postset. Analogously, for a transition t define its preset as •t = {p ∈ P | F (p, t) > 0}, and its postset as t• = {p ∈ P | F (t, p) > 0}. N is called pure or side-condition free if p• ∩ •p = ∅ for all p ∈ P ; plain (also known as ordinary) if F (t, p) ≤ 1 and F (p, t) ≤ 1 for all p ∈ P and t ∈ T ; bounded if ∃k ∈ N : ∀M ∈ [M0i : ∀p ∈ P : M (p) ≤ k (i.e., a limit of the number of tokens on any place exists); simply live if ∀t ∈ T : ∃M ∈ [M0i : M [ti; homogeneous if ∀p ∈ P : ∃k ∈ N : ∀t ∈ p• : F (p, t) = k; weighted free-choice if ∀t1, t2 ∈ T : •t1 ∩•t2 6= ∅ ⇒ •t1 = •t2; and equal-conflict if it is homogeneous and weighted free-choice.
An lts (labelled transition system with initial state) is a tuple (S, →, T, s0), where S is a set of states, T is a set of labels with S ∩ T = ∅, → ⊆ (S × T × S) is the transition relation, and s0 ∈ S is an initial state. A label t is enabled in a state s if there is some state s0 such that (s, t, s0) ∈ →. Two lts A1 = (S1, →1, T, s01) and A2 = (S2, →2, T, s02) over the same set of labels T are isomorphic (notation: A1 =∼ A2) if there is a bijection ζ : S1 → S2 with ζ(s01) = s02 and (s, t, s0) ∈ →1 ⇐⇒ (ζ(s), t, ζ(s0)) ∈ →2, for all s, s0 ∈ S1.
The reachability graph of N , with initial marking M0 and transitions T , is the lts RG(N ) = ([M0i, {(M, t, M 0) | M, M 0 ∈ [M0i ∧ t ∈ T ∧ M [tiM 0}, T, M0). If an lts A is isomorphic to the reachability graph of a Petri net N , then we will also say that N is a solution of A.
A region of an lts A = (S, →, T, s0) is a tuple (R, B, F) ∈ (NS , NT , NT ) such that for all arcs (s, t, s0) ∈ → in A, both R(s) ≥ B(t) and R(s0) = R(s) − B(t) + F(t) hold. Intuitively, this describes a possible place in a Petri net generating A where B(t), resp. F(t), describes the number of tokens consumed, resp. produced, by a transition t ∈ T and R(s) is the number of tokens on this place in state s ∈ S. The requirement above then describes an occurrence of transition t. Thus, a region corresponds to a Petri net with a single place. Similarly, a set of regions corresponds to a Petri net with multiple places. We call a region homogeneous if its corresponding Petri net is homogeneous and use the same convention for sets of regions and other properties, like equal-conflict and weighted free-choice. 3
This section investigates the following two properties: Two transitions t1, t2 ∈ T of a Petri net N are preset-equal if they have the same preset, •t1 = •t2. Two labels t1, t2 ∈ T of an lts A are enabling-equivalent if no state s ∈ S only enables one of the two labels, i.e. ∀s ∈ S : (∃s0 ∈ S : (s, t1, s0) ∈ →) ⇔ (∃s0 ∈ S : (s, t2, s0) ∈ →).
As an example for this definition, consider the equal-conflict Petri net N from Figure 2. The transition t1 is not preset-equal with any other transition, but t2 and t3 are preset-equal. A similar relationship can be seen in RG(N ): There are states where only t1 is enabled, so it is not enabling-equivalent with any other label, but t2 and t3 are enabling-equivalent.
The following theorems show that these two properties (almost) imply each other in equal-conflict Petri nets and their reachability graphs. This relationship is then used to define additional constraints on the regions found by Petri net synthesis, so that equal-conflict Petri nets are computed.
Theorem 1. Let N be a homogeneous Petri net. Then the preset-equal property on N implies the enabling-equivalence property on RG(N ).
Proof. Let t1, t2 ∈ T be two preset-equal transitions. Since N is homogeneous, we get for each p ∈ P that F (p, t1) = F (p, t2). By the definition of enabledness, any given marking enables either both transitions or neither. tu This theorem allows us to show that there is no equal-conflict Petri net N with RG(N ) ∼= A, where A was shown in Figure 1. Assume that an equal-conflict Petri net N exists. We can see that t1 and t3 are not enabling-equivalent, because in s3 only t1 is enabled. By the previous theorem, they are not preset-equal. Since we are desiring an equal-conflict solution, they must have disjoint presets. However, in the initial state both t1 and t3 are enabled, but firing one of them disables the other. This is only possible if they have non-disjoint presets in N , hence we get a contradiction. Thus, there is no equal-conflict Petri net that generates A.
For the opposite implication, namely deriving preset-equality from enablingequivalence, we can only show a weaker result: There is a Petri net where enabling-equivalent transitions are preset-equal. Examples for this construction are provided in Figure 3.
Theorem 2. Let N be an equal-conflict Petri net. Then there is an equalconflict Petri net N 0 with RG(N ) = RG(N 0) so that enabling-equivalent transitions in RG(N 0) are preset-equal in N 0.
Proof. The following step can inductively be used to modify N so that any t1, t2 ∈ T which are enabling-equivalent, but not preset-equal, become presetequal. The result of this construction will be the needed N 0.
For any transition t3 that is preset-equal with t2 (including t2 itself) and any place p ∈ •t1, add a side-condition between t3 and p with weight F (p, t1). This means both F (p, t3) (previously zero by assumption) and F (t3, p) (possibly non-zero) are increased by F (p, t1). Also, do the analogous operation with t1 and t2 swapped.
The resulting net will still be equal-conflict by construction, but it will also satisfy •t1 = •t2. Also, its behaviour was not modified, because the effects of transitions were not modified and no transition becomes disabled in a marking that previously enabled it, because by enabling-equivalence enough tokens for the added flows are available. tu N1 :
N10 :
N2 :
N20 : 2 t1 t2 2 t1 t2 t1 t2 t1 t2
With the results so far we can assume w.l.o.g. that in equal-conflict Petri nets, transitions are enabling-equivalent iff they are preset-equal. This can be used to define a predicate on regions, as follows.
Let an lts A over the set of labels T be given that should be solved by an equal-conflict Petri net N with A ∼= RG(N ). First, the enabling-equivalent labels in A are computed. This produces a partitioning E ⊆ 2T of the set of labels into enabling-equivalent classes. Next, we say that a region (R, B, F) is compatible with the desired equal-conflict Petri net N = (P, T, F, M0), if it is homogeneous, meaning that for all transitions t1, t2 ∈ T if B(t1) > 0 ∧ B(t2) > 0 then B(t1) = B(t2), and its postset is in E ∪ {∅}. These two conditions (homogeneous and postset in E) are expressed by the following predicate:
_ e∈E∪{∅}
^ t1,t2∈e
B(t1) = B(t2) ∧ B(t2) > 0 !
∧ ^ B(t) = 0
t6∈e
The algorithm from [
As an example of this, let us come back to the lts A from Figure 1. We already argued that this lts cannot be solved by an equal-conflict Petri net and will now look more formally at this problem. Because no two labels are enablingequivalent, we have E = {{t1}, {t2}, {t3}}. Our predicate indicates that at most one transition can consume tokens from a place.
We will try to find a region (R, B, F) that prevents1 t1 in state s2, i.e. that satisfies R(s2) < B(t1). From this formula we already conclude that 0 < B(t1), because R(s2) ∈ N. By definition of a region, we have R(s0) − B(t3) + F(t3) = R(s2) < B(t1). Because of the edge (s0, t1, s1) we know by definition of a region that B(t1) ≤ R(s0). Adding the last two inequalities produces −B(t3)+F(t3) < 0, which implies that 0 < B(t3). Thus, we have shown that 0 < B(t1) and 0 < B(t3), which is however not compatible with the predicate, since there is no e ∈ E ∪ {∅} with t1, t3 ∈ e. This means that the assumption that t1 can be prevented in state s2 was wrong and A cannot be solved by an equal-conflict Petri net. Theorem 3. Given a finite lts A, the synthesis procedure produces an equalconflict Petri net NR with RG(NR) ∼= A iff there is an equal-conflict Petri net N with RG(N ) ∼= A.
Proof. (⇒): If the algorithm finds a Petri net N , then each place of N corresponds to a region satisfying the predicate. This means that N is homogeneous and the postset of each place is in E ∪ {∅}. Since elements of E are disjoint, N is an equal-conflict Petri net.
(⇐): To show that a solution is always found if one exists, assume a suitable
Petri net N exists. By Theorem 2 we can w.l.o.g. assume that enabling-equivalent
transitions are preset-equal in N . The contraposition of Theorem 1 shows that
non-enabling-equivalent transitions must not be preset-equal, which means that
their presets must be disjoint by weighted free-choice. Thus, the regions
corresponding to the places of N satisfy the above predicate and are a possible result
of the algorithm. tu
1 We are attempting to solve the ESSP instance (s2, t1). For more details, see [
So far we can synthesise equal-conflict Petri nets via the new predicate and the
algorithm from [
Theorem 2 is not applicable for synthesising pure equal-conflict Petri nets, because it only shows the existence of an equivalent non-pure Petri net, as the example N2 and N20 in Figure 3 demonstrates. Additionally, Figure 4 has an example N3 and N30 showing that plainness is not preserved, too. All properties from the list above except for plain and pure are unaffected by the construction from Theorem 2, or are already more restrictive than equal-conflictness. The following Theorem 4 closes this gap.
N3 :
N4 : t1
t2 t3
N30 : t1 t2 t1 2 t2 N400 :
N300 : t3 t1
t2 t1 t2
Theorem 4. Let N be an equal-conflict Petri net that is pure or both bounded and plain. Then there is an equal-conflict Petri net N 0 with RG(N ) ∼= RG(N 0) so that enabling-equivalent transitions in RG(N 0) are preset-equal in N 0. Additionally, N 0 is pure if N is pure and plain if N is plain.
Proof. First we modify the transitions which can never occur, so that we can assume simple liveness for the remaining transitions. Let D ⊆ T be the set of all such dead transitions. We construct N 0 by removing all flows connected to a transition in D. Then, we add a new place p with M0(p) = 0 and add flows so that ∀t ∈ D : F (p, t) = 1. This place ensures that all transitions in D cannot occur. Because dead transitions do not influence the behaviour of the Petri net, we have RG(N ) ∼= RG(N 0). Also, this construction preserves plainness and pureness.
Next, let T 0 ⊆ T be a set of pairwise enabling-equivalent transitions containing t1, t2 ∈ T 0 that are not preset-equal. By simple liveness, there are two cases: Either there are reachable markings M, M 0 with M 0[t1iM and ¬M [t1i, or t1 can be fired infinitely often once it is enabled.
In the first case, by enabling-equivalence we get M 0[t2iM and ¬M [t2i. Thus, firing t1 disables t2 and by the firing rule we deduce •t1 ∩ •t2 6= ∅. Because N is weighted free-choice, this implies that •t1 = •t2. Since t2 was arbitrary, we have that all transitions that are enabling-equivalent with t1 are in fact preset-equal with it. Thus, in this case we have N 0 = N .
In the latter case, by the firing rule we have ∀p ∈ P : F (t1, p) ≥ F (p, t1). If N is pure (and possibly plain), it follows that F (p, t1) = 0 and so t1 has an empty preset. By enabling-equivalence we get analogously •t2 = ∅ and hence •t1 = ∅ = •t2. We have again N 0 = N .
If N is bounded and plain, then by boundedness we get ∀p ∈ P : F (t1, p) = F (p, t1) ∧ F (t2, p) = F (p, t2). By plainness, the only option for t1 and t2 not to be preset-equal is if (w.l.o.g.) F (t1, p) = 1 and F (t2, p) = 0 for some place p ∈ P . Let T 00 ⊆ T 0 contain all transitions t ∈ T 0 with F (t, p) = 0. We can add a side condition between each t ∈ T 00 and p of weight one without modifying the behaviour of the Petri net, because by enabling-equivalence with t1 there is always a token in p when t ∈ T 00 is enabled. This produces the pure and equalconflict Petri net N 0 with RG(N 0) = RG(N ). tu With this theorem, the construction from the previous section also works when the new predicate for equal-conflict Petri net synthesis is combined with predicates for other properties. 5
In this paper we extended the family of Petri net classes which can be targeted
for Petri net synthesis. The synthesis can now target equal-conflict Petri nets
and, by combination with other predicates (c.f. [
A construction similar to Theorem 2 is called equalisation in [
Besides implementing this new approach in our tool APT [
Acknowledgements: The authors are grateful to the anonymous reviewers for their helpful remarks and to Eike Best for his help in preparing this paper.