Properties of Plain, Pure, and Safe Petri Nets

Abstract

A set of necessary conditions for a Petri net to be plain, pure and safe is derived. It is argued that these conditions are applicable, both in practice (in the interest of Petri net synthesis), and in theory (e.g., as part of a characterisation of the reachability graphs of live and safe marked graphs).

Keywords

• Labelled transition systems
• marked graphs
• Petri nets

Introduction

In the first part (section 2) of this paper, we examine a number of properties

which are typical for plain, pure and safe (pps) Petri nets. Such nets are intimately related to elementary Petri net systems [ 7–10 ]. We shall also argue that these properties can be employed usefully in the quick-fail, pre-synthesis stage of a Petri net synthesis algorithm, if it is aimed at pps nets.

In the second part (section 3) of the paper, we apply our results in order to

obtain a characterisation of the state spaces of live and safe marked graphs [ 5 ].

This result will be built upon the characterisation of live and bounded marked graphs previously described in [3].

Basic definitions about transition systems and Petri nets have been transferred to

the appendix (section A), in order to make the paper self-contained, without impeding its readability for readers familiar with the basic theory. In conformance with the book [ 1 ] on net synthesis, we shall consider arc-labelled transition systems and transition-unlabelled Petri nets.

Part of this work was done during a research visit by the first author in Oldenburg on a research fellowship within the EU-sponsored project POKL.04.01.01-00-081/10

Some necessary conditions for pps Petri nets

In the following, we shall use letters a, b, c, . . . ∈ T (also t ∈ T ) for letters of

a transition system (or, respectively, for the corresponding transitions of a Petri net); u, v, w ∈ T ∗ for sequences of transitions; p, q for the places of a net; M, K, L for the markings of a net; and r, s for the states of an lts. The • and notation, which is much used in the following, is explained in section A (definition 7). 2.1

Properties of plain, pure, and safe Petri nets Proposition 1. Properties of pps nets Let N = (P, T, F, M0) be a pps net, let a, b, c be (not necessarily different) transitions in T , let M, M , K, . . . be reachable markings, and let w, v, u, . . . be sequences of transitions. Then (A) If M [wv or M [vw , then w ∩ v = ∅ = w ∩ v . (B) If M [a M and M [b M , then [b M ⇐⇒ [a M . (C) If M [a and M [b , then a• ∩ •b = ∅ = •a ∩ b•. (D) If M [a and M [b , then for any K: (K[ab ⇐⇒ K[ba ). (E) If M [awb then (•a ∩ •b) ⊆ w and (a• ∩ b•) ⊆ w. (F) If M [wv and M [vw and M [wc and M [vc ,

then M [wvc M and M [vwc M and M [c . (G) – If (M1[x1w1y1 ) and (M2[x2w2y2 ) with x1, y1, x2, y2 ∈ {a, b}, and (•a ∩ •b = ∅ or a• ∩ b• = ∅), and there exist v1, v2, v3 such that Ψ (w1) = Ψ (v1)+Ψ (v2), Ψ (w2) = Ψ (v2)+Ψ (v3), Ψ (w3) = Ψ (v3)+Ψ (v1), – then ¬K[x3w3y3 for x3, y3 ∈ {a, b}.

Proof: (A): Suppose M [w M1[v M2. If Ψ (w) = Ψ (v) then if p ∈ w and p ∈ v then M (p) = M2(p) + 2 as well as if p ∈ w and p ∈ v then M2(p) = M (p) + 2. Both situations contradicts safeness. This implies that w = ∅ = w and v = ∅ = v and the claim is true. Assume now that Ψ (w) = Ψ (v). If p ∈ w ∩ v then M (p) = 1, M1(p) = 0 and M2(p) = −1. Contradiction. Similarly, if p ∈ w ∩ v then M (p) = 0, M1(p) = 1 and M2(p) = 2. Contradiction. Hence w ∩ v = ∅ = w ∩ v , as was claimed. (B): Suppose that M [a M and M [b M and K[b M , for some reachable K, and ¬([a M ). By ¬([a M ), there is some place p ∈ a• \ •a with M (p) = 0. By M [a M , both M (p) = 0 and M (p) = 1. By M [b M , p ∈ b• \ •b. By K[b M , M (p) = 1, contradicting M (p) = 0. Hence K [a M for some reachable K , and K = K because K and K can be backward-reached from M by the same

Parikh vector.

(C,D): If a = b, the claim follows by the absence of side-places.

Suppose that a = b and M [a and M [b . If p ∈ a• ∩ •b, then M (p) = 0 since M enables a, but also M (p) = 1 since M enables b, which is a contradiction. If p ∈ •a ∩ b•, we get a symmetrical contradiction. To show the remaining part of the claim, suppose that K[ab . Using (A) applied to K with w = a and v = b and knowing that •a = a and a• = a we get (•a∪a•)∩(•b∪b•) = ∅ (i.e., intuitively, a and b are completely independent), and thus also K[ba . The reverse direction is symmetrical. (E): Suppose that M [a M1[w M2[b M and that p ∈ (•a ∩ •b). Then M (p) = 1, M1(p) = 0, M2(p) = 1, and M (p) = 0, so that w acts positively on p, that is, p ∈ w . Similarly for p ∈ (a• ∩ b•): M (p) = 0, M1(p) = 1, M2(p) = 0 and M (p) = 1 w acts negatively on p, that is, p ∈ w. (F): Suppose that M [w M1[v M2 and M [v M3[w M4. Of course from the firing rule we know that M3 = M4. By (A) and M [w M1[c with M [v M3[c we get: •c ∩ v = ∅ = •c ∩ w and c• ∩ v = ∅ = c• ∩ w .

From M1[c we know that for all p ∈ •c we have M1(p) = 1 and from the previous considerations p ∈/ v. Assume now that p ∈ v . Then M2(p) = 2. Contradiction. Hence •c ∩ ( v ∪ v ) = ∅.

From M3[c we know that for all p ∈ •c we have M3(p) = 1 and from the previous considerations p ∈/ w. Assume now that p ∈ w . Then M2(p) = 2. Contradiction. Hence •c ∩ ( w ∪ w ) = ∅.

From the other hand, from M1[c we know that for all p ∈ c• we have M1(p) = 0 and from the previous considerations p ∈/ v . Assume now that p ∈ v. Then M2(p) = −1. Contradiction. Hence c• ∩ ( v ∪ v ) = ∅.

From M1[c we know that for all p ∈ c• we have M3(p) = 0 and from the previous considerations p ∈/ w . Assume now that p ∈ w. Then M2(p) = −1. Contradiction. Hence c• ∩ ( w ∪ w ) = ∅.

Together we have (•c ∪ c•) ∩ ( v ∪ v ) = ∅ as well as (•c ∪ c•) ∩ ( w ∪ w ) = ∅ and it is straightforward that M [c and M2[c . (G): Assume M1[x1 M1.1[w1 M1.2[y1 M1, M2[x2 M2.1[w2 M2.2[y2 M2 and M3[x3 M3.1[w3 M3.2[y3 M3 with x1, y1, x2, y2, x3, y3 ∈ {a, b} as well as there exist v1, v2, v3 such that Ψ (w1) = Ψ (v1) + Ψ (v2), Ψ (w2) = Ψ (v2) + Ψ (v3), and Ψ (w3) = Ψ (v3) + Ψ (v1).

Case 1: •a ∩• b = ∅ Since M1[x1 M1.1[w1 M1.2[y1 M1, for every place p ∈ •a∩•b we have M1(p) = 1, M1.1(p) = 0, M1.2(p) = 1, hence ef p(w1) = 1. In a similar way we can observe that ef p(w2) = 1 and ef p(w3) = 1. Of course 1 = ef p(w2) = ef p(v1v2) = ef p(v1) + ef p(v2) hence either (1) ef p(v1) = 1 and ef p(v2) = 0 or (2) ef p(v1) = 0 and ef p(v2) = 1. Assuming (1) we obtain 1 = ef p(w2) = ef p(v2v3) = ef p(v2) + ef p(v3) = 0 + ef p(v3), hence ef p(v3) = 1. But then ef p(w3) = ef p(v3v1) = ef p(v3) + ef p(v1) = 1 + 1 = 2, which contradicts ef p(w3) = 1. Assuming (2) we obtain 1 = ef p(w2) = ef p(v2v3) = ef p(v2) + ef p(v3) = 1 + ef p(v3), hence ef p(v3) = 0. But then = ef p(w3) = ef p(v3v1) = ef p(v3) + ef p(v1) = 0 + 0 = 0, which contradicts ef p(w3) = 1. Since M1[x1 M1.1[w1 M1.2[y1 M1, for every place p ∈ a• ∩b• we have M1(p) = 0, M1.1(p) = 1, M1.2(p) = 0, hence ef p(w1) = −1. Similarly, ef p(w2) = −1 and ef p(w3) = −1. Of course −1 = ef p(w1) = ef p(v1v2) = ef p(v1) + ef p(v2) hence either (1) ef p(v1) = −1 and ef p(v2) = 0 or (2) ef p(v1) = 0 and ef p(v2) = −1. Assuming (1) we obtain −1 = ef p(w2) = ef p(v2v3) = ef p(v2) + ef p(v3) = 0 + ef p(v3), hence ef p(v3) = −1. But then ef p(w3) = ef p(v3v1) = ef p(v3) + ef p(v1) = −1 + (−1) = −2, which contradicts ef p(w3) = −1. Assuming (2) we obtain −1 = ef p(w2) = ef p(v2v3) = ef p(v2) + ef p(v3) = −1 + ef p(v3), hence ef p(v3) = 0. But then ef p(w3) = ef p(v3v1) = ef p(v3) + ef p(v1) = 0 + 0 = 0, which contradicts ef p(w3) = −1.

This finishes the proof. 1

2.2

Some discussion, and some examples

Proposition 1 implies that in any pps net reachability graph, any pair of two

distinct transitions (a, b) can be classified structurally into two types: • •a ∩ •b = ∅. Suppose that some marking M enables both a and b. Then, as a consequence of part (C) or (D) of proposition 1 and safeness, also a• ∩ b• = ∅. Therefore, M [a ∧ M [b implies the existence of a full diamond M [ab ∧

M [ba in the reachability graph. Moreover, if one such full diamond exists

for a and b, any other branching points K[a ∧ K[b can also be extended to full diamonds K[ab ∧ K[ba . • •a ∩ •b = ∅. Then any marking M enabling both a and b only leads to a proper triangle, i.e. ¬M [ab ∧ ¬M [ba . In particular, there can be no “halfpersistence” [ 2 ] such as ¬M [ab ∧ M [ba or M [ab ∧ ¬M [ba .

The two relations are symmetric but not, in general, transitive. Moreover, there

is no backward version of Proposition 1(C) or (D). Therefore, the above classification cannot be applied fully for postsets instead of presets of transitions.

Indeed, Figure 1 shows a reachability graph which has a full diamond and, at the

same time, a state-disjoint proper backward triangle between transitions a and b.

Moreover, two transitions may have a common pre-place never being enabled at the same time. See figure 2 for an example.

The properties (A)–(G) of proposition 1 come in two varieties:

• Non-structural properties. This name applies to properties (B), (D), and (F), since they do not contain any reference to a generating Petri net. Therefore, (B), (D) and (F) can be taken as properties of any arbitrary transition system. • Structural properties. This applies to properties (A), (C), (E), and (G), since they make partial reference to a generating Petri net, by mentioning the pre- and/or postsets of transitions and/or transition sequences. c a b a e a b d b M0 c a b c c a • • e p d b b a

c (A)∧(C) ⇒ (B)∧(D)∧(F) (The proofs of these claims are easy and will be omitted in the present paper.) Speaking in terms of applications, however, the non-structural conditions can be more useful than the structural ones. If a transition system is given without any generating Petri net, then (B), (D) and (F) can be tested straight away, while it can be very difficult to test one of the other properties when we also need to consider the possible shapes of any (hoped-for) Petri net solutions. For this reason, the non-structural properties can be used as limiting conditions on the class of transition systems eligible for Petri net (pre-)synthesis; this will be discussed later, in section 2.3. We finally point out that, in general, (B), (D) and (F) are independent of each other. This is proved by the labelled transition systems depicted in figure 3. Of course, due to the previous proposition, none of the three lts is actually pps solvable. (But all of them have a Petri net solution.

APT [11] is useful in confirming this.) We now briefly discuss the relevance, and the independence, of property (G).

• Consider the labelled transition system T S1 (only solid edges) depicted in figure 4. From the pattern around state K, more precisely, from K[a and

K[b and neither K[ab nor K[ba , it follows that in any pps solution of

T S1, there must exist a place p ∈ (•a ∩ •b). But then, (G) is violated, letting v1 = d1d1, v2 = e1e1, and v3 = c1c2. Nevertheless, T S1 satisfies the properties (B), (D) and (F) (and, we believe, also (A), (C) and (E), for any pps solution). In this sense, (G) “explains” the non-pps-solvability of T S1. • Now consider the transition system T S2 (solid and dashed egdes) shown in the same figure. The raison d’ˆetre for a place such as p above has disappeared, and T S2 satisfies, in fact, (G), along with (B), (D) and (F). Thus, none of these properties can be used in order to explain its non-pps-solvability.

So far, we know of no general property which explains the non-pps-solvability of

T S2 in a similar way as (G) explains the non-pps-solvability of T S1. It should come as no surprise at all that such examples can be found: obtaining an exact characterisation of the state spaces of pps Petri nets seems to be quite out of reach, at the present time.

h3 h1 h2

K a a a b d1 e1 c1 a b e1 c1 c2

M d2 e2 d1 e2 c2 d2 b b b

Pre-synthesis, and other non-structural conditions

Proposition 1 yields an upper approximation of the class of pps solvable lts. The

transition system T S2 shown in figure 4 proves that this is a true approximation, although its relative complexity suggests that it may be a reasonably good one, for the time being.

Consequently, the non-structural properties (B), (D), (F) described in proposi

tion 1 can be useful for synthesis. Suppose that a labelled transition system T S is given and a pps solution is sought for it. Before actual synthesis begins, i.e. in a pre-synthesis stage, it is possible to check (B), (D) and (F). If one of them fails, then pps synthesis is infeasible; such an effect is usually called quick fail.

In a quick-fail case, we might reject T S immediately, with two benefits: first, a costly synthesis does not need to be started, and secondly, a meaningful – possibly very useful – error message can be issued.

Quick-fail pre-synthesis may be relatively cheap (as when checking (B) or (D)),

or relatively costly (as when checking (F), for instance). Other properties may or may not be checked easily, depending on the circumstances. Therefore, we shall next give a list (in no particular order and without full proof) of non-structural properties which can be used for quick-fail purposes. All of them, except the last one, are consequences of properties (B), (D) and (F) described in proposition 1.

Some of them may be easier to check than (F). The last property mentioned in proposition 2 actually follows from proposition 1(G).

Proposition 2. More non-structural properties of pps nets Let N = (P, T, F, M0) be a pps net, let a, b, c be (not necessarily different) transitions in T , let M, M , K, . . . be reachable markings, and let w, v, u, . . . be sequences of transitions. Then the following properties are true: If M [w M [v M

for w, v ∈ T ∗ such that Ψ (w) = Ψ (v), then M = M = M .

If M [ab and M [ba and M [ac and M [bc , then M [c .

If M [a and M [b and K[ab , then M [ab and M [ba and K[ab and K[ba . If M [a M and M [b M , then M [b ⇐⇒ M [a .

If M [a M , M [b M , ¬M [ab , and ¬M [ba , then neither K[ab nor K[ba . If M [bu1 and M [u2 and Ψ (u1) = Ψ (u2) then M [u2b .

If M [bwa and M [av and Ψ (w) = Ψ (v), then M [avb If M [wvw and K[wv and Ψ (v) = Ψ (v ), then K[wv w .

If M [wvw

and K[wv and Ψ (v) = Ψ (v ) and w is a prefix of w, then K[wv w . If M [tvt , K[v K and Ψ (v) = Ψ (v ), then K [t .

If M [vwv , then for all reachable markings K such that K[vw K , we have K [v . If M [awa , then for all reachable markings K such that K[w K , we have K [a . If M [a and M [b and ¬M [ab , then neither K[ab nor K[ba .

If M [aua and M [ava then ¬K[awa for any w such that Ψ (w) = Ψ (u) + Ψ (v).

If ¬K[y and K[x K0[a1 . . . am Km with Ψ (a1 . . . am)(y) = 0, and if Kj [y for all 0 ≤ j ≤ m, then ¬Km[x .

If M [a , M [b , ¬M [ab and M [x u y , M [x v y for x , x , y , y then ¬K[x w y for x, y ∈ {a, b} and Ψ (w) = Ψ (u) + Ψ (v). ∈ {a, b} 2 3

The reachability graphs of safe marked graphs

In this section, we present a novel characterisation of the reachability graphs of safe, connected and live marked graphs, using the pps property (D) derived in the previous section. We first recall some of the results of [ 3 ]. Throughout the following (up to theorem 1), assume T S = (S, →, T, s0) to be a transition system which is finite, totally reachable, deterministic, persistent, and backward persistent, reversible, and satisfies P1. 3.1

Distances, lattices, and marked graph synthesis Definition 1. Short paths - definition 24 in [ 3 ]

Let r, s be two states of an lts. A path r[τ s will be called short if |τ | ≤ |τ | for every path r[τ s, where |τ | denotes the length of τ . 1

Lemma 1. Lemmata 25, 26, 27, and 28 of [ 3 ] • In TS , a path s[τ s is short iff, for some x ∈ T , Ψ (τ )(x) = 0. • If s[τ s and s[τ s are both short, then Ψ (τ ) = Ψ (τ ). • Suppose that s[τ s . Then Ψ (τ ) = Ψ (τ ) + m · 1, for some number m ∈ N, where s[τ s is any short path from s to s .

• There is a short path between any pair of reachable markings. 1

By lemma 1, the following definition is sound.

Definition 2. Distance - definition 29 of [ 3 ]

Let s, s be two states of TS , the Parikh vector of some short path from s to s

is called the distance between s and s , and denoted by Δs,s . 2 For x ∈ T , define x⊆ S × S by s

x s iff s[α s for some α ∈ (T \ {x})∗.

Proposition 3. Lattices - lemma 30 and 32, and proposition 31 of [ 3 ] • TS -x has state set S and label set T \ {x}; ( x \id ) is acyclic, and the paths of (TS -x, x) are precisely the short paths of TS not containing x. • For any label x ∈ T , (TS -x, x) is a complete lattice for the order x. • For every x ∈ T , there is a single state sx enabling only x, and a single state rx only produced by x, which are the top and bottom elements of (TS -x, x). 3 Lemma 2. Labels on short paths into sx - lemma 33 of [ 3 ] On any short path into sx, there is no label x.

Corollary 1. Properties of TS -x - corollary 34 of [ 3 ] (TS -x, x) is acyclic, weakly connected, and a complete lattice with a unique maximal state sx and a unique minimal state rx. 1

When a given lts TS is solved by an unlabelled Petri net [1], places should be

introduced in order to constrain the behaviour, and more precisely, in order to prevent the occurrence of some transition x in those states of TS that do not enable x. It is therefore reasonable to consider the set of states that do not enable x but for which x is necessarily enabled after one further step, as follows. Definition 3. Sequentialising states - definition 35 of [ 3 ] For any x ∈ T , Seq (x) = {s ∈ S | ¬s[x ∧ (∀a ∈ s• : s[ax )}. 2 3 Theorem 1. Marked graph synthesis - theorem 40 in [ 3 ] A labelled transition system T S is isomorphic to the reachability graph of a bounded, connected and live marked graph M G(T S) iff it is totally reachable, deterministic, persistent, backward persistent, reversible, finite, and satisfies P1. 1 [ 3 ] also contains a characterisation of the bound, as follows.

Proposition 4. Exact bounds – lemma 42 in [ 3 ] The bound of the marked graph MG (TS ) is max{Δsy,sx (y) | y ∈ T, sy ∈ Seq (x)}. 4 3.2

The state spaces of live and safe marked graphs

Our aim is to replace the indirect characterisation of the bound given by proposi

tion 4 by a direct one, using one of the properties derived in the previous section.

The lts depicted in figure 5 illustrates this idea.

Let us first see why the condition of proposition 4 – for bound 1 – is violated.

Consider the short path

It contains b twice. Moreover, sb ∈ Seq(a). According to theorem 1 and proposition 4, any marked graph Petri net solution must necessarily have a non-safe place with bound 2 leading from transition b to transition a. Note that there is also a short path containing a two times. However, this path is not indicative of an unsafe place from a to b, since sa ∈/ Seq(b).

We now show that, in order to characterise safeness, proposition 4 can essentially be replaced by condition (D), in the sense that the following two properties are equivalent for an lts T S:

1. T S is isomorphic to the reachability graph of a safe, connected and live

marked graph;

2. T S is totally reachable, deterministic, persistent, backward persistent, reversible, finite, and satisfies properties P1 and (D).

Since (1)⇒(2) is clear from the properties of live and safe marked graphs [5], and by part (D) of proposition 1, we only need to prove (2)⇒(1).

Lemma 3. (D) and the rest implies safe marked graph solvability Suppose that a transition system T S is totally reachable, deterministic, persistent, backward persistent, reversible, finite, and satisfies properties P1 and (D). Then the maximum in proposition 4 does not exceed 1.

Proof:

Consider a short path sy[y s[α sx, with sy ∈ Seq(x), which contains another y

in α. Consider the second y on such a path and an y-free prefix α of α with sy[y s[α s [y . By lemma 2, α (and thus α ) is x-free. Let M = s and K = sy.

Because K ∈ Seq(x), we get ¬K[x as well as K[yx . Along α , transition x

never gets disabled because it is not contained in α , and because of persistence.

Hence M [x . Thus, we get M [x and M [y and K[yx and ¬K[xy .

In other words, by contraposition, if the maximum in proposition 4 exceeds 1,

then ¬(D) holds true. This proves the claim. 3 To illustrate this lemma, we show how (D) is violated in figure 5. Consider x = a, y = b, K = 6, and M = 4. We have M [a and M [b , as well as K[ba . According to (D), we should also have K[ab , but contrariwise, ¬6[a in figure 5. Corollary 2. Characterisation of safe marked graphs A labelled transition system is isomorphic to the reachability graph of a safe, connected and live marked graph iff it is totally reachable, deterministic, persistent, backward persistent, reversible, finite, and satisfies P1 as well as (D). 2

The difference to theorem 1 is that, in addition, safeness is characterised by (D).

4

Concluding Remarks

In the first part of this paper, we have derived a collection of properties of plain, pure and safe Petri nets. The ambition is that these properties encompass (or imply) many generally known properties of pps nets and – by proxy – elementary nets, causing the resulting upper approximation of pps state spaces to be as tight as possible. In the second part of the paper, we have shown how these properties can contribute to the characterisation of a class of pps solvable transition systems, more precisely, transition systems solvable by live and safe marked graphs.

Our hopes for future work are twofold. It would be nice if the properties listed here can be usefully integrated in synthesis or pre-synthesis tools, for instance in order to allow sophisticated quick-fail mechanisms. Also, it would be nice if they could help in obtaining direct characterisations of the state spaces of net classes which are different from marked graphs, such as live and pps free-choice nets, or reversible, pps, persistent nets (though the difficulty of such a task should not be underestimated).

Acknowledgments

The authors would like to thank the reviewers for helpful comments.

A

Labelled transition systems and Petri nets

Definition 4. lts, reverse lts, reachability, Parikh vectors, cycles

A labelled transition system with initial state, abbreviated lts, is a quadruple

(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.3 For a label x ∈ T , the restricted lts TS -x is the lts (S, {(s, t, s ) ∈→| t = x}, T \{x}, s0) obtained by dropping all x-labelled transitions.

A label t is enabled in a state s, denoted by s[t , if there is some state s ∈ S

such that (s, t, s ) ∈→, and backward enabled in s, denoted by [t s, if there is some state s ∈ S such that (s , t, s) ∈→. For s ∈ S, let s• = {t ∈ T | s[t }.

For t ∈ T , s[t s iff (s, t, s ) ∈→, meaning that s is reachable from s through the

execution of t. The definitions of enabledness and of the reachability relation are extended to sequences σ ∈ T ∗: s[ε and s[ε s are always true; s[σt (s[σt s ) iff there is some s with s[σ s and s [t (s [t s , respectively). For any s ∈ S, [s = {s ∈ S | ∃σ ∈ T ∗ : s[σ s } denotes the set of states reachable from s. Two lts with the same label set, (S, →, T, s0) and (S , → , T, s0), will be called isomorphic if there is a bijection β : S → S such that s0 = β(s0) and (r, t, s) ∈→ iff (β(r), t, β(s)) ∈→ . 3 Formally, S can be considered as a set of vertices and → as a set of edges of a directed graph whose edges are labelled by letters from T . For a finite sequence σ ∈ T ∗ of labels, the Parikh vector Ψ (σ) is a T -vector (i.e., a vector of natural numbers with index set T ), where Ψ (σ)(t) denotes the number of occurrences of t in σ. s[σ s is called a cycle, or more precisely a cycle at (or around) state s, if s = s . The cycle is nontrivial if σ = ε. An lts is called acyclic if it has no nontrivial cycles. A nontrivial cycle s[σ s around a reachable state s ∈ [s0 is called small if there is no nontrivial cycle s [σ s with s ∈ [s0 and Ψ (σ ) Ψ (σ), where, by definition, equals (≤ ∩ =). An lts has property

P1 [3] if the Parikh vector of any small cycle in TS contains each transition exactly once. 4

If there is some sequence s[τ s leading from state s to state s , we sometimes wish to emphasise the intermediate states. In that case, we also express this, more explicitly, by an alternating sequence

s = q0t1q1t2 . . . qn−1tnqn = s meaning that τ = t1 . . . tn leads from s to s while visiting the intervening states q0, q1, . . . , qn, in that order.

Definition 5. Basic properties of an lts A labelled transition system (S, →, T, s0) is called • totally reachable if [s0 = S (i.e., every state is reachable from s0); • finite if S and T (hence also →) are finite sets; • deterministic, if for any states s, s , s ∈ [s0 and sequences σ, τ ∈ T ∗ with Ψ (σ) = Ψ (τ ): (s[σ s ∧ s[τ s ) ⇒ s = s and (s [σ s ∧ s [τ s) ⇒ s = s (i.e., from any one state, Parikh-equivalent sequences may not lead to two different successor states, nor come from two different predecessor states); • reversible if ∀s ∈ [s0 : s0 ∈ [s (i.e., s0 always remains reachable); • persistent [ 6 ] if for all reachable states s, s , s , and labels t, u, if s[t s and s[u s with t = u, then there is some (reachable) state r ∈ S such that both s [u r and s [t r (i.e., once two different labels are both enabled, neither can disable the other, and executing both, in any order, leads to the same state); • backward persistent if for all reachable states s, s , s , and labels t, u, if s [t s and s [u s and t = u, then there is some reachable state r ∈ S such that both r[u s and r[t s (i.e., persistence in backward direction). 5

If the lts is totally reachable, reversibility is the same as strong connectedness in the graph-theoretical sense.

Definition 6. Petri nets, markings, reachability graphs

A (finite, initially marked, place-transition, arc-weighted) Petri net is a tuple

N = (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, M0 is the initial marking, where a marking is a mapping M : P → N. A transition t ∈ T is enabled by a marking M , denoted by M [t , 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 defined by M (p) = M (p) − F (p, t) + F (t, p) (denoted by

M [t M ). The set of markings reachable from M is denoted [M . The reachability

graph of N , RG(N ), is the labelled transition system with the set of vertices [M0 and set of edges {(M, t, M ) | M, M ∈ [M0 ∧ M [t M }. A Petri net N solves a transition system T S, if RG(N ) and T S are isomorphic. 6 Definition 7. Basic structural properties of Petri nets For a place p of a Petri net N = (P, T, F, M0), let •p = {t ∈ T | F (t, p) > 0} and p• = {t ∈ T | F (p, t) > 0}. N is called connected if it is weakly connected as a graph; plain if cod(F ) ⊆ {0, 1}; pure or side-condition free if p• ∩ •p = ∅ for all places p ∈ P ; and a marked graph if N is plain and |p•| ≤ 1 and |•p| ≤ 1 for all places p ∈ P . For t ∈ T and w ∈ T ∗, let #t(w) = Ψ (w)(t) denote the number of times transition t occurs in w. The effect of a sequence w on a place p is ef p(w) = Ψ (w)(t) −

Ψ (w)(t) t∈•p

t∈p• i.e., the token difference w would generate on p if it were executed. For w ∈ T ∗, define w = {p ∈ P | ef p(w) < 0} and w = {p ∈ P | ef p(w) > 0}. 7 For the effect of w ∈ T ∗ on a given place p, there are exactly three, mutually exclusive, possibilities: • • • t∈T F (p, t) · #t(w) < 0. In that case, the effect of w on p is negative. t∈T F (p, t) · #t(w) > 0. In that case, the effect of w on p is positive. t∈T F (p, t) · #t(w) = 0. In that case, the effect of w on p is neutral.

In a pps net, when executing a sequence M [w M from a marking M to a marking

M , this specialises as follows, again with respect to a given place p: • #p• (w) = #•p(w) + 1. In that case, M (p) = 1 and M (p) = 0, and the effect of w on p is negative, more precisely, equal to −1. • #p• (w) = #•p(w) − 1. In that case, M (p) = 0 and M (p) = 1, and the effect of w on p is positive, more precisely, equal to +1. • #p• (w) = #•p(w). In that case, M (p) = M (p), and the effect of w on p is neutral, more precisely, equal to 0.

In general, let w (respectively, w ) denote the sets of places on which w has

a negative (respectively, positive) effect. Note that ε = ∅ = ε , since ε acts neutrally on any place. Also, if Ψ (w1) = Ψ (w2), then w1 = w2 and w1 = w2 .

This follows directly from the definitions, since for any place p, the number of

transitions of •p is the same in w1 as in w2, and similarly for the transitions in p•. Moreover, if M [wv M , then for every place p ∈ P the effect of wv on p is equal to the effect of w on p plus the effect of v on p (ef p(wv) = ef p(w)+ef p(v)). Also, if w and v are such that Ψ (w) = Ψ (w ) and Ψ (v) = Ψ (v ) then ef p(wv) = ef p(w ) + ef p(v ).

In the pps case, because of plainness and pureness, the

with the pre- and postset notation, more precisely: provided w = a ∈ T . Definition 8. Basic behavioural properties of Petri nets A Petri net N = (P, T, F, M0) is weakly live if ∀t ∈ T ∃M ∈ [M0 : M [t (i.e., there are no unfireable - hence dead, hence irrelevant - transitions); k-bounded for some fixed k ∈ N, if ∀M ∈ [M0 ∀p ∈ P : M (p) ≤ k (i.e., the number of tokens on any place never exceeds k); safe if it is 1-bounded; bounded if ∃k ∈

N : N is k-bounded; persistent (reversible) if its reachability graph is persistent

(reversible, respectively); and live if ∀t ∈ T ∀M ∈ [M0 ∃M ∈ [M : M [t (i.e., no transition can be made unfireable). Finally, N is called pps if it is plain, pure, and safe. 8 Proposition 5. Properties of Petri net reachability graphs The reachability graph RG of a Petri net N is totally reachable and deterministic. N is bounded iff RG is finite. 5 The class of pps (plain, pure, safe) Petri nets specified in definition 8 is very much related to elementary nets [ 10 ], in the following way. Elementary Petri nets have a strengthened firing rule: viz., t can occur if all its pre-places have exactly one token and all its post-places have exactly zero tokens. Every elementary net with this strengthed firing rule can be turned into an equivalent pps net with the usual firing rule, by adding appropriate complement places. Conversely, for pps nets, the two firing rules coincide.

References

1. E ´. Badouel , L. Bernardinello , P. Darondeau: Petri Net Synthesis. Springer-Verlag, ISBN 978-3-662-47966-7 , 339 pages ( 2015 ).

2. E. Best , P. Darondeau: Petri Net Distributability . In I. Virbitskaite, A . Voronkov (eds): PSI'11 , Novosibirsk , LNCS Vol. 7162 , Springer-Verlag, 1 - 18 ( 2011 ).

3. E. Best , R. Devillers: Characterisation of the State Spaces of Marked Graph Petri Nets . Selected extended papers of LATA'2014 . To appear in Information and Computation, A.H. Dediu et al. (eds), 20 pages ( 2016 or 2017 ).

4. W. Brauer , W. Reisig , G. Rozenberg (eds): Petri Nets: Central Models and their Properties, Lecture Notes in Computer Science Vol. 254 , Springer-Verlag, Berlin ( 1987 ).

5. F. Commoner , A.W. Holt , S. Even , A. Pnueli: Marked Directed Graphs . J. Comput. Syst. Sci. 5 ( 5 ): 511 - 523 ( 1971 ).

6. L.H. Landweber , E.L. Robertson : Properties of Conflict-Free and Persistent Petri Nets . JACM 25 ( 3 ), 352 - 364 ( 1978 ).

7. E. Ochman ´ski: Persistent Runs in Elementary Nets . FolCo Technical Report ( 2014 ).

8. L. Pomello , C. Simone: An Algebraic Characterisation of Elementary Net System (Observable) State Space . Formal Aspects of Computing 4 ( 6A ): 612 - 637 ( 1992 ).

9. G. Rozenberg: Behaviour of Elementary Net Systems . In [4] , 60 - 94 ( 1987 ).

10. G. Rozenberg, J. Engelfriet: Elementary Net Systems . In Lectures on Petri Nets I: Basic Models , Advances in Petri Nets, W. Reisig , G. Rozenberg (eds), SpringerVerlag, LNCS Vol. 1491 , 12 - 121 ( 1998 ).

11. U. Schlachter: Petri Net Synthesis in Restricted Classes of Nets . Proc. ICATPN' 2016 , Torun´, Poland, to appear in Springer LNCS ( 2016 ). See also https://github.com/CvO-Theory/apt ( 2013 ).