The Individual and Collective Token Interpretations of Petri Nets

Rob van Glabbeek

National ICT Australia and School of Computer Science and Engineering The University of New South Wales

                           rvg@cs.stanford.edu

Abstract. Starting from the opinion that the standard firing rule of Petri nets embodies the collective token interpretation of nets rather than their individual token interpretation, I propose a new firing rule that embodies the latter. Also variants of both firing rules for the selfsequential interpretation of nets are studied. Using these rules, I express the four computational interpretations of Petri nets by semantic mappings from nets to labelled step transition systems, the latter being event-oriented representations of higher dimensional automata. This paper totally orders the expressive power of the four interpretations, measured in terms of the classes of labelled step transition systems up to isomorphism of reachable parts that can be denoted by nets under each of the interpretations. Furthermore, I extend the unfolding construction of place/transition nets into occurrence net to nets that may have transitions without incoming arcs.

Introduction

In the literature on Petri nets 2 × 2 = 4 computational interpretations of nets can be distinguished, that in Van Glabbeek & Plotkin [6] were called the individual token and the collective token interpretation, and, orthogonally, the self-sequential and the self-concurrent interpretation. The differences show up only when dealing with non-safe place/transition nets and, as far as the individual/collective token dichotomy concerns, only when precisely keeping track of causal dependencies between action occurrences.

The individual token interpretation has been formalised by the notion of a process, described in Goltz & Reisig [7]. A causality respecting bisimulation relation based on this approach was proposed by Best, Devillers, Kiehn & Pomello [3] under the name fully concurrent bisimulation. Engelfriet [4] and Meseguer et al. [8] define an unfolding of Petri nets into occurrence nets that preserves this interpretation. Best & Devillers [2] adapted the process concept of [7] to fit the collective token philosophy. Equivalence relations on Petri nets based on the collective token interpretation were proposed in [6].

In older papers on Petri nets a multiset of transitions was allowed to fire only if it was a set, i.e., no transition could fire multiple times concurrent with itself. The argument for this restriction was that a transition can be thought of as a subsystem like a printer, that can only print one file at a time. When there are enough tokens in its preplaces (representing print-requests and other preconditions for printing) to handle two files, these have to be printed one by one. Goltz & Reisig [7] exemplified that not all subsystems suffer from such limitations; when one does, this is a matter of scarcity of recourses that can be modelled by an extra place. Since [7] multisets are generally allowed to fire. Nevertheless, for the sake of completeness, I take both interpretations into account.

The present work can be understood as a way of formally pinpointing the differences between these computational interpretations. This is done by formulating four different firing rules, and by giving four translations from Petri nets into labelled step transition systems, one for each interpretation. Labelled step transition systems arose from discussions with Vaughan Pratt in 1991 as an event-oriented representation of higher dimensional automata [10], an angle that will not be pursued here. Step transition systems were used to describe the operational behaviour of Petri nets in Mukund [9]. In the form proposed here, but without the labelling, they appear in Badouel [1].

I compare the expressive power of classes of Petri nets under each of the four interpretations in terms of the labelled step transition systems they can denote up to isomorphism of reachable parts, and find that the class of all Petri nets under either one of the individual token interpretations is equally expressive as a subclass of nets on which all four interpretations coincide. Likewise, the class of all Petri nets under the self-concurrent collective token interpretation is equally expressive as a subclass of nets on which both collective token interpretations coincide. This gives rise to the following hierarchy:

[figure: self-sequential individual token interpretation; self-concurrent individual token interpretation; self-sequential collective token interpretation; self-concurrent collective token interpretation]

Fig. 1. Relative expressiveness of four computational interpretations of Petri nets

The expressiveness results above were first claimed by me in [5], using a different model of higher dimensional automata for interpreting the dynamic behaviour of Petri nets, namely cubical sets instead of labelled step transition systems. However, the individual token interpretations of [5] apply to standard nets only, nets in which each transition has at least one incoming arc, and a proof is given for the expressiveness result relating the two self-concurrent interpretations only.

As a spin-off, this study provides a particularly simple definition of the unfolding of an arbitrary place/transition net into an occurrence net. My construction extends the constructions of [11], [4] and [8] by including non-standard nets.

1 Petri Nets and the Firing Rule

Definition 1. A (labelled, marked) Petri net is a tuple (S, T, F, I, l) with

– S and T two disjoint sets of places (Stellen in German) and transitions,

– F : (S × T ∪ T × S) → IN, the flow relation,

– I : S → IN, the initial marking,

– and l : T → A, for A a set of actions, the labelling function.

Petri nets are pictured by drawing the places as circles and the transitions as boxes, containing their label. For x,y ∈ S ∪T there are F (s, t) arcs from x to y. When a Petri net represents a concurrent system, a global state of this system is given as a marking, a function M : S → IN. Such a state is depicted by placing M(s) dots (tokens) in each place s. The initial state is given by the marking I. In order to describe the behaviour of a net, one defines the step transition relation between markings.

Definition 2. A multiset over a set S is a function M : S → IN, i.e. M ∈ IN^{S}. For multisets M and N over S write M ≤ N if M(s) ≤ N(s) for all s ∈ S. M + N ∈ IN^{S} is the multiset with (M + N)(s) = M(s) + N(s), and M − N is the function given by (M − N)(s) = M(s) − N(s)—it is not always a multiset. The function 0 : S → IN given by 0(s) = 0 for all s ∈ S is the empty multiset. A multiset M ∈ IN^{S} with M(s) ≤ 1 for all s ∈ S is identified with the set {s ∈ S | M(s) = 1}. A multiset M over S is finite if {s ∈ S | M(s) > 0} is finite. Let ℳ(S) denote the collection of finite multisets over S.

Definition 3. For a finite multiset U : T → IN of transitions in a Petri net, let •U, U^{•} : S → IN be the multisets of input and output places of U, given by

•U(s) = ∑_{t∈T} F (s, t) · U(t) and U^{•}(s) = ∑_{t∈T} U(t) · F (t, s) for all s ∈ S.

U is enabled under a marking M if ^{•}U ≤ M. In that case U can fire under M, yielding the marking M′ = M −^{•}U + U^{•}, written M ⟶^{U} M′.

If a multiset U of transitions fires, for every transition t in U and every arc from a place s to t, a token moves along that arc from s to t. These tokens are consumed by the firing, but also new tokens are created, namely one for every outgoing arc of t. These end up in the places at the end of those arcs. If t occurs several times in U, all this happens several times (in parallel) as well. The firing of U is only possible if there are sufficiently many tokens in the preplaces of U (the places where the incoming arcs come from).

The components of a net N are called S^{N}, T^{N}, F^{N}, I^{N} and l^{N}, a convention that also applies to other structures given as tuples. When clear from context, the index N is omitted.

Two nets P and Q are isomorphic, written P ≅ Q, if they differ only in the names of their places and transitions, i.e. if there are bijections β : S^{P} → S^{Q} and η : T^{P} → T^{Q} such that, for s ∈ S^{P} and t ∈ T^{P}: I^{Q}(β(s)) = I^{P}(s), F^{Q}(β(s), η(t)) = F^{P}(s, t), F^{Q}(η(t), β(s)) = F^{P}(t, s) and l^{Q}(η(t)) = l^{P}(t).

2 The Individual and Collective Token Interpretations

In the individual token interpretation of Petri nets one distinguishes different tokens residing in the same place, keeping track of where they come from. If a transition fires by using a token that has been produced by another transition, there is a causal link between the two. Consequently, the causal relations between the transitions in a run of a net can always be described by means of a partial order. In the collective token interpretation, on the other hand, tokens cannot be distinguished: if there are two tokens in a place, all that is present there is the number 2. This gives rise to more subtle causal relationships between transitions in a run of a net, which cannot be expressed by partial orders.

The following example illustrates the difference between the two interpreta-

tions. A:  •  a  •  b  •

In this net, the transitions labelled a and b can fire once each. After a has fired, there are two tokens in the middle place. According to the individual token philosophy, it makes a difference which of these tokens is used in firing b. If the token that was there already is used (which must certainly be the case if b happens before the token from a arrives), the transitions a and b are causally independent. If the token that was produced by a is used, b is causally dependent on a. Thus, the net A above has two maximal executions, that can be characterised by the partial orders \begin{matrix}a \\ b \end{matrix} and a \overline{}b. According to the collective token philosophy on the other hand, all that is present in the middle place after the occurrence of a is the number 2. The preconditions for b to fire do not change, and consequently b is always causally independent of a.

The following illustrates that both philosophies yield incomparable notions of equivalence.

B:  •  a  •  b  •

In the collective token philosophy the precondition of b expressed by the place in the middle is redundant, and hence A must be equivalent to B. However, A and B are not fully concurrent bisimulation equivalent (a causality respecting equivalence based on the individual token approach [3]), as B lacks the execution a \overline{}b. On the other hand, A is fully concurrent bisimulation equivalent with

C below. C:  •  a  b  • b •

In fact, C is the occurrence net obtained from A by the unfolding of [4, 8]. In the individual token philosophy, both A and C have the executions a \overline{}b and \begin{aligned}a \\ & b \end{aligned}. However, in the collective token philosophy A does not have a run a \overline{}b and can therefore not be equivalent to C in any causality preserving way.

• H_{CT}(D) ∘ a ∘ c  ∘ b b c ∘ b a bc  ∘ b ∘ a c a c a  c D • a  •b •  • H_{IT}(D) ∘ a ∘ c_{a} ∘ b b c_{a} ∘ b a b c_{a}  ∘ b  ∘ a  c_{b} ∘ c_{b} a c_{b} a

The Petri net D above (ignore H_{CT}(D) and H_{IT}(D) for now) illustrates how the collective token interpretation gives rise to causal relationships that cannot be expressed by partial orders. Under the collective token interpretation this net features disjunctive causality: c is causally dependent on a ∨ b. In contrast, under the individual token interpretation D admits two executions, one in which c depends only on a, and one in which c depends only on b.

Antoni Mazurkiewicz once argued for the collective reading of this net by letting a and b be £1 contributions of two school children to buy a present for their teacher. The act of buying the present, which only costs £1, is represented by c. Now the individual token interpretation suggests that the present is bought from the contribution from either one child or the other, whereas the collective token interpretation admits only one complete execution, in which the buying of the present is caused by the disjunction of the two contributions. The latter would be a fairer description of the intended state of affairs.

3 A Firing Rule for the Individual Token Interpretation

In my opinion, the standard definition of a marking and the corresponding firing rule (Def. 3) embody the collective token interpretation rather than the individual one. Here I will redefine these concepts in a way that embodies the individual token interpretation. To this end I define the notion of a token as it could occur in a Petri net, in such a way that all possible token occurrences have a different name. A token will be a triple (t′, k, s), with s the place where the token occurs, and t′ the transition firing that brought it there. For tokens that are in s initially, I take t′ = ∗. When the number of tokens that t′ deposits in s in n, I distinguish these tokens by giving them ordinal numbers k = 0, 1, 2, …, n−1. In order to define tokens as announced above I need to define transition firings simultaneously. These will be pairs (X, t) with t the transition that fires, and X the set of tokens that is consumed in the firing. Transitions t that can fire without consuming tokens can fire multiple times on the same (empty) input; these firings will be called (k, t) with k ∈ IN instead of (∅, t). I define the functions β from tokens to the places where they occur by β(x, k, s) = s, and η from transition firings to the transition that fires by η(x, t) = t. The function β extends to a function from sets of tokens X to multisets of places β(X) : S → IN, by β(X)(s) = |{s′ ∈ X | β(s′) = s}|.

Definition 4. Given a Petri net N = (S, T, F, I, l), the sets of tokens S_{•} and transition firings T_{•} of N are recursively defined by

– (∗, k, s) ∈ S_{•} for s ∈ S and k < I(s);

– (t′, k, s) ∈ S_{•} for s ∈ S, t′ ∈ T_{•} and k < F (η(t′), s);

– (X, t) ∈ T_{•} for t ∈ T and X ⊆ S_{•} such that β(X) = ^{•}t ≠ 0;

– (k, t) ∈ T_{•} for k ∈ IN and t ∈ T such that ^{•}t = 0.

The labelling function l_{•}: T_{•} → A on transition firings is given by l_{•}(t) = l(η(t)). An individual marking of N is a multiset M : S_{•} → IN of tokens. The initial individual marking I_{•}: S_{•} → IN is given by I_{•}(∗, k, s) = 1 and I_{•}(t′, k, s) = 0.

Standard Nets. A standard net is a net N in which each transition has at least one incoming arc: ∀t ∈ T. ^{•}t > 0. A net is standard iff its set of spontaneous transition firings T_{∘} = {(k, t) ∈ T_{•} | k ∈ IN} is empty. I define the firing rule embodying the individual token interpretation for standard nets first.

Definition 5. For a finite set U ⊆ T_{•} of transition firings in a standard net, let

•U = ∑_{(X,t)∈U}X and U^{•} = {(t′, k, s) | t′ ∈ U ∧ k < F (η(t′), s)}

be the multiset of input tokens and the set of output tokens of U. The set U is enabled under an individual marking M ∈ IN^{S_{•}} if ^{•}U ≤ M. In that case U can fire under M, yielding M′ = M −^{•}U + U^{•} ∈ IN^{S_{•}}, written M ⟶^{U}_{•} M′. A chain I_{•} ⟶^{U_{1}}_{•} M_{1} ⟶^{U_{2}}_{•} ⋯ ⟶^{U_{n}}_{•} M_{n} is called a firing sequence. An individual marking M ∈ IN^{S_{•}} is reachable if there is such a sequence ending in M = M_{n}.

The following proposition says that I succeeded in giving all possible token occurrences a different name.

Proposition 1. In a standard net, any reachable multiset of tokens is a set.

Proof. I show that in a firing sequence I_{•} ⟶^{U_{1}}_{•} M_{1} ⟶^{U_{2}}_{•} ⋯ ⟶^{U_{n}}_{•} M_{n} the multiset I_{•} + ∑_{i=1}^{n} U_{i}^{•}, which includes M_{n}, is a set. Applying induction on n, the base case holds by the definition of I_{•}. For the induction step, if a token occurs twice in I_{•} + ∑_{i=1}^{n} U_{i}^{•}, the definitions of I_{•} and U^{•} imply that it has the form (t′, k, s), hence the transition firing t′ occurs twice in ∑_{i=1}^{n} U_{i}. As t′ is not spontaneous, it has the form (X, t) with X a nonempty set of tokens. By the definition of ^{•}U, a token in X occurs twice in I_{•} + ∑_{i=1}^{n−1} U_{i}^{•}. ⊓ ⊔

Prop. 1 also shows that there is no point in upgrading Def. 5 to multisets U.

Non-standard Nets. For arbitrary nets, the definition of U^{•}, for U a finite set of transitions, remains the same, but in the definition of ^{•}U one needs to decide on the input conditions of spontaneous transition firings. The simplest solution would be to treat k as ∅ in the definition of ^{•}U or, equivalently, to let the sum range over the non-spontaneous transition firings in U only. However, this would lead to a failure of Prop. 1 for non-standard nets, as a spontaneous transition firing (k, t) could occur multiple times in a firing sequence, leaving multiple copies of its output tokens in the resulting reachable marking. A solution for this problem would be to upgrade the definition of a firing sequence with the requirement that each spontaneous transition firing may only occur once in it. This condition would be motivated by the idea that every time a transition t with ^{•}t = 0 fires, its firing gets a different identifier.

Here I aim at the same result by using a notion of state that consists of an individual marking, together with the set names of spontaneous transition firings that may still fire. I could just as well have taken the set of spontaneous transition firings that have already occurred, this set being equally rich in information content, but the choice above allows me to combine both components of a state into one set of resources that need to be available for transition firings to occur.

Definition 6. Let N be a Petri net. Let S_{•}^{+} = S_{•} ∪{t_{k} | (k, t)∈T_{∘}} be the set of resources of N. An individual state M ∈ IN^{S_{•}^{+}} of N is the union of an individual marking and a multiset of names t_{k} of spontaneous transition firings (k, t). The initial state I_{•}^{+} = {(∗, k, s) | k < I(s)} ∪ {t_{k} | (k, t) ∈ T_{∘}} is the union of I_{•} and the set of names of all spontaneous transition firings. The multiset of input resources of a finite set of transition firings U ⊆ T_{•} is given by

•U = ∑_{(X,t)∈U−T_{∘}} X + {t_{k} | (k, t) ∈ U ∩ T_{∘}}.

All other elements of Def. 5 apply unchanged, but using individual states instead of individual markings, and I_{•}^{+} instead of I_{•}.

Corollary 1. In any Petri net, all reachable individual states are sets.

4 The Individual and Collective Firing Rules Agree

Having defined a new firing rule that caters to the individual token interpretation, I now show how it is consistent with the standard firing rule of Definition 3. I use variables M_{•} to range over individual states, and U_{•} to range over sets of transition firings. The function η from transition firings to the transition that fires extends to a function from sets of transition firings U_{•} to multisets of transitions η(U_{•}) : T → IN, by η(U_{•})(t) = |{t′ ∈ U_{•} | η(t′) = t}|. Moreover, the function β from tokens to the places where they occur extends to a function from individual states (multisets of resources) to markings (multisets of places) by β(M_{•})(s) = ∑_{s′∈β^{−1}(s)} M_{•}(s′) (where non-token resources are ignored).

Now the following theorem, whose proof is trivial, says that the functions β and η constitute a bisimulation between the step transition relations of a given net under the individual and collective token interpretations.

Theorem 1. β(I_{•}^{+}) = I and for any individual states M_{•} and markings M′:

β(M_{•}) ⟶^{U} M′ ⇔ ∃U_{•}, M′_{•} : M_{•} ⟶^{U_{•}}_{•} M′_{•} ∧ η(U_{•}) = U ∧ β(M′_{•}) = M′.

5 Firing Rules for the Self-sequential Interpretations

The firing rules of Sections 1 and 3 embody the self-concurrent interpretations of Petri nets, allowing a transition to fire concurrently with itself. Here I investigate how they need to be adapted to obtain firing rules for the self-sequential interpretations, excluding transitions from firing concurrently with themselves.

The firing rule for the self-sequential collective token interpretation is evident: a multiset U of transitions is enabled under the self-sequential interpretation of nets if it is enabled in the sense of Def. 3 and U is a set. The self-sequential step transition relation →^{ss} between markings is given by M⟶^{U}^{ss}M′ iff M ⟶^{U} M′ and U is a set.

On standard nets, a firing rule for the self-sequential individual token interpretation can be obtained in the same way: a multiset U of transition firings is enabled under the self-sequential interpretation of nets if it is enabled in the sense of Def. 5 and U is a set with the property that if (X, t), (Y, t) ∈ U for t ∈ T then X = Y. Thus, all transition firings in U should be firings of different transitions. One defines →_{•}^{ss} by imposing the same requirement.

On non-standard nets, before employing the same definitions, I take the opportunity to rectify an unfortunate design decision that was unavoidable under the self-concurrent interpretation. Namely, if a net contains a transition t without input places, Def. 6 yields an infinitely branching transition relation: there

is a transition I_{•} ⟶^{{(k,t)}}_{•} M_{(k,t)} for any k ∈ IN. The reason this was unavoidable under the self-concurrent interpretation is that any number of transition firings (k, t) can happen simultaneously, and I want to preserve the fundamental property of Petri nets that whenever a number of transition firings can happen in one step, they can happen in any order; so any of the firings (k, t) can happen first. Under the self-sequential interpretation, on the other hand, it is much more natural so take the point of view that although the transition t allows arbitrary many firings to occur sequentially, there is no point in distinguishing different kinds of first firings. Thus, I will use k not merely as a label taken from an arbitrary countable set, but as an actual number, (k, t) denoting the k+1^{th} firing of transition t. The set S_{•}^{+} of resources of a net and the individual states M ∈ IN^{S_{•}^{+}} are as in Def. 6, but this time the presence of t_{k} in a state signifies that the k+1^{th} firing of t is enabled. The multiset of input resources remains the same as in Def. 6, but the notions of initial state and output resources need to be adapted.

Definition 7. Let N be a Petri net. The initial state of N under the selfsequential interpretation is I_{•}^{ss} = {(∗, k, s) | k < I(s)} ∪ {t_{0} | t∈T ∧^{•} t = 0}, and the set of output resources of a finite set of transition firings U ⊆ T_{•} is

U_{ss}^{•} = {(t′, k, s) | t′ ∈ U ∧ k < F (η(t′), s)} ∪ {t_{k+1} | (k, t) ∈ U ∩ T_{∘}}.

The set U is enabled in an individual state M: S_{•}^{+} → IN under the self-sequential interpretation if ^{•}U ≤ M and ∀t((x, t), (y, t) ∈ U ⇒ x = y). In that case U can fire under M, yielding the state M′ = M −^{•}U + U_{ss}^{•}, written M ⟶^{U}_{•}^{ss}M′.

Again, it is trivial to check that all →_{•}^{ss}-reachable individual states are sets, and β and η constitute a bisimulation between the step transition relations of a net under the self-sequential individual and collective token interpretations.

Theorem 2. β(I_{•}^{ss}) = I and for any individual states M_{•} and markings M′:

β(M_{•})⟶^{U}^{ss}M′ ⇔ ∃U_{•}, M′_{•} : M_{•}⟶^{U_{•}}_{•}^{ss}M′_{•} ∧ η(U_{•}) = U ∧ β(M′_{•}) = M′.

6 Labelled Step Transition Systems

Definition 8. A labelled step transition system is a tuple (Q, E, →, I, l) with – Q and E are two disjoint sets of states and events,

– → ⊆ Q × ℳ(E) × Q, the step transition relation, satisfying

(1) if (p, u, q), (p, u, q′) ∈ → then q = q′  (determinism)
(2) (p, 0, p) ∈ →  (trivial step)
(3) if (p, u + v, r) ∈ → then ∃q : (p, u, q), (q, v, r) ∈ → (asynchronousness)

– I ∈ Q, the initial state,

– and l : E → A, for A a set of actions, the labelling function. Henceforth, write p ⟶^{u} q for (p, u, q) ∈ →.

Notes. A labelled transition system (LTS) is a quadruple (Q, Σ, →, I) with Q a set of states, Σ a set of labels, → ⊆ Q×Σ×Q, and I ∈ Q. An LTS is deterministic, if it satisfies (1) above; in that case the transition relation → is really a partial function from Q × Σ to Q. A step transition system is an LTS whose labels are sets or multisets of actions, rather than single actions. Here p ⟶^{u} q means that the represented system can transition from state p to state q by performing the actions in u in one step, meaning simultaneously or concurrently. Property (2) says that in any state p it is possible to do nothing and stay in p. Together with (1), property (2) implies that p ⟶^{0} q iff q = p, so without performing actions it is not possible to move to another state. The information content would be the same if in Def. 8 instead of (2) it would be required that transitions are labelled by nonempty multisets.

A step transition system is asynchronous if it satisfies (3). This requirement represents the postulate that different action occurrences do not synchronise in any way; they can happen simultaneously only if they are causality independent, and in that case they can also happen in any order.

Now a labelled step transition system (LSTS) is a doubly labelled transition system. First of all the arrows are labelled by sets of events, and secondly the events are labelled by actions. This double layer of labelling is reflected in the name, as the word “step” already implies “labelled”. The creation of events as an intermediate concept between transitions and actions is a trick that allows me to control the non-determinism of concurrent systems on the level of actions. I want to be able to model that a system in state p has a choice between two a-actions, leading to different successor states, and at the level of abstraction at which the system is represented there is no way to tell the two as apart (or influence the choice). However, optionally based on the belief that the world is not truly nondeterministic, the nondeterminism can be attributed to a difference between the two a actions that, although not observable, does account for the fact that they lead to different successor states. An event is now an action together with all its subtle qualities that influence which state it leads to when executed in a given state. Thus, an action is an equivalence class of events that are indistinguishable at the chosen level of abstraction.

When used for representing concurrent systems, LSTSs need to be considered modulo a suitable semantic equivalence. One the finest possible candidates is the following notion of isomorphism of reachable parts, ≅_{R}:

Definition 9. Two LSTSs A and B are isomorphic, written A ≅ B, if they differ only in the names of their states and events, i.e. if there are bijections β : Q^{A} → Q^{B} and η : E^{A} → E^{B} such that β(I^{A}) = I^{B}, and, for p, q ∈ Q^{A}, u : E^{A} → IN and e∈E^{A}: β(p) ⟶^{η(u)} β(q) iff p ⟶^{u} q and l^{B}(η(e)) = l^{A}(e).

The set R(Q) of reachable states in A = (Q, E, →, I, l) is the smallest set such that I is reachable and whenever p is reachable and p ⟶^{u} q then q is reachable. The reachable part of A is the LSTS R(A) = (R(Q), E, →^{\}R(Q), I, l).

Write A ≅_{R} B if R(A) and R(B) are isomorphic.

To check A ≅_{R} B it suffices to restrict to subsets of Q^{A} and Q^{B} that contain all reachable states, and construct an isomorphism between the resulting LSTSs.

7 Interpreting Petri Nets in LSTSs

I now give four translations from Petri nets into labelled step transition systems, one for each of the computational interpretations of this paper. This is a way of formally pinpointing the differences between these interpretations; it amounts to giving four different semantics of Petri nets.

Definition 10. Let N = (S, T, F, I, l) be a net. Then H_{CT}(N) = (IN^{S}, T, →, I, l) is the LSTS associated to N under the self-concurrent collective token interpretation, and H_{IT}(N) = (IN^{S_{•}^{+}}, T_{•}, →_{•}, I_{•}^{+}, l_{•}) is the LSTS associated to N under the self-concurrent collective token interpretation. H_{CT}^{ss}(N) = (IN^{S}, T, →^{ss}, I, l) and H_{IT}^{ss}(N) = (IN^{S_{•}^{+}}, T_{•}, →_{•}^{ss}, I_{•}^{ss}, l_{•}) are the LSTSs associated to N under the self-sequential interpretations.

Example 1. The LSTSs below express the collective and individual token interpretation of the net A from Sect. 2, respectively. The equivalence of A and B

H_{CT}(A) ≅_{R} H_{CT}(B) ≅_{R} H_{IT}(B) • ∘ a ∘ b a b  ∘ b a  H_{IT}(A) ≅_{R} H_{IT}(C) ≅_{R} H_{CT}(C) • ∘ a ∘ b_{a}  ∘ b_{∗} a b_{∗} ∘ b_{∗} a

under the collective token interpretation, and of A and C under the individual token interpretation, manifests itself as isomorphism of reachable parts of the associated LSTSs.

The pictures above display LSTSs up to isomorphism of reachable parts. Letters like b_{a} and b_{∗} stand for “different events labelled b”. In fact, if the places of A are called s_{1}, s_{2} and s_{3}, respectively, and its transitions a and b, then the event b_{∗} is ({(∗, 0, s_{2}), (∗, 0, s_{3})}, b), whereas b_{a} = ({(({(∗, 0, s_{1})}, a), 0, s_{2}), (∗, 0, s_{3})}, b).

Example 2. The LSTSs associated to the net D of Sect. 2 under the the collective and individual token interpretations can be found right next to it.

Example 3. In the previous examples there was no difference between the selfsequential and the self-concurrent interpretations. The following shows, however, that in general all four interpretations yield a different result.

•• a E  • H_{IT}(E) : ∘ a_{0} ∘ a_{1}a_{0} a_{1} ∘ a_{1} a_{0}  • H_{IT}^{ss}(E) : ∘ a_{0} ∘ a_{1}  ∘ a_{1} a_{0} • H_{CT}(E) : ∘ a ∘ a a a  • H_{CT}^{ss}(E) : ∘ a ∘ a

8 The Relative Expressiveness of the Four Interpretations

Each of the four computational interpretations above makes a different model of concurrency out of Petri nets. These models can now be compared with respect to their expressive power in denoting labelled step transition systems.

8.1 The Individual versus Collective Token Interpretations

The following theorem says that Petri nets under the self-concurrent collective token interpretation are at least as expressive as Petri nets under the selfconcurrent individual token interpretation, in the sense that any LSTS that can be denoted by a net under the latter interpretation can also be a denoted by a net under the former interpretation. On the other hand, the LSTS H_{CT}(D) in Sect. 2 cannot be denoted by a Petri net under the individual token interpretation.

Theorem 3. For every net N there is a net N_{•} such that H_{CT}(N_{•}) = H_{IT}(N).

Proof. N_{•} = (S_{•}^{+}, T_{•}, F_{•}, I_{•}^{+}, l_{•}) with S_{•}^{+}, T_{•}, I_{•}^{+} and l_{•} as in Def. 4 and 6, and – F_{•}(s′, t′) = 1 if t′ = (X, t) with s′ ∈ X, or t′ = (k, t) ∈ T_{∘} and s′ = t_{k};

F_{•}(s′, t′) = 0 otherwise;

– F_{•}(t′, s′) = 1 if s′ has the form (t′, k, s); F_{•}(t′, s′) = 0 otherwise. That H_{CT}(N_{•}) = H_{IT}(N) is straightforward. ⊓ ⊔

The net N_{•} constructed above is a close relative of the unfolding of a Petri net into an occurrence net, as defined in [11, 4, 8] (see Sect. 9). The difference is that I have not bothered to eliminate unreachable places and transitions.

8.2 The Self-sequential versus Self-concurrent Interpretations

In general, results as strong as the one above can not be obtained: in order to compare expressiveness in a meaningful way, processes represented by LSTSs, Petri nets, or other models of concurrency should be regarded modulo some semantic equivalence relation. A particularly fine equivalence relation that allows me to totally order the computational interpretations of Petri nets is isomorphism of reachable parts of LSTSs (see Def. 9 in Sect. 6).

The following theorem shows that the behaviour of nets under the selfsequential interpretations can easily be encoded into the behaviour of nets under the corresponding self-concurrent interpretation.

Theorem 4. For every net N there is a net N^{ss} such that H_{CT}(N^{ss}) ≅_{R} H_{CT}^{ss}(N) and H_{IT}(N^{ss}) ≅_{R} H_{IT}^{ss}(N).

Proof. Following [7], N^{ss} is obtained from N by adding for every transition t a self-loop, consisting of a place s_{t} with I(s_{t}) = F (s_{t}, t) = F (t, s_{t}) = 1 and F (s_{t}, u) = F (u, s_{t}) = 0 for all u ≠ t. Write S_{new} for the set of new places s_{t}.

To check that H_{CT}(N^{ss}) ≅_{R} H_{CT}^{ss}(N), restrict the states of H_{CT}(N^{ss}), i.e. the markings M of N^{ss}, to the ones with M(s_{t}) = 1 for all s_{t} ∈S_{new}; this set of states surely contains all reachable ones. Let \overline{β}(M)∈ IN^{S} be obtained by restricting the domain of M ∈ IN^{S∪S_{new}} to S, and \overline{η} be the identity. Now the bijections \overline{β} and \overline{η} constitute an isomorphism of reachable parts between H_{CT}(N^{ss}) and H_{CT}^{ss}(N).

To check that H_{IT}(N^{ss}) ≅_{R} H_{IT}^{ss}(N), restrict the states of H_{IT}(N^{ss}) to the individual states M_{•} of N^{ss} that contain exactly one token of the form (x, 0, s_{t}) for each s_{t} ∈ S_{new}; this set of states surely contains all reachable ones. Also, in view of Cor. 1, the states of H_{IT}(N^{ss}) and H_{IT}^{ss}(N) may be restricted to sets of resources rather than multisets. Let S_{∘} = {s_{t} ∈S_{new} | ^{•}t = 0 (in N)}. For s_{t} ∈S_{∘}, let s_{t}^{0} = (∗, 0, s_{t}) and s_{t}^{k+1} = (({s_{t}^{k}}, t), 0, s_{t}). Then all tokens (x, k, s_{t}) of N^{ss} are of the form s_{t}^{k} for k ∈ IN. Now the mappings \overline{η} from the transition firings in N^{ss} to the transition firings in N, for convenience extended with \overline{η}(∗) = ∗, and \overline{β} from sets of individual tokens in N^{ss} to sets of individual resources in N, are defined with recursion on the structure of transition firings and sets of tokens

by \overline{η}(X, t) = \begin{cases}(\overline{β}(X), t) if & ^{•}t ≠ 0 \\ (k, t) if & ^{•}t = 0 ∧ X = \{s_{t}^{k}\} \end{cases}

and \overline{β}(X) = \{(\overline{η}(x), k, s) | (x, k, s)∈X ∧ s∉S_{new}\} ∪ \{t_{k} | s_{t}^{k} ∈X ∧ s_{t} ∈S_{∘}\}.

Again, the bijections \overline{β} and \overline{η} constitute an isomorphism between the reachable parts of H_{IT}(N^{ss}) and H_{IT}^{ss}(N). ⊓ ⊔

The construction of N^{ss} above, reducing the self-sequential to the self-concurrent interpretation of nets is well known [7]. The point of the proof above is to some extent just a sanity check on the definitions of H_{CT}, H_{CT}^{ss}, H_{IT} and H_{IT}^{ss}.

By Theorem 4, any LSTS that can be denoted by a Petri nets under the selfsequential collective token interpretation, can also be denoted by a net under the self-concurrent collective token interpretation, and likewise for nets under the individual token interpretations. On the other hand, the LSTS H_{CT}(E) of Example 3 cannot be denoted by a Petri net under the self-sequential collective token interpretation.

8.3 Subsumption

So far, I proved the expressiveness results H_{IT}^{ss} ⪯ H_{IT} ≺ H_{CT} ≻ H_{CT}^{ss}, where J ≺ K means that up to ≅_{R} the class of LSTSs that can be denoted by Petri nets under the computational interpretation J is a proper subclass of the class that can be denoted by Petri nets under the computational interpretation K. Here I will strengthen and augment these results by considering the following subsumption relation between computational interpretations and classes of nets.

Definition 11. Write J ⪯_{C} K if C is a class of Petri nets such that

– for any net N ∈ C one has J (N) ≅_{R} K(N) and

– for any net N there is a net N′ ∈ C such that J (N′) ≅_{R} J (N).

If J ⪯_{C} K, then up to ≅_{R}, the class of all Petri nets under interpretation J is equally expressive as the subclass C on which the two interpretations coincide.

Observation 1. If J ⪯_{C} K ⪯_{D} L and C ⊆ D then J ⪯_{C} L.

Observation 2. If J ⪯_{C} K ⪯_{C} L then K ⪯_{C} J.

Moreover, J ⪯_{C} K implies J ⪯ K. Also note that in the presence of the first clause, the second clause of Def. 11 is equivalent with

– for any net N there is a net N′ ∈ C such that K(N′) ≅_{R} J (N).

8.4 Self-sequential Petri Nets

Definition 12. A Petri net is self-sequential if, using the standard firing rule of Def. 3, under no reachable marking a proper multiset of transitions is enabled, i.e. a transition is doubly enabled. Let SS be the class of self-sequential nets.

Theorem 5. H_{CT}^{ss} ⪯_{SS} H_{CT} and H_{IT}^{ss} ⪯_{SS} H_{IT}.

Proof. If N is self-sequential, trivially R(H_{CT}^{ss}(N)) = R(H_{CT}(N)), and therefore H_{CT}^{ss}(N) ≅_{R} H_{CT}(N). Likewise, R(H_{IT}^{ss}(N)) = R(H_{IT}(N)), considering that selfsequential nets can have no transitions t with^{•}t = 0. The second clause of Def. 11 is satisfied because the net N^{ss} constructed in the proof of Theorem 4 is selfsequential.

8.5 Unique-Occurrence Nets

Definition 13. A Petri net is a unique-occurrence net if ∀t ∈ T. ^{•}t > 0 (i.e. it is a standard net), ∀s ∈ S. I(s) + Σ_{t∈T} F (t, s) = 1 and the flow relation F is well-founded, i.e. there is no infinite alternating sequence x_{0}, x_{1}, … of places and transitions such that F (x_{i+1}, x_{i}) > 0 for i ∈ IN. Let UO be the class of unique-occurrence nets.

This class of nets is a close relative of the class of occurrence nets of Winskel [11]; it just lacks the requirements that cause the elimination of unreachable places and transitions (see Sect. 9).

Proposition 2. For every Petri net N, the net N_{•} is an unique-occurrence net. Moreover, if N is an unique-occurrence net, then N_{•} ≅ N.

Proof. The first statement follows immediately from the construction of N_{•}, the well-foundedness of F being a consequence of the recursive nature of Def. 4.

The second statement follows with induction on the well-founded order F, using the mappings β and η of Sect. 3. ⊓ ⊔

Prop. 2 tells that in a unique-occurrence net there is a bijective correspondence between places and token occurrences, and between transitions and transition firings. In particular, in a run of a net each place will be visited at most once, and each transition will fire at most once. Hence the name “unique-occurrence nets”. It follows that unique-occurrence nets are self-sequential.

Theorem 6. H_{IT} ⪯_{UO} H_{CT}.

Proof. Let N be a unique-occurrence net. Then H_{IT}(N) = H_{CT}(N_{•}) ≅ H_{CT}(N), using Theorem 3, Prop. 2 and the observation N_{•} ≅ N ⇒ H_{CT}(N_{•}) ≅ H_{CT}(N). Now let N be any Petri net. Then N_{•} ∈ UO by Prop. 2 and H_{CT}(N_{•}) ≅ H_{IT}(N) by Theorem 3.

Theorem 7. H_{IT}^{ss} ⪯_{UO} H_{IT} ⪯_{UO} H_{CT}^{ss} and H_{IT} ⪯_{UO} H_{IT}^{ss} ⪯_{UO} H_{CT}.

Proof. Let N be a unique-occurrence net. As unique-occurrence nets are selfsequential, Theorems 5 and 6 yield H_{IT}^{ss}(N) ≅_{R} H_{IT}(N) ≅_{R} H_{CT}(N) ≅_{R} H_{CT}^{ss}(N). Now let N be any Petri net. Then (N^{ss})_{•} is a unique-occurrence net by Prop. 2 and H_{any}^{any}((N^{ss})_{•}) ≅_{R} H_{CT}((N^{ss})_{•}) ≅_{R} H_{IT}(N^{ss}) ≅_{R} H_{IT}^{ss}(N) by Theorems 3 and 4.

This yields the expressiveness hierarchy of Fig. 1.

9 Unfolding into Occurrence Nets

Definition 14 ([11]). An occurrence net is a unique-occurrence net such that – the conflict relation #⊆ T × T is irreflexive, where

x#y ⇔ ∃t, t′ ∈T. t ≠ t′, ^{•}t ∩^{•}t′ ≠ ∅, tF^{∗}x, tF^{∗}y

– and ∀t ∈ T. {t′ | t′F^{∗}t} is finite.

Here F^{∗} denotes the reflexive and transitive closure of the flow relation, given by xF y iff F (x, y) > 0. It is easy to see that transitions in a unique-occurrence net that violate the conditions above can never fire, and in fact an occurrence net is a unique-occurrence net with the property that every place occurs in a reachable marking and every transition in a firing sequence. Therefore, any uniqueoccurrence net can be converted into an occurrence net by the operation R that omits all transitions t that violate the requirements above, together with all places and transitions x with tF^{∗}x. The net R(N) consists of the reachable places and transitions in N, and H(R(N)) ≅_{R} H(N) for H ∈ {H_{CT}, H_{IT}, H_{CT}^{ss}, H_{IT}^{ss}}. This allows me to define an unfolding operator U, turning any given Petri net N into an occurrence net U(N) with H_{IT}(U(N)) ≅_{R} H_{IT}(N), as follows.

Definition 15. Let N be a Petri net. The unfolding U(N) of N is R(N_{•}).

This construction extends the prior unfolding constructions of Winskel [11], Engelfriet [4] and Meseguer, Montanari & Sassone [8]. The latter, and most general, was given for standard nets only. Instead of restricting to reachable transitions at the end, these approaches do so on the fly. The same could be done here, by applying the two requirements of Def. 14 in the third clause of Def. 4.

References

1. E. Badouel (1996): Splitting of actions, higher-dimensional automata, and net synthesis. Technical Report RR-3490, Inria, France.

2. E. Best & R. Devillers (1987): Sequential and concurrent behavior in Petri net theory. Theoretical Computer Science 55(1), pp. 87–136.

3. E. Best, R. Devillers, A. Kiehn & L. Pomello (1991): Concurrent bisimulations in Petri nets. Acta Informatica 28, pp. 231–264.

4. J. Engelfriet (1991): Branching processes of petri nets. Acta Informatica 28(6), pp. 575–591.

5. R.J. van Glabbeek (2005): On the expressiveness of higher dimensional automata

(extended abstract). Available at http://boole.stanford.edu/pub/hda-ea.pdf.

Electronic Notes in Theoretical Computer Science 128(2): Proc. 11th International Workshop on Expressiveness in Concurrency, EXPRESS 2004, pp. 5–34.

6. R.J. van Glabbeek & G.D. Plotkin (1995): Configuration structures (extended abstract). In D. Kozen, editor: Proceedings 10^{th} Annual IEEE Symposium on Logic in Computer Science, LICS’95, San Diego, USA, IEEE Computer Society Press,

pp. 199–209. Available at http://boole.stanford.edu/pub/conf.ps.gz.

7. U. Goltz & W. Reisig (1983): The non-sequential behaviour of Petri nets. Information and Computation 57, pp. 125–147.

8. J. Meseguer, U. Montanari & V. Sassone (1997): On the semantics of place/ transition Petri nets. Mathematical Structures in Computer Science 7, pp. 359–397.

9. M. Mukund (1992): Petri nets and step transition systems. International Journal of Foundations of Computer Science 3(4), pp. 443–478.

10. V.R. Pratt (1991): Modeling concurrency with geometry. In Proc. 18th Ann. ACM Symposium on Principles of Programming Languages, pp. 311–322.

11. G. Winskel (1987): Event structures. In W. Brauer, W. Reisig & G. Rozenberg, editors: Petri Nets: Applications and Relationships to Other Models of Concurrency, Advances in Petri Nets 1986, Part II, Proceedings of an Advanced Course, Bad Honnef, September 1986, LNCS 255, Springer, pp. 325–392.