Florent Avellaneda

Rémi Morin

Vector Addition Systems with States vs. Petri Nets

Petri nets are a well-known and intensively studied model of concurrency often used to specify distributed or parallel systems. Vector addition systems with states are simply Petri nets provided control states. In this paper we introduce a natural partial order semantics for vector addition systems with states which extends the process semantics of Petri nets. The addition of control states to Petri nets leads to undecidable problems, namely the equality of two process languages given by two systems. However we show that basic problems about the set of markings reached along the processes of a VASS, such as boundedness, covering and reachability, can be reduced to the analogous problems for Petri nets. We show also how to check effectively any MSO property of these partial orders, provided that the system is bounded. This result generalizes known results and techniques for the model checking of compositional message sequence graphs.

Introduction

Consider a set of reactions that take place among a collection of particles such that each reaction consumes a multiset of available particles and produces a linear combination of other particle types. This kind of framework can be formalized by a vector addition system [START_REF] Karp | Parallel program schemata[END_REF] or, equivalently, a (pure) Petri net [START_REF] Peterson | Petri Net Theory and the Modeling of Systems[END_REF]. Consider in addition some control state which determines whether a reaction can occur or not, and such that the occurrence of a reaction leads to a possibly distinct control state. Then the model becomes formally a vector addition system with states (a VASS), a notion introduced in [START_REF] Hopcroft | On the reachability problem for 5-dimensional vector addition systems[END_REF]. It is well-known that all these models are computationally equivalent, because they can simulate each other [START_REF] Peterson | Petri Net Theory and the Modeling of Systems[END_REF][START_REF] Reisig | Petri Nets, An Introduction[END_REF][START_REF] Reutenauer | The Mathematics of Petri Nets[END_REF]. More precisely any vector addition system with states over n places can be simulated by some vector addition system over n + 3 places [START_REF] Hopcroft | On the reachability problem for 5-dimensional vector addition systems[END_REF]. These simulations do not preserve strictly the set of reachable markings because they require additional places to encode control states. Still they allow us to use techniques or tools designed for Petri nets to check the properties of the set of reachable markings of a VASS. The addition of control states to vector addition systems makes it easier to model and to analyse distributed or parallel systems. For instance it is convenient to use a vector of control states to check the structural properties of channels within a network of communicating finite state machines [START_REF] Leue | A scalable incomplete test for the boundedness of UML RT models[END_REF].

The popular model of message sequence graphs (MSGs) can be regarded as a particular case of VASSs where the only allowed reactions are the sending and the receipt of one message from one site to another [START_REF] Alur | Model checking of message sequence charts[END_REF][START_REF] Ben-Abdallah | Syntactic detection of process divergence and non-local choice in message sequence charts[END_REF][START_REF] Genest | A Kleene theorem and model checking algorithms for existentially bounded communicating automata[END_REF][START_REF] Gunter | Compositional message sequence charts[END_REF][START_REF] Madhusudan | Beyond message sequence graphs[END_REF]. Then each sequence of reactions can be described by a partial order of events called a message sequence chart (MSC). Each MSC corresponds to several sequences of elementary actions which are equivalent up to the reordering of independent events. Similarly each sequence of MSCs is equivalent to several sequences of MSCs. Thus control states are used to focus on particular interleavings of events in order to avoid the state explosion problem due to concurrency. However there exists so far no way to regard an execution of a VASS as a partial order of events. Consequently there is no means to apply techniques or tools for Petri nets to the analysis of MSGs. The first contribution of this paper is the definition of a partial order semantics for VASSs in such a way that the framework of MSGs can effectively be regarded as a particular case of VASS.

Suggested by Petri in the restricted setting of condition/event systems [START_REF] Petri | Non-Sequential Processes: Translation of a Lecture given at the IMMD Jubilee Colloquium on 'Parallelism in Computer Science[END_REF], the process semantics of a Petri net defines labeled occurrence nets as partially ordered sets of events with non-branching conditions [START_REF] Best | Sequential and concurrent behaviour in Petri net theory[END_REF][START_REF] Engelfriet | Branching processes of Petri nets[END_REF][START_REF] Goltz | The non-sequential behavior of Petri nets[END_REF][START_REF] Reisig | Petri Nets, An Introduction[END_REF][START_REF] Vogler | Modular Construction and Partial Order Semantics of Petri Nets[END_REF]. As opposed to the other classical partialorder semantics based on step firing sequences [START_REF] Grabowski | On partial languages[END_REF][START_REF] Kiehn | On the interrelation between synchronized and non-synchronized behaviour of Petri nets[END_REF][START_REF] Vogler | Modular Construction and Partial Order Semantics of Petri Nets[END_REF], a process records all causal dependencies between the events occurring along a run. We present in Section 1 a partial order semantics for VASSs which extends the usual process semantics of Petri nets. The approach is simple and natural. First we consider the set of firable computation sequences of a VASS and second we define the processes that represent a given sequence. Then each process describes some causal dependencies between events which are no longer linearly ordered. This means that two reactions that appear one after the other in a computation sequence can occur concurrently (that is, possibly in the reverse order) within a corresponding process. This situation is usual when modeling asynchronous systems. In particular this is similar to the way message sequence charts are derived from message sequence graphs (see, e.g. [2, ?,3]). Thus, control states represent abstract stages of computations used to specify particular sets of reaction sequences: They do not appear formally in the process semantics. In this way, message sequence graphs are embedded in the framework of VASSs. However, one specific feature of the process semantics is that a computation sequence can yield several non-isomorphic processes depending on the order identical particles are consumed. Along this paper, we shall exhibit few other facts which make clear that the model of VASS is more general and more difficult to handle than MSGs.

It is easy to prove that checking the inclusion (or the equality) of two process languages given by two VASSs is undecidable. The reason is that the equality and the inclusion problems for rational Mazurkiewicz trace languages [START_REF] Diekert | The Book of Traces[END_REF] are undecidable because the universality problem is undecidable [START_REF] Sakarovitch | The "last" decision problem for rational trace languages[END_REF]. Moreover rational Mazurkiewicz trace languages can be represented by MSGs [START_REF] Henriksen | A theory of regular MSC languages[END_REF] and MSGs are embedded into VASSs. This basic observation illustrates the computional gap between Petri nets and VASSs under the process semantics because these two problems are decidable for Petri nets, by means of a straightforward reduction to the covering problem [START_REF] Esparza | Decidability issues for Petri nets -a survey[END_REF].This shows also that the analysis of the partially ordered executions of a VASS does not boil down to the verification of a Petri net in general, in spite of the well-known simulation of a VASS by a Petri net. Synthesis problems have been investigated for various models of concurrency: Asynchronous automata [START_REF] Diekert | The Book of Traces[END_REF][START_REF] Droste | Asynchronous cellular automata for pomsets[END_REF][START_REF] Zielonka | Notes on finite asynchronous automata[END_REF], Petri nets [START_REF] Ph | Unbounded Petri Net Synthesis[END_REF][START_REF] Ehrenfeucht | Partial (set) 2-structures. Part II: State spaces of concurrent systems[END_REF][START_REF] Hoogers | A trace semantics for Petri nets[END_REF][START_REF] Mukund | Petri nets and step transition systems[END_REF], communicating finite-state machines [START_REF] Alur | Model checking of message sequence charts[END_REF][START_REF] Henriksen | A theory of regular MSC languages[END_REF], etc. They consist mainly in characterizing which formal behaviours correspond to some class of concurrent devices and to build if it exists such a device from its behavioural specification. We study in Section 2 a natural synthesis problem: Given some VASS we ask whether its processes are generated by some Petri net. We show that this problem is undecidable (even for bounded systems) by means of a reduction to the universality problem for rational Mazurkiewicz trace languages. However we present in the rest of this paper several techniques to check properties of a VASS under the process semantics with the help of known algorithms and tools.

A key verification problem for MSGs is to detect channel divergence, i.e. to decide whether the number of pending messages along an execution is unbounded [2, ?,3, 19]. This problem is NP-complete. An equivalent problem in the more general setting of VASSs is the prefix-boundedness problem. It consists in checking that the set of markings reached by prefixes of processes is finite. We present in Section 3 a technique to solve this problem by means of a new construction. We obtain that prefix-boundedness is computationally equivalent to the boundedness problem for Petri nets and requires exponential space [START_REF] Esparza | Decidability issues for Petri nets -a survey[END_REF]. This result exhibits an interesting complexity gap between MSGs and VASSs. It shows that algorithms to check properties of MSGs need to be revised in order to deal with the more expressive framework of VASSs. Other basic decision problems for the markings reached by prefixes are of course interesting. We show in particular that the reachability and the covering of a given marking by prefixes can be solved using the same technique.

The model-checking problem for MSGs against monadic second-order logic (MSO) was investigated first in [START_REF] Madhusudan | Reasoning about sequential and branching behaviours of message sequence graphs[END_REF]. As opposed to earlier works [START_REF] Alur | Model checking of message sequence charts[END_REF], formulas are interpreted on the partially ordered scenarios accepted by the MSGs. This problem was proved decidable for the whole class of safe MSGs [START_REF] Madhusudan | Beyond message sequence graphs[END_REF] (see also [START_REF] Genest | A Kleene theorem and model checking algorithms for existentially bounded communicating automata[END_REF]). Each safe MSG can be regarded as a bounded VASS. However a safe MSG can describe an infinite set of markings because the reordering of events can produce an unbounded number of pending messages within channels: In other words, a safe MSG may be divergent. We present in Section 4 a technique to check effectively that all processes of a given bounded VASS satisfy a given MSO formula. We shall explain in details why this result subsumes, but cannot be reduced to, previous works on the model-checking of MSGs.

Model and semantics

The goal of this section is to extend the usual process semantics from Petri nets to VASSs. In order to avoid repetitive definitions we introduce the model of Petri nets with states as a minimal framework which includes both Petri nets and VASSs. Thus Petri nets are regarded as Petri nets with states provided with a single state whereas VASSs are simply Petri nets with states using pure transition rules, only. Next we present the notions of firable computation sequence, reachable marking, and (non-branching) process as simple generalizations of the classical definitions in the restricted setting of Petri nets.

For simplicity's sake, for any mapping λ : A → B between two finite sets A and B, we shall denote also by λ the natural mapping λ : A ⋆ → B ⋆ from words over A to words over B and the mapping λ : N A → N B from multisets over A to multisets over B such that λ(µ) = a∈A µ(a) • λ(a) for each multiset µ ∈ N A . Moreover we will often identify a set S with the multiset µ S for which µ S (x) = 1 if x ∈ S and µ S (x) = 0 otherwise. We borrow from the setting of Petri nets the abstract notion of places which can represent different kinds of components within a system: a local control state of a sequential process, a communication channel, a shared register, a particle type, a molecule in a chemical system, etc. We let P denote a finite set of places throughout this paper. As usual a multiset of places is called a marking and it is regarded as a distribution of tokens in places. Further we fix a finite set N of rule names.

A transition rule (or a reaction) is a means to produce new tokens in some places by consuming tokens in some other places. Formally a rule is a triple r = (λ, α, β) where λ ∈ N is a rule name and α, β ∈ N P are markings called the guard and the update respectively. Such a rule is denoted by λ : α ¨β. It means intuitively that a set of tokens α can be consumed to produce a set of tokens β in an atomic way. Different rules can share the same guard α and the same update β. That is why we use here rule names to distinguish between similar but distinct rules. For each rule r = (λ, α, β), we put • r = α and r • = β. Definition 1.1. A Petri net with states (for short: a PNS) over a set of rules R is an automaton S = (Q, ı, -→, µ in ) where Q is a finite set of states, with a distinguished initial state ı ∈ Q, -→⊆ Q × R × Q is a finite set of arcs labeled by rules, and µ in ∈ N P is some initial marking.

Let S = (Q, ı, -→, µ in ) be a Petri net with states. A labeled arc (q 1 , r, q 2 ) ∈-→ will be denoted by q 1 r -→ q 2 . A rule sequence s = r 1 ...r n ∈ R ⋆ is called a computation sequence of S if there are states q 0 , ..., q n ∈ Q such that ı = q 0 and for each i ∈ [1, n], q i-1 r i -→ q i . These conditions will be summed-up by the notation ı s -→ q n . For instance, (p : x ¨x + z) • (c : y + z ¨y) • (p : x ¨x + z) • (c : y + z ¨y) is a computation sequence of the PNS with two states depicted in Fig. 1. We denote by CS(S) the set of all computation sequences of S. This language is obviously a regular and prefix-closed set of words over R. Conversely any regular and prefix-closed language over a finite subset of rules is the set of computation sequences of some PNS. Actually the partial order semantics we shall adopt considers PNSs simply as a formal means to specify regular sets of rules.

A rule sequence s = r 1 ...r n ∈ R ⋆ is firable from a marking µ if there are multisets of places µ 0 , ..., µ n such that µ 0 = µ and for each k ∈

[1, n]: µ k-1 • r k and µ k = µ k-1 -• r k +r • k .
This means intuitively that each rule from s can be applied from the marking µ in the linear order specified by s: Each rule r k consumes • r k tokens from µ k-1 and produces r • k new tokens which yields the subsequent multiset µ k . Then we say that µ n is reached by the rule sequence s from the marking µ. We also say that s leads to µ n . We denote by FCS(S) the set of all firable computation sequences of S. A marking is reachable in S if it is reached by a firable computation sequence of S. A PNS is said to be bounded if the set of its reachable markings is finite.

VASS, Petri net and causal net

Originally introduced in [START_REF] Hopcroft | On the reachability problem for 5-dimensional vector addition systems[END_REF], the notion of a vector addition system with states (for short: a VASS) can be formally defined in several slightly different ways. In this paper, a VASS is simply a PNS such that each rule r labeling an arc is pure, which means that for all places p ∈ P , • r(p) × r • (p) = 0. This amounts to require that • r(p) 1 implies r • (p) = 0 and vice versa. For this reason each rule r in a VASS can be represented by a vector v ∈ Z P where v(p) = r • (p) -• r(p) for all p ∈ P . We could also require that a VASS uses a single rule name, i.e. for all rules r 1 , r 2 ∈ R, r 1

• -• r 1 = r 2 • -• r 2 implies r 1 = r 2 .
In this way any two similar rules must carry the same rule name. This restriction would have no effect on the results presented in this paper.

We explain at present why we can identify the well-known formalism of Petri nets as particular PNSs provided with a single state. Definition 1.2. A Petri net is a quadruple N = (P, T, W, µ in ) where -P is a finite set of places and T is a finite set of transitions such that P ∩ T = ∅; -W is a map from (P × T ) ∪ (T × P ) to N, called the weight function; -µ in is a map from P to N, called the initial marking.

We shall depict Petri nets in the usual way as in Fig. 4: Black rectangles represent transitions whereas circles represent places; moreover tokens in places describe the initial marking. Given a Petri net N = (P, T, W, µ in ) and a transition t ∈ T , • t = p∈P W (p, t) • p is the pre-multiset of t and t • = p∈P W (t, p) • p is the post-multiset of t. Similarly we put • p = t∈T W (t, p) • t and p • = t∈T W (p, t) • t for each place p ∈ P .

Let N = (P, T, W, µ in ) be a Petri net. We will regard N as a PNS S N with the same set of places P and the same initial marking. Moreover S N is provided with a single state ı such that each transition t ∈ T is represented by a self-loop labeled arc ı r -→ ı where r = (t, • t, t • ). In this way, the class of Petri nets is faithfully embedded into the subclass of PNSs provided with a single state such that each transition carries a rule with a distinct rule name. Conversely, take any PNS S with a single state ı such that each transition carries a rule with a distinct rule name. The corresponding Petri net shares with S its set of places and its initial marking. Moreover for each self-loop ı r -→ ı it admits a transition t r such that • t r = • r and t r • = r • . For instance the PNS from Fig. 3 corresponds to the Petri net from Fig. 4.

If the weight function W takes only binary values then it is often described as a flow relation F ⊆ (P × T ) ∪ (T × P ) where (x, y) ∈ F if W (x, y) = 1. Further F + denotes the transitive closure of F .

• | 1 for all b ∈ B. 3. µ min (b) = 1 if • b = ∅ and µ min (b) = 0 otherwise.
Note that the third requirement guarantees that the initial marking µ min can be recovered from the structure (B, E, F ) because it coincides with the set of minimal conditions. For that reason causal nets are often defined as a triple (B, E, F ) satisfying the two first conditions of Def. 1.3. In the literature causal nets are also called occurrence nets, see e.g. [START_REF] Best | Sequential and concurrent behaviour in Petri net theory[END_REF][START_REF] Genrich | A dictionary of some basic notions of net theory[END_REF][START_REF] Goltz | The non-sequential behavior of Petri nets[END_REF][START_REF] Van Glabbeek | On causal semantics of Petri nets[END_REF][START_REF] Reisig | Petri Nets, An Introduction[END_REF]. However more general Petri nets are called occurrence nets in the theory of partial unfolding or branching processes [START_REF] Engelfriet | Branching processes of Petri nets[END_REF][START_REF] Esparza | An improvement of McMillan's unfolding algorithm[END_REF][START_REF] Nielsen | Petri nets, event structures and domains, part I[END_REF].

The transitive and reflexive closure F * of the flow relation F in a causal net K = (B, E, F, µ min ) yields a partial order over the set of events E. A configuration is a subset of events H ⊆ E that is downwards closed, i.e. e ′ F * e and e ∈ H imply e ′ ∈ H. Each configuration H defines a prefix causal net K H whose events are precisely the events from H and whose places consists of the minimal places of K (with respect to the partial order relation F * ) and all places related to some event from H. For instance Fig. 2 exhibits a subset of a causal net (circled with a dotted line) that is a prefix of that causal net. For each class of labeled causal nets L, we denote by Pref(L) the class of all prefixes of all labeled causal nets from L.

Simulation of a VASS by a Petri net

Let us now recall how a k-dimensional VASS or more generally a PNS S with k places can be simulated by a Petri net N with k+n places, where n is the number of states [START_REF] Reutenauer | The Mathematics of Petri Nets[END_REF][START_REF] Peterson | Petri Net Theory and the Modeling of Systems[END_REF]. The usual construction is illustrated by Fig. 5 which shows on the left-hand side a PNS with 2 states (ı and q) and 3 places (x, y and z) and on the right-hand side the corresponding Petri net with 5 places: Each place from S and each state from S corresponds to a place from N. The initial marking of N describes the initial marking of S and some token is added in the place corresponding to the initial state of S. Moreover each arc q 1 r -→ q 2 in S is represented by a transition in N. It is easy to see that there is a one-to-one correspondence between the firable computation sequences of S and the firable rule sequences of N; moreover the marking reached by N describes the marking reached by S and the current state of S.

This construction of N from S is interesting because it enables us to analyse the set of reachable markings of S by means of usual techniques from the Petri net literature (see [START_REF] Esparza | Decidability issues for Petri nets -a survey[END_REF] for a survey). In particular the boundedness problem asks whether the set of reachable markings is finite whereas the covering problem asks whether a given marking µ is covered by some reachable marking µ ′ , i.e. µ µ ′ . These two problems are decidable (for Petri nets and Petri nets with states) but they can require exponential space [START_REF] Rackoff | The covering and boundedness problems for vector addition systems[END_REF].

The simulation of a PNS by a Petri net leads us to the next result.

Proposition 1.4. Let S be a PNS and r be a rule attached to some arc of S. We can decide whether r occurs in a firable computation sequence of S.

Proof. We have recalled that there is a one-to-one correspondence between the firable computation sequences of S and the firable computation sequences of N. The rule r occurs in a firable computation sequence of S if and only if a corresponding transition t in N occurs in a firable transition sequence in N. This is equivalent to check whether the marking of • t is covered by a reachable marking of N. As mentionned above this question is known to be decidable.

Process semantics of a PNS

In this paper we are interested in a semantics of PNS based on causal nets which is a direct generalization of the process semantics of Petri nets [START_REF] Best | Sequential and concurrent behaviour in Petri net theory[END_REF][START_REF] Engelfriet | Branching processes of Petri nets[END_REF][START_REF] Van Glabbeek | On causal semantics of Petri nets[END_REF][START_REF] Goltz | The non-sequential behavior of Petri nets[END_REF][START_REF] Reisig | Petri Nets, An Introduction[END_REF][START_REF] Vogler | Modular Construction and Partial Order Semantics of Petri Nets[END_REF]. The process semantics of Petri nets characterizes the labeled causal nets that describe an execution of a given Petri net. We have already observed that each transition of a Petri net can be regarded as a rule. For that reason we adopt a graphical representation of rules similar to a transition of a Petri net, as depicted in Fig. 6. Given an initial multiset of places, each firable computation sequence can be represented by a causal net, called a process, which somehow glues together the representations of each rule. For instance the labeled causal net K from Fig. 2 depicts a process of the Petri net N from Fig. 4 in which each condition of K is labeled by a place of N and each event of K is labeled by a transition of N.

The following definition explains how processes are derived from a given rule sequence. Next the processes of a PNS will be defined as the processes of its firable computation sequences (Def. 1.6). Definition 1.5. A process of a rule sequence s = r 1 ...r n ∈ R ⋆ from a marking µ ∈ N P consists of a causal net K = (B, E, F, µ min ) with n events e 1 , ..., e n provided with a labeling π : B ∪ E → P ∪ N such that the following conditions are satisfied:

1. π(b) ∈ P for all b ∈ B, π(e) ∈ N for all e ∈ E, and π(µ min ) = µ; )) for all i ∈ [1, n]; 3. e i F + e j implies i < j for any two i, j ∈ [1, n].

We denote by [[s]] µ the class of all processes of s from µ.

In this definition the mapping π denotes the labeling of K and its natural extension to multisets. The first condition asserts that the initial marking of the causal net describes the marking µ; moreover each condition is associated with some place and each event corresponds to some rule name. The second condition requires that the label, the preset and the post-set of each event coincide with the name, the guard and the update of the corresponding rule. Finally the last property ensures that the total order of rules in s corresponds to an order extension of the partial order of events in K. Consequently any subset of events {e 1 , ..., e k } is downwards closed. Moreover the prefix causal net K ′ corresponding to the configuration {e 1 , ..., e n-1 } is a process of the rule sequence r 1 ...r n-1 from the same marking µ. Consequently the class of processes of a rule sequence could be also defined inductively over its length, as we will see in Prop. 3.3. Furthermore it is easy to see that the class of processes of a rule sequence is empty if and only if the rule sequence is not firable from µ min .

Let H be a configuration of a process K = (B, E, F, µ min , π) of a rule sequence s from µ. Let B max be the set of maximal conditions of the prefix K H w.r.t. F * . Then the multiset of places π(B max ) is called the marking reached by K H and we say that K H leads to the marking π(B max ). Let s H be a linear extension of the events from H. Then it is clear that the rule sequence π(s H ) is firable from µ and leads to the marking π(B max ); moreover K H is a process of π(s H ) from µ.

Roughly speaking, any labeled causal net isomorphic to a process of s is also a process of s. In particular the class of processes of the empty rule sequence from some marking µ collects all labeled causal nets with no event and such that its set of labeled places represents the multiset µ. Further a rule sequence may give rise to multiple (non-isomorphic) causal nets depending on the consumption of tokens by each event and the initial marking. For instance the computation sequence (p : x ¨x+z)•(c : y+z ¨y)•(p : x ¨x+z)•(c : y+z ¨y) of the PNS from Fig. 1 corresponds to the causal net from Fig. 2. However if there are x + y + z tokens initially, then this computation sequence corresponds to the two labeled causal nets from Fig. 7 among some others. Definition 1.6. Let S be a PNS with initial marking µ in . A process of S is a process of a computation sequence of S from µ in . We let [[S]] denote the class of all processes of S.

Thus [[S]] = s∈CS(S) [[s]] µ in .
It is easy to check that the processes of a PNS provided with a single state are precisely the processes of the corresponding Petri net w.r.t. the usual process semantics [START_REF] Best | Sequential and concurrent behaviour in Petri net theory[END_REF][START_REF] Van Glabbeek | On causal semantics of Petri nets[END_REF][START_REF] Vogler | Modular Construction and Partial Order Semantics of Petri Nets[END_REF]. Moreover any prefix of a process of S is a process of some rule sequence. Consequently the class of processes of a Petri net is closed by prefixes. However the set of processes of a PNS need not to be prefix-closed in general, as the next example shows.

Example 1.7. Consider the PNS from Fig. 1 with initial marking x + y and its process depicted in Fig. 2. Clearly the prefix of this process circled with the dotted line in Fig. 2 is not a process of that PNS.

A PNS is said to be prefix-bounded if the set of markings reached by prefixes is finite. Clearly any prefix-bounded PNS is bounded. The converse property does not hold in general. Continuing Example 1.7, each process of the PNS from Fig. 1 leads to a marking with at most 3 tokens whereas prefixes of these processes lead to infinitely many distinct markings (see in Fig. 2 a prefix of a process which leads to a marking with 4 tokens). However we stress that each bounded Petri net is prefix-bounded because its class of processes is prefix-closed.

Note that the simulation of a PNS by a Petri net considered in Subsection 1.3 is not faithful from the partial order point-of-view we adopt here. Consider again Figure 5. The processes of the PNS S (with three places) on the left-hand side differ from the processes of the Petri net N (with five places) on the right-hand side. In Section 3 we introduce a simulation of a PNS by another PNS that allows us to analyse the set of markings reached along the prefixes of the processes of a given PNS.

From compositional MSGs to PNSs

The formalism of compositional message sequence graphs (cMSGs) was introduced in [START_REF] Gunter | Compositional message sequence charts[END_REF] in order to strengthen the expressive power of MSGs and to provide an algebraic framework for the whole class of regular sets of MSCs [START_REF] Henriksen | A theory of regular MSC languages[END_REF]. As opposed to usual MSGs, cMSGs are built on components MSCs in which unmatched send or receive events are allowed. It was argued in [START_REF] Gunter | Compositional message sequence charts[END_REF] that simple protocols such as the alternating bit protocol can be described by cMSGs but not by MSGs. With no surprise cMSGs can be regarded as a particular case of VASS under the process semantics. Consider a distributed system consisting of a set I of sites and a set K of communication channels between pairs of sites. The behaviour of such a system can be specified by a PNS over the set P = I ∪ K of places such that the sending of a message from site i to site j within the channel k i,j from i to j is encoded by a rule i ¨i + k i,j and the receipt of such a message is encoded by a rule j + k i,j ¨j. Then we require that the initial marking (and each reachable marking) contains a single token in each place i ∈ I so that all events on a given site are linearly ordered. Such a PNS can actually be regarded as a compositional message sequence graph. The partial order semantics of cMSGs consists of message sequence charts which are simply a partial order of events obtained from a process by removing all conditions. Example 1.8. The PNS from Figure 8 describes a simplified sliding window protocol used to transmit data from a server i to a client j. The maximal number of missing acknowledgments is specified by the n initial tokens in the place w (the window). The system behaviour consists of three basic steps.

ı i + j + n • w q1 q2 q3 i + w ¨i j + m ¨j i ¨i + m j ¨j + a i + a ¨i i ¨i + w Time i j w i + w ¨i i i ¨i + d i d j + d ¨j j i + a ¨i i a j ¨j + a j i ¨i + w w i
1. The server sends a new data formalized by a token d if some token w is available: It consumes first a w token: i + w ¨i and next sends a new data: i ¨i + d. 2. The client receives a data and returns an acknowledgment formalized by a token a: It consumes first a data: j + d ¨j and next produces the ack: j ¨j + a. 3. The server receives an acknowledgment and increments the window size: First the ack is consumed: i + a ¨i and then a new token w is released: i ¨i + w.

A typical process of this system with n = 1 is depicted in Figure 9. It is clear that this system is bounded and even prefix-bounded.

Since local variables are prohibited in MSGs, the size of any safe cMSG equivalent to the PNS from the above example is exponential in the size of n. Thus a bounded PNS can be exponentially more concise than an equivalent safe cMSG. If this protocol starts with an initial window size of n = 2 k • w, then any safe cMSG describing the same class of processes needs 2 k distinct states.

Checking inclusion properties

A classical issue in concurrency theory consists in characterizing the expressive power of a model. Then a usual problem is the synthesis of a system from its behavioural specification. In this section we consider Petri nets with states as a means to specify concurrent behaviours in the form of processes. We tackle the problem of building a Petri net equivalent to some given Petri net with states. Two classes of specifications are studied according to the notion of equivalence we adopt.

Definition 2.1. A Petri net with states S is realizable (resp. prefix-realizable) if there is some Petri net N such that [[S]] = [[N]] (resp. Pref([[S]]) = [[N]]).
Note that the Petri net with states S from Figure 1 is not realizable because the set of processes it accepts is not prefix-closed (Example 1.7) whereas the set of processes recognized by any Petri net is prefix-closed. However S is prefix-realizable because the prefixes of its processes are precisely the processes of the Petri net with states provided with a single state depicted in Fig. 3 (i.e. the Petri net from Fig. 4). The next example exhibits a Petri net with states that is not prefix-realizable.

Example 2.2. Consider the PNS S from Figure 10.

Any Petri net N such that [[N]] = Pref([[S]]
) would accept the causal net K from Figure 11 as a process. However K is obviously not the prefix of some process from S. Therefore S is not prefix-realizable.

Although realizability appears to be the simplest problem to consider, we claim that prefixrealizability is also a natural issue because the processes of a

]]) ⊆ [[S 2 ]
]. Thus the difference between the specification S 1 and the canonical implementation S 2 stems from processes built on rules of S 1 that are not represented by some computation sequence of S 1 . This situation is similar to the notion of an implied scenario in the setting of realizable high-level message sequence charts [START_REF] Alur | Inference of message sequence charts[END_REF].

An undecidable problem with Mazurkiewicz traces

The undecidability results presented in this section rely on the universality problem in the setting of Mazurkiewicz trace theory [START_REF] Diekert | The Book of Traces[END_REF] that we recall now. Let Σ be some finite alphabet of actions. The concurrency of a distributed system is often represented by an independence relation over Σ, that is a binary, symmetric, and irreflexive relation ⊆ Σ × Σ. Then the pair (Σ, ) is called an independence alphabet. The associated trace equivalence is the least congruence ∼ over Σ ⋆ such that a b implies ab ∼ ba for all a, b ∈ Σ. We let [u] denote the trace equivalence class of a word u ∈ Σ ⋆ and we put [L] = u∈L [u] for any language L ⊆ Σ ⋆ .

Theorem 2.4. [START_REF] Sakarovitch | Elements of Automata Theory[END_REF]Theorem IV.4.3] It is undecidable whether [L] = Σ ⋆ for a given independence alphabet (Σ, ) and a given regular language L ⊆ Σ ⋆ .

Since we have not provided the model of VASS with the notion of accepting states, we need the slightly stronger but immediate next statement.

Corollary 2.5. It is undecidable whether [L] = Σ ⋆ for some given independence alphabet (Σ, ) and some given regular and prefix-closed language L ⊆ Σ ⋆ .

Proof. We proceed by contradiction. We assume that this problem is decidable and show that the problem from Theorem 2.4 becomes decidable. Let (Σ, ) be some independence alphabet and L ⊆ Σ ⋆ be some regular language. We consider some additional letter ⊥ and the new alphabet Γ = Σ ∪ {⊥} provided with the same independence relation: The new letter ⊥ is dependent with all letters from Σ.

Let L ′ = Pref(L) ∪ (L • {⊥} • Γ ⋆ ). It is clear that L ′ is regular and prefix-closed. Moreover L ⊆ L ′ . To conclude the proof we can check easily that [L ′ ] = Γ ⋆ if and only if [L] = Σ ⋆ . Assume first that [L] = Σ ⋆ . It is clear that [L ′ ] ⊆ Γ ⋆ . Let v ∈ Γ ⋆ . We distinguish two cases: If v ∈ Σ ⋆ then v ∼ u for some u ∈ L. If v / ∈ Σ ⋆ then v = v 0 .⊥.v 1 with v 0 ∈ Σ ⋆ and v 1 ∈ Γ ⋆ . Furthermore v 0 ∼ u 0 for some u 0 ∈ L. It follows that v ∼ u 0 .⊥.v 1 and u 0 .⊥.v 1 ∈ L ′ . In both cases we get v ∈ [u] for some u ∈ L ′ . Hence [L ′ ] = Γ ⋆ .
Conversely assume now that Γ ⋆ = [L ′ ] and consider v ∈ Σ ⋆ . Then v.⊥ ∈ Γ ⋆ . There exists some u ∈ L ′ such that v.⊥ ∼ u. Then u = u 0 .⊥ because ⊥ is dependent with all letters. Moreover v ∼ u 0 (because the trace equivalence is right-cancellative) and u 0 ∈ L ′ ∩ Σ ⋆ (because the trace equivalence is a Parikh equivalence). It follows that u 0 ∈ L.

Hence [L] = Σ ⋆ . Corollary 2.6. Let (Σ, ) be an independence alphabet. It is undecidable whether [L 1 ] ⊆ [L 2 ]
for any two regular and prefix-closed language L ⊆ Σ ⋆ .

Proof. Consider L 1 = Σ ⋆ and apply Cor. 2.5.

In the sequel of this section, we present a natural encoding of Mazurkiewicz traces in the form of causal nets. Then each prefix-closed rational Mazurkiewicz trace languages can be represented by a prefix-bounded PNS. As a consequence the inclusion relation

[[S 1 ]] ⊆ [[S 2 ]]
is undecidable for two given prefix-bounded PNSs S 1 and S 2 .

From Mazurkiewicz traces to processes

Let (Σ, ) be a fixed independence alphabet. We consider a finite set of places P and some mapping Loc : Σ → 2 P such that a b iff Loc(a) ∩ Loc(b) = ∅. There are several ways to find such a set P together with the location mapping Loc, one of which is to consider any subset {a, b} ⊆ Σ to be a place whenever a b and to put Loc(a) = {p ∈ P | a ∈ p}. We assume that each place p ∈ P occurs in some location Loc(a) of some action a ∈ Σ. Note that for any word u ∈ Σ ⋆ the rule sequence ρ(u) is firable from µ in and leads to the marking µ in . It follows from Prop. 3.3 that all processes from [[ρ(u)]] µ in are isomorphic to each other, i.e. there is intuitively only one process for ρ(u) from µ in .

We put N = Σ, R Σ = {(a, α, α) ∈ R | α = Loc
The next result asserts that trace equivalent words give rise to the same processes. And conversely, if two words correspond to the same processes, then these two words are trace equivalent. In this way equivalence classes of words are identified with processes. This property is actually similar to the well-known fact that trace equivalence classes of words can be represented by particular labeled partial orders.

Lemma 2.9. For all u, v ∈ Σ ⋆ : u ∼ v if and only if [[ρ(u)]] µ in = [[ρ(v)]] µ in . Proof. Let u ∈ Σ ⋆ and a, b ∈ Σ such that a = b. If u.ab ∼ u.ba then a b, Loc(a)∩Loc(b) = ∅, and [[ρ(u.ab)]] µ in = [[ρ(u.ba)]] µ in by Prop. 3.3. Therefore u ∼ v implies [[ρ(u)]] µ in = [[ρ(v)]] µ in for all u, v ∈ Σ ⋆ (
again with the help of Prop. 3.3). To prove the converse property, we proceed by induction over the length of u. The base case is trivial. We consider u

, v ∈ Σ ⋆ of length n + 1 such that [[ρ(u)]] µ in = [[ρ(v)]] µ in .
We distinguish two cases:

1. u = u ′ .a and v = v ′ .a for some u ′ , v ′ ∈ Σ ⋆ and a ∈ Σ. We have ρ(u) = ρ(u ′ ).ρ(a) and

ρ(v) = ρ(v ′ ).ρ(a). By Prop. 3.3 we have [[ρ(u ′ )]] µ in = [[ρ(v ′ )]] µ in . It follows from induction hypothesis that u ′ ∼ v ′ hence u ′ .a ∼ v ′ .a. 2. u = u ′ .a and v = v ′ .b for some u ′ , v ′ ∈ Σ ⋆ and a, b ∈ Σ with a = b. We have ρ(u) = ρ(u ′ ).ρ(a) and ρ(v) = ρ(v ′ ).ρ(b) with ρ(a) = ρ(b). Then any labeled causal net K from [[ρ(u)]] µ in = [[ρ(v)]
] µ in includes two maximal events e a and e b labeled by a and b respectively. It follows that a b. Let K ′ be the prefix of K obtained by erasing the two maximal event e a and e b . We consider a linear extension w ′ of the Σ-labeled events from K ′ . Then K ′ is the process from [[ρ(w

′ )]] µ in . Moreover [[ρ(w ′ .a)]] µ in = [[ρ(v ′ )]] µ in and [[ρ(w ′ .b)]] µ in = [[ρ(u ′ )]] µ in .
By induction hypothesis, we get w ′ .a ∼ v ′ and w ′ .b ∼ u ′ . On the other hand w ′ .ab ∼ w ′ .ba because a b. Hence u ∼ w ′ .ba ∼ w ′ .ab ∼ v.

We consider at present a regular and prefix-closed language L ⊆ Σ ⋆ and a finite automaton A(L) = (Q, ı, -→ A(L) ) whose states are all accepting and which recognized L. We may assume that each state of A(L) is reachable from the initial state and each action of Σ appears on a labeled arc of A(L). We build from the automaton A(L) the PNS S(L) = (Q, ı, -→ S(L) , µ in ) with the same set of states Q, the same initial state ı ∈ Q and such that for each rule r = (a, α, α) ∈ R Σ and all states q 1 , q 2 ∈ Q, there is some labeled arc q 1 r -→ S(L) q 2 if q 1 a -→ A(L) q 2 . Observe here the multiset of tokens is left unchanged by each rule. Consequently the set of markings reached by prefixes of [[S(L)]] is finite, i.e. the PNS S L is prefix-bounded. For any two regular and prefix-closed languages L 1 , L 2 ⊆ Σ ⋆ Lemma 2.9 shows that we have

[L 1 ] ⊆ [L 2 ] if and only if [[S L 1 ]] ⊆ [[S L 2 ]]. Thus the property [[S 1 ]] ⊆ [[S 2 ]
] is undecidable for two given prefix-bounded PNS S 1 and S 2 . We can strengthen this observation by the next statement. Proof. Let L ⊆ Σ ⋆ be a regular and prefix-closed language and S(L) be the corresponding PNS. Let N(L) be the Petri net collecting all rules R ⋆ Σ of S(L).

Then [[N(L)]] = [[R ⋆ Σ ]]. Moreover we can check that [[S(L)]] = [[R ⋆ Σ ]] if and only if [L] = Σ ⋆ . Assume first that [[S]] = [[R ⋆ Σ ]]. Let u ∈ Σ ⋆ . We have [[ρ(u)]] µ in = [[w]] µ in for some w ∈ CS(S). Let v = ρ -1 (w). Clearly v ∈ L. Since [[ρ(u)]] µ in = [[ρ(v)]] µ in we get u ∼ v by Lemma 2.9. Hence Σ ⋆ = [L]. Assume now that [L] = Σ ⋆ . Let w ∈ R ⋆ Σ . We have ρ -1 (w) ∈ Σ ⋆ . Then ρ -1 (w) ∼ u for some u ∈ L. It follows from Lemma 2.9 that [[w]] µ in = [[ρ(u)]] µ in . Moreover ρ(u) ∈ CS(S). Therefore [[R ⋆ Σ ]] µ in = [[CS(S)]] µ in .
By means of a slightly more involved encoding of Mazurkiewicz traces, we show in the next section that Theorem 2.10 holds also if S is a prefix-bounded VASS.

Gap between VASS and Petri nets

At present we focus on the subclass of vector addition systems with states, i.e. Petri nets with states with pure rules only. So far no rule from R Σ is pure, so the processes obtained

x y a x y ;

x, 0 y, 0 a

x, 1 y, 1

x, 1

x, 0 Fig. 13. Building the pure rule corresponding to a synchronisation rule Fig. 14. A release rule from R Σ cannot be described by a VASS. For this reason we have to use a slightly more involved encoding of Mazurkiewicz tracesbut we keep the same set of rule names ΣLet us consider the set of places P • = P × {0, 1} and the initial marking µ • in = P × {0}. This means that we use two copies of each place from P . Moreover we will make sure that any reachable marking will contain exactly one of these two copies. Intuitively places tagged by 0 are available and may be consumed by the system whereas places tagged by 1 are locked and need to be released. We let π : P • → P denote the first projection: π(m, n) = m for each m ∈ P . This mapping extends naturally to a mapping from multisets over P • to multisets over P :

π(µ) = (m,n)∈P • µ(m, n) • π(m, n).
We let R 1 collect all rules (a, α, β) over P • such that (a, π(α), π(β)) ∈ R Σ , α(m, n) 1 implies n = 0 and β(m, n) 1 implies n = 1. Thus we require that α and β correspond to the same set of untagged tokens, i.e. π(α) = π(β). Moreover we require that the tokens consumed are available whereas the tokens produced are locked. We denote by π : R 1 → R Σ the function which maps each rule (a, α, β) ∈ R 1 to (a, π(α), π(β)) ∈ R Σ . It is clear that this mapping is a bijection. For instance Figure 13 depicts a synchronization rule from R Σ together with the corresponding rule from R 1 .

We consider also a set of additional release rules that consume a locked place and produce the corresponding available oneas depicted in Figure 14Formally we let R 2 denote the set of rules (a, α, β) such that |α| = |β| = 1, α(m, 0) = 0 for all m ∈ P , and α(m, 1) = 1 implies β(m, 0) = 1. We put

R 0 = R 1 ∪ R 2 .
We build from S the Petri net with states

S • = (Q, ı, -→ S • , µ • in )
with the same set of states Q, the same initial state ı ∈ Q, and µ • in = P × {0} as initial marking. The labeled arcs of S • are defined as follows: For each rule r ∈ R 0 and for all states q 1 , q 2 ∈ Q, we put q 1 r -→ S • q 2 if one of these two conditions is satisfied:

r ∈ R 1 and q 1 a -→ S q 2 with a = π(r); -r ∈ R 2 and q 1 = q 2 . Note here that S • is a VASS because each rule from R 0 is pure. Since each place p ∈ P occurs in the location Loc(a) of some action a ∈ Σ and each action a appears on a labeled arc of A starting from a state reachable from its initial state ı, it is clear that each rule from R 0 appears in some firable computation sequence of S • .

The bijection π : R 1 → R Σ can be regarded as a function π : R 0 → R Σ ∪ {ε} where π(r) map to the empty word ε for each r ∈ R 2 . This function extends naturally to a mapping π : R ⋆ 0 → R ⋆ Σ which associates each rule sequence r 1 ...r n from R ⋆ 0 to the rule sequence π(r 1 )...π(r n ) from R ⋆ Σ . Due to the similar structure between S • and S, it is clear that each computation sequence u of S • maps to some computation sequence π(u) of S. Furthermore, firable computation sequences correspond to firable computation sequences. Thus we have π : FCS(S • ) → FCS(S). The next observation asserts that the mapping π : FCS(S • ) → FCS(S) is actually onto.

Proposition 2.11. For all u ∈ FCS(S) there exists u

• ∈ FCS(S • ) such that π(u • ) = u.
Proof. By an immediate induction over the length of u, we can check that for each u ∈ FCS(S) there exists some u • ∈ FCS(S • ) such that π(u • ) = u and the marking reached by u • is µ • in . Recall that each rule of S is a synchronisation rule and the initial marking of S consists of a single token in each place. As a consequence, for each rule sequence u ∈ R ⋆ Σ , the class of processes

[[u]] µ • in consists of isomorphic labeled causal nets. For any two rule sequences u, v ∈ R ⋆ Σ , we put u ≃ v if [[u]] µ • in = [[v]]
, v ∈ R ⋆ 0 , we put u ≃ • v if u = v or [[u]] µ • in = [[v]] µ • in = ∅.
The second observation ensures that this process equivalence is preserved by the mapping π : FCS(S • ) → FCS(S). Proposition 2.12. For all

u 1 , u 2 ∈ FCS(S • ), u 1 ≃ • u 2 implies π(u 1 ) ≃ π(u 2 ). Proof. Let u 1 , u 2 ∈ FCS(S • ) be such that u 1 ≃ • u 2 and u 1 = u 2 . Let K be the labeled causal net from [[u 1 ]] µ • in .
Then u 1 and u 2 are two linear extensions of the partial order of rules occurring in K. We may assume that u 1 = v.ab.w and u 2 = v.ba.w with v, w ∈ R ⋆ 0 and a, b ∈ R 0 . We distinguish then two cases. We will also need the next technical result.

Proposition 2.13. For all firable computation sequences v ∈ FCS(S) and all firable rule sequences u ∈ R ⋆ 0 , if π(u) ≃ v then u ≃ • w for some firable computation sequence w ∈ FCS(S • ).

Proof. We distinguish two cases. 1. The marking reached by u consists of available places only. We consider the rule sequence w ∈ R 0 built inductively over the length of v by replacing each rule r from v by the corresponding rule π -1 (r) ∈ R 1 followed by a series of release rules from R 2 such that all locked places produced by π -1 (r) are released. Then w ∈ FCS(S • ) and π(w) = v. Hence π(u) ≃ π(w). It follows that u ≃ • w. 2. Some places in the marking reached by u are locked. We add a sequence of release rules z to u to get w = u.z such that the marking reached by w consists of available places only. Then π(w) ≃ v. We apply the first case to get some firable computation sequence w ′ ∈ FCS(S • ) such that w ≃ • w ′ . We can remove from w ′ the release rules of z and get some firable computation sequence w ′′ ∈ FCS(S • ) such that u ≃ • w ′′ .

Observe here the number of tokens is constant whenever a rule is applied. Consequently the set of markings reached by prefixes of [[S • ]] is finite, i.e. S • is prefix-bounded. We can prove that S • is realizable if and only if S is realizable. Thus, Theorem 2.14. It is undecidable whether a given prefix-bounded VASS is realizable.

Proof. Let N be the Petri net consisting of all rules of R Σ with the initial marking µ in = P . By Prop.

2.3, S is realizable if and only if [[S]] = [[N]

]. Moreover N is equivalent to a PNS with only synchronisation rules (and with only one state). We let N • be the VASS corresponding to N w.r.t. the above construction of S from S • . We may apply the three above propositions with N and N • respectively. Since N • has a single state, it is equivalent to a pure Petri net. Further N • consists of all rules of R 0 and its initial marking is µ • in . Since each rule from R 0 appears in some firable computation sequence of S • , Prop. [START_REF] Alur | Model checking of message sequence charts[END_REF]

.3 claims that S • is realizable if and only if [[S

• ]] = [[N • ]]. We can check that S • is realizable if and only if S is realizable. Assume first that S • is realizable: We have [[S • ]] = [[N • ]]. Let K ∈ [[N]].
Let u be a linear extension of the partial order of rules occurring in K. Then u ∈ FCS(N). There exists some firable computation sequence u

• ∈ FCS(N • ) such that π(u • ) = u (Prop. 2.11 applied with N and N • ). Then u • ≃ • v • for some v • ∈ FCS(S • ) because [[S • ]] = [[N • ]]. Furthermore u = π(u • ) ≃ π(v • ) ∈ FCS(S) by Prop. 2.12. Hence K ∈ [[S]]. It follows that [[S]] = [[N]], i.e. S is realizable. Assume now that S is realizable: We have [[S]] = [[N]]. By construction, [[S • ]] ⊆ [[N • ]]. We can check [[N • ]] ⊆ [[S • ]], hence [[N • ]] = [[S • ]] and S • is realizable. Let K • be a process of N • and u • be a linear extension of the rules occurring in K • . Then u • ∈ FCS(N • ). Let u = π(u • ). Then u ∈ FCS(N). Since [[S]] = [[N]
] we have u ≃ v for some v ∈ FCS(S). By Prop. 2.13, there exists some v

• ∈ FCS(S • ) such that u • ≃ • v • . Then K • ∈ [[v • ]] µ • in hence K • ∈ [[S • ]].
Finally we can consider now the problem of prefix-realizability. We call terminating rule each rule ⊥ : M ¨∅ for which M ⊆ P • is a subset of places such that π(M) = P . We denote by R 3 the set of all terminating rules and we put R ⊥ = R 0 ∪ R 3 . We build from S • the Petri net with states S

• ⊥ = (Q, ı, -→ S • ⊥ , µ • in )
with the same set of states Q, the same initial state ı ∈ Q, the same set of places P • and the same initial marking µ • in . Each labeled arc from S • appears in S • ⊥ . For each terminating rule r ∈ R 3 and each state q ∈ Q we add a self-loop q r -→ S • ⊥ q. Then we can check that S • ⊥ is prefix-realizable if and only if S • is realizable. This leads us to the main result of this section.

Theorem 2.15. It is undecidable whether a prefix-bounded VASS is prefix-realizable.

Proof. So far, we have proved that the PNS S is realizable if and only if the VASS S • is realizable. We can prove that

S • ⊥ is prefix-realizable if and only if S • is realizable. Assume first that S • ⊥ is prefix-realizable. Then Pref([[S • ⊥ ]]) = [[N • ⊥ ]] for some Petri net N • ⊥ . Let N • be the Petri net obtained from N •
⊥ by erasing all transitions corresponding to some terminating rule. It is clear that

[[S • ]] ⊆ [[N • ]]. To prove that S • is realizable, we simply check that [[N • ]] ⊆ [[S • ]]. Let K ∈ [[N • ]].
We build the label causal net K ⊥ from K by adding an occurrence of some terminating rule ⊥ : M ¨∅. This requires that M coincides with the marking reached by K.

Then K ⊥ is a process of N • ⊥ . Hence K ⊥ ∈ Pref([[S • ⊥ ]]). Thus K ⊥ is a prefix of some process K ′ ∈ [[u ′ ]] µ in where u ′ ∈ CS(S • ⊥ )
. Since the terminating rule ⊥ : M ¨∅ consumes all places from the marking reached by K, it must be the last rule of u ′ , and the single terminating rule of u ′ , i.e. u ′ = u • (⊥ : M ¨∅) for some u ∈ CS(S • ). Hence

K ⊥ = K ′ . Therefore K ∈ [[u]] µ in and K ∈ [[S • ]]. Assume now that S • is realizable. Then [[S • ]] = [[N • ]
] for some Petri net N • . Adding to the Petri net N • a transition for each terminating rule yields a new Petri net denoted by

N • ⊥ . We can check that [[S • ⊥ ]] = [[N • ⊥ ]], so S • ⊥ is prefix-realizable. It is clear that [[S • ⊥ ]] ⊆ [[N • ⊥ ]]. Let K ∈ [[N • ⊥ ]
] and u be a linear extension of the partial order of rules in K. Each terminating rule ⊥ : M ¨∅ may only occur in u as the last rule of u. Let v be the word obtained by removing the possible occurrence of some terminating rule

⊥ : M ¨∅ from u. Then v is a firable rule sequence of N • because u is a firable rule sequence of N • ⊥ . Since [[S • ]] = [[N • ]], we have [[v]] µ • in = [[v ′ ]] µ • in for some v ′ ∈ FCS(S • ). Then [[u]] µ • in = [[u ′ ]] µ • in for some u ′ ∈ FCS(S •
⊥ ) obtained from v ′ by adding possibly an occurrence some terminating rule.

Therefore K ∈ [[S • ⊥ ]].
As an immediate consequence, we can now establish the following fact.

Corollary 2.16. Given two prefix-bounded vector addition systems with states S 1 and S 2 , it is undecidable whether

[[S 1 ]] = [[S 2 ]] (resp. Pref([[S 1 ]]) = [[S 2 ]], Pref([[S 1 ]]) = Pref([[S 2 ]])).

Proof. By Proposition 2.3, a VASS S is realizable if and only if [[S]] = [[S ′

]] where S ′ is the VASS with a single state which admits a self-loop carrying r if r occurs in some firable computation sequence of S. By Proposition 1.4, we can effectively build S ′ from S.

By Theorem 2.14, [[S]] = [[S

′ ]] is undecidable. Therefore [[S 1 ]] = [[S 2 ]]
]]) = Pref([[S 2 ]]
) is undecidable for two vector addition systems with states.

The gap between vector addition systems with states and Petri nets is illustrated by the next result which shows that these decision problems are decidable if one considers (possibly unbounded) Petri nets only.

Proposition 2.17. Let N 1 and N 2 be two Petri nets. The property

[[N 1 ]] ⊆ [[N 2 ]] is decid- able.
Proof. Observe first that this property requires that N 1 and N 2 share the same initial marking. Let R i be the set of rules occurring in some firable computation sequence of N i . The set R i can be effectively computed (Prop. 1.4). Then

[[N 1 ]] ⊆ [[N 2 ]] if and only if R 1 ⊆ R 2 .

Checking reachability properties of process prefixes

Basic decision problems about the set of reachable markings of a Petri net are known to be decidable, namely boundedness, covering and reachability. Due to the simple simulation of a VASS by a Petri net recalled in Subsection 1.3 these results apply to the analysis of the reachable markings of a VASS or a PNS.

On the other hand, adopting a partial order semantics leads us to new difficulties and the model of VASSs is no longer equivalent to Petri nets. For instance the process language equality

[[S 1 ]] = [[S 2 ]] is
decidable for two Petri nets S 1 and S 2 , because one need simply to compare their initial markings and the two subsets of rules occurring in their firable rule sequences.

undecidable for two prefix-bounded VASSs S 1 and S 2 , because rational sets of Mazurkiewicz traces can be described by prefix-bounded VASSs.

Thus VASSs and Petri nets are no longer equivalent models under the process semantics.

In this section we investigate three basic verification problems about the set of markings reached by prefixes of processes: boundedness, covering and reachability. We show how to reduce these problems to the particular case of Petri nets in such a way that all complexity and decidability results extend from Petri nets to PNSs under the process semantics. Definition 3.1. A marking µ is prefix-reachable in a PNS S if there exists a prefix of a process of S which leads to the marking µ.

Thus any reachable marking marking is prefix-reachable. In the particular case of Petri nets, conversely, any prefix-reachable marking is reachable, because the class of processes is prefix-closed. However the set of prefix-reachable markings can differ from the set of reachable markings in general. For instance, each process of the PNS from Fig. 1 leads to a marking with at most 3 tokens whereas prefixes of these processes lead to infinitely many distinct markings (see in Fig. 2 a prefix of a process which leads to a marking with 4 tokens).

The first basic problem we consider is the prefix-boundedness problem, which asks whether the set of prefix-reachable markings of a given PNS S is finite. We give below a linear construction of a PNS S • from S such that S is prefix-bounded if and only if S • is bounded. Since the boundedness of S • boils down to the boundedness of a Petri net, we get that the prefix-boundedness problem for PNSs is computationally equivalent to the boundedness problem of Petri nets. Further we show that this technique apply to other similar basic problems about prefix-reachable markings, namely covering and reachability.

From Petri nets with states to Petri nets

Let S = (Q, ı, -→, µ in ) be a fixed PNS. We build a PNS S • that allows us to analyse the set of prefix-reachable markings of S. The construction of S • from S is illustrated by Fig. 15. The PNS S • makes use of three disjoint sets of places: P pre , P suf , P cut which are copies of the set of places P of S. We let π pre : P → P pre , π suf : P → P suf , and π cut : P → P cut be the bijections that map each place from P to the corresponding place in P pre , P cut and P suf respectively. These mappings extend naturally to mappings from multisets to multisets. The initial marking µ • in of S • is the multiset µ • in = π pre (µ in ). The PNS S • shares with S its set of states Q and its initial state ı. It consists of three disjoint sets of labeled arcs: -→ pre , -→ suf , -→ cut . The restriction of S • to the labeled arcs from -→ pre and to the places from P pre yields a PNS S • pre isomorphic to S. Thus for each labeled arc q 1 r -→ q 2 in S with r = (a, • r, r • ) there exists some labeled arc q 1 s -→ pre q 2 with s = (a, π pre ( • r), π pre (r • )). Similarly the restriction of S • to the labeled arcs from -→ suf and to the places from P suf yields a PNS S • suf isomorphic to S, except that its initial marking is empty: For each labeled arc q 1 r -→ q 2 in S with r = (a, • r, r • ) there exists some labeled arc q 1 s -→ suf q 2 with s = (a, π suf ( • r), π suf (r • )). Note that the two PNSs S • pre and S • suf are synchronized because they share a common set of state. The set of labeled arcs -→ cut consists of a self-loop q s -→ cut q for each state q and each place p ∈ P ; this labeled arc allows to move a token from the place π pre (p) to the place π suf (p) and to keep track of that transfer in the place π cut (p), i.e. • s = π pre (p) and s • = π suf (p) + π cut (p). Note that tokens in P cut cannot be consumed.

Intuitively, for any process K of S and for any prefix K ′ of K, the PNS S • can simulate a computation sequence of S which corresponds to K in such a way that each event from the prefix K ′ corresponds to the occurrence of a labeled arc from -→ pre and each event from the suffix K \ K ′ corresponds to the occurrence of a labeled arc from -→ suf . Moreover the set of places P cut keeps track of the tokens transferred from K to K ′ , i.e. from S • pre to S • suf , by labeled arcs from -→ cut . Thus any prefix-reachable marking of S is represented by the restriction to P pre ∪ P cut of some reachable marking of S • . The key property of this representation, stated in Prop. 3.2 below, asserts that, conversely, each firable computation sequence of S • corresponds to a process K of S and a prefix K ′ of K such that the marking of P pre ∪ P cut describes the marking reached by K ′ .

In order to prove our results in details, we shall adopt also the next notations:

-We denote by τ pre and τ suf the bijections that maps each labeled arc q r -→ q ′ from S to the corresponding labeled arc in -→ pre and -→ suf respectively.

-For each state q ∈ Q, we denote τ q cut the bijection between P and the self-loop labeled on q from -→ cut .

In the next statement and the sequel of this section, for each marking µ and for each subset of places X, we denote by µ|X the restriction of µ to the places from X. The main results of this section rely essentially on the next observation. Proposition 3.2. A multiset of places µ ∈ N P is prefix-reachable in S if and only if there exists some reachable marking µ

• of S • such that µ = π -1 pre (µ • |P pre ) + π -1 cut (µ • |P cut ).

Proof of Proposition 3.2

For each rule sequence u = r 1 ...r n ∈ R ⋆ , the cost of u is the vector cost(u)

∈ Z P such that cost(u)(p) = n i=1 • r i (p) -r i • (p)
for each p ∈ P . In particular the cost of the empty rule sequence is the null vector. If a rule sequence u is firable from a marking µ then the marking reached by u from µ is µcost(u). Let K be a process of a rule sequence u firable from µ. Then µcost(u) is the marking reached by K from µ. Moreover the marking µcost(u) corresponds to the set of conditions in K that are not input places of any event in K (which means intuitively that they are still available), i.e. to the maximal places of

K: We have µ -cost(u) = p∈max(K)∩P π(p).
For each rule r such that • r µcost(u), we let K • r denote the class of labeled causal nets obtained by adding to K an event that describes an occurrence of rule r which consumes • r available conditions from K.

Proof. Let K be a labeled causal net from [[v.w]] µ in ∩ [[u]] µ in . Since • a µ u , the class [[u.a]
] µ in is not empty (Prop. 3.3). Moreover all causal nets from [[u.a]] µ in are obtained from some causal net from [[u]] µ in by adding an occurrence of rule a. In particular we can add an occurrence of rule a to K and get a causal net from [[u.a]] µ in . The latter is also a causal

net from [[v.w.a]] µ in since K ∈ [[v.w]] µ in .
The proof of Prop. 3.2 relies on the two next technical lemmas which can be established by means of a bit tedious inductions. The first one asserts that for each firable computation sequence u ∈ FCS(S) and each prefix K v of each process K u ∈ [[u]] µ in , the VASS S • can be guided in order to simulate each rule of u in its sequential order so that the marking reached by u is described by the current marking of P pre ∪ P suf while the marking reached by K v is described by the current marking of P pre ∪ P cut . Furthermore we have to make sure that the state q ∈ Q reached by u is also reached by s in S • and to check that all events from K u that do not occur in K v are performed by transitions from -→ suf . To do so, we have to guide S • to transfer exactly the required number of tokens from P pre to P suf , which corresponds to the marking of P cut . Lemma 3.8. Let (u, v, w) be a partial computation in S and q be some state such that ı u -→ q in S. There exists some firable rule sequence s in S • which leads to the marking µ

• s such that (a) π -1 cut (µ • s |P cut ) + π -1 pre (µ • s |P pre ) = µ v , (b) π -1 suf (µ • s |P suf ) + π -1 pre (µ • s |P pre ) = µ u , (c) π -1 cut (µ • s |P cut ) = req(w), (d) ı s -→ q in S • .
Proof. We proceed by induction over the length of u. If |u| = 0 then u = ε, q = ı, v = ε and w = ε. The empty firing sequence of S • satisfies the four above properties because µ • in = π pre (µ in ). Induction step: We consider some partial computation (u ′ , v ′ , w ′ ) with |u ′ | = n + 1. We put u ′ = u.a with |u| = n and ı

u -→ q a -→ q ′ . Let K u ′ , K v ′ and K w ′ be three labeled causal nets such that K u ′ ∈ [[u ′ ]] µ in ∩ [[v ′ .w ′ ]] µ in , K v ′ ∈ [[v ′ ]] µ in is a prefix of K u ′ and K w ′ ∈ [[w ′ ]] µ v ′ is the corresponding suffix. We know that K u ′ is obtained from some process K u ∈ [[u]
] µ in by adding an event e a that corresponds to an occurrence of rule a. We distinguish two cases.

1. Event e a occurs in K w ′ . Then there is some rule sequence w such that

K w ′ ∈ [[w.a]] µ v ′ and K u ∈ [[v ′ .w]] µ in so (u, v ′ , w
) is a partial computation of length n. By induction hypothesis there exists some firable computation sequence s in S • such that the four above properties are satisfied. In particular, π -1 cut (µ • s |P cut ) = req(w). Moreover Prop. 3.5 ensures that req(w.a)

µ v ′ because K w ′ ∈ [[w.a]] µ v ′ . Furthermore we have on one hand π -1 cut (µ • s |P cut ) = req(w)
req(w.a); and on the other hand req(w.a)

µ v ′ i.e. req(w.a) π -1 cut (µ • s |P cut ) + π -1 pre (µ • s |P pre ). Therefore π -1 cut (µ • s |P cut ) req(w.a) π -1 cut (µ • s |P cut ) + π -1 pre (µ • s |P pre )
It follows that there is some multiset of places μ

∈ N P such that π -1 cut (µ • s |P cut ) + μ = req(w.a) with π pre (μ) µ • s |P pre .
We consider a sequence of transitions A ∈-→ ⋆ cut in S • which consumes the multiset of tokens π pre (μ) and produces the multiset of tokens π suf (μ). We have

• a + µ v -µ u = • a + cost(w) max(req(w), • a + cost(w)) = req(w.a)
Hence µ uµ v + req(w.a) • a. On the other hand

µ u -µ v +req(w.a) = µ u -µ v +π -1 cut (µ • s |P cut )+ μ = µ u -π -1 pre (µ • s |P pre )+ μ = π -1 suf (µ • s |P suf )+ μ Hence π -1 suf (µ • s.A |P suf ) = π -1 suf (µ • s |P suf ) + μ • a. It follows that s.A.τ suf (a)
is a firable computation sequence of S • . The latter satisfies the required conditions:

(a) π -1 pre (µ • s.A.τ suf (a) |P pre ) = π -1 pre (µ • s |P pre ) -μ and π -1 cut (µ • s.A.τ suf (a) |P cut ) = π -1 cut (µ • s |P cut ) + μ hence π -1 pre (µ • s.A.τ suf (a) |P pre )+π -1 cut (µ • s.A.τ suf (a) |P cut ) = π -1 pre (µ • s |P pre )+π -1 cut (µ • s |P cut ) = µ v ′ . (b) π -1 pre (µ • s.A.τ suf (a) |P pre ) = π -1 pre (µ • s |P pre )-μ, π -1 suf (µ • s.A.τ suf (a) |P suf ) = π -1 suf (µ • s |P suf )+ μ-• a+ a • therefore π -1 pre (µ • s.A.τ suf (a) |P pre )+π -1 suf (µ • s.A.τ suf (a) |P suf ) = π -1 pre (µ • s |P pre )+π -1 suf (µ • s |P suf )- • a + a • = µ u.a = µ u ′ . (c) π -1 cut (µ • s.A.τ suf (a) |P cut ) = π -1 cut (µ • s |P cut ) + μ = req(w.a). (d) ı s -→ q A -→ q ′′ τ suf (a) -→ q ′ . 2. Event e a occurs in K v ′ . Then there exists some v such that K v ′ ∈ [[v.a]] µ in and K u ∈ [[v.w ′ ]] µ in . It follows that (u, v, w ′
) is a partial computation of length n. By induction hypothesis, there exists some firable computation sequence s in S • such that the four above properties are satisfied. Then we have

• a µ v -req(w ′ ) = π -1 cut (µ • s |P cut ) + π -1 pre (µ • s |P pre ) -π -1 cut (µ • s |P cut ) = π -1 pre (µ • s |P pre ).
Therefore τ pre (a) can be fired from the marking µ • s and we get a new firable computation sequence s.τ pre (a). The latter fulfills the required properties.

(a) We have π -1 cut (µ • s.τpre(a) |P cut ) = π -1 cut (µ • s |P cut ) and π -1 pre (µ • s.τpre(a) |P pre ) = π -1 pre (µ • s |P pre ) - • a + a • , hence π -1 cut (µ • s.τpre(a) |P cut ) + π -1 pre (µ • s.τpre(a) |P pre ) = µ v.a . (b) Since π -1 suf (µ • s.τpre(a) |P suf ) = π -1 suf (µ • s |P suf ) and π -1 pre (µ • s.τpre(a) |P pre ) = π -1 pre (µ • s |P pre ) -• a + a • we get π -1 suf (µ • s.τpre(a) |P suf ) + π -1 pre (µ • s.τpre(a) |P pre ) = µ u.a = µ u ′ . (c) π -1 cut (µ • s.τpre(a) |P cut ) = π -1 cut (µ • s |P cut ) = req(w ′ ). (d) ı s -→ q τpre(a)
-→ q ′ . Lemma 3.9. Let (u, v, w) be a partial computation and a ∈ R be a rule such that • a + req(w) µ v . If u.a ∈ CS(S) then (u.a, v.a, w) is a partial computation.

Proof. Let K u ∈ [[u]] µ in and let K v ∈ [[v]
] µ in be a prefix of K u . Since w is firable from req(w), there exists some labeled causal net K w ∈ [[w]] req(w) . We can build a process K ′ u of u which admits K v as prefix and such that the suffix K ′ u \ K v corresponds to K w . In particular only req(w) tokens from the multiset µ v reached by K v are consumed by K w . Then we can add an occurrence of rule a to K ′ u which consumes • a remaining tokens from µ vreq(w).

Conversely we need to show that the marking of P pre ∪ P cut reached after any firable transition sequence s of S • corresponds to a prefix-reachable marking of S, i.e. to some partial computation (u, v, w). To do so, we have to build a firable rule sequence u ∈ FCS(S), a process

K u ∈ [[u]] µ in and a prefix K v ∈ [[v]
] µ in inductively from s. At each step the state reached by s coincides with the state reached by u. When S • applies an additional labeled arc a, the corresponding partial computation is either (u, v, w) if a ∈ r -→ cut ; or (u.r, v, w.r) if a ∈ r -→ suf ; or (u.r, v.r, w) if a ∈ r -→ pre . In this last case, the rule r and the sequence of rules w can be performed concurrently: Formally we shall establish that • r + req(w) µ v . This property follows actually from the fact that w can be fired from the marking obtained by the tokens transferred from P pre to P suf , i.e. π cut (req(w)) µ • s |P cut . Lemma 3.10. Let s be a firable rule sequence in S • leading to the state q and the marking µ • s . There exists some partial computation (u, v, w) of S such that

(a) π -1 cut (µ • s |P cut ) + π -1 pre (µ • s |P pre ) = µ v , (b) π -1 suf (µ • s |P suf ) + π -1 pre (µ • s |P pre ) = µ u , (c) π -1 cut (µ • s |P cut ) req(w), and (d) ı u -→ q in S.
Proof. We proceed by induction over the length of s. If |s| = 0 then s = ε; the empty partial computation (ε, ε, ε) satisfies the four requirements because µ • in = π pre (µ in ). Induction step: Let s.a be a firable computation sequence of length n + 1. By induction hypothesis, there exists some partial computation (u, v, w) which fulfills the four above requirements. We distinguish three cases:

1. q a -→ cut q in S • . Then we can check that (u, v, w) satisfies the four requirements for s.a.

(a) π -1 cut (µ • s.a |P cut ) + π -1 pre (µ • s.a |P pre ) = π -1 cut (µ • s |P cut ) + π -1 pre (µ • s |P pre ) = µ v . (b) π -1 suf (µ • s.a |P suf ) + π -1 pre (µ • s.a |P pre ) = π -1 suf (µ • s |P suf ) + π -1 pre (µ • s |P pre ) = µ u . (c) We have π -1 cut (µ • s.a |P cut ) > π -1 cut (µ • s |P cut ) req(w). (d) ı u -→ q by induction hypothesis. 2. q a -→ suf q ′ . Then τ -1
suf (a) is an arc q r -→ S q ′ in S and u.r is a computation sequence of S. Moreover π -1 suf ( • a|P suf ) = • r and π -1 suf (a

• |P suf ) = r • . Furthermore • a µ • s , hence • r π -1 suf (µ • s |P suf ) µ u . By Lemma 3.7 we know that (u.r, v, w.r) is a partial computation of S. Moreover (a) π -1 cut (µ • s.a |P cut ) + π -1 pre (µ • s.a |P pre ) = π -1 cut (µ • s |P cut ) + π -1 pre (µ • s |P pre ) = µ v . (b) π -1 suf (µ • s.a |P suf ) + π -1 pre (µ • s.a |P pre ) = π -1 suf (µ • s |P suf ) + π -1 pre (µ • s |P pre ) + π -1 suf (a • -• a|P suf ) = µ u -• r + r • = µ u.r . (c) We have µ s.a |P cut = µ s |P cut . Moreover • a µ • s , hence π -1 cut (µ • s |P cut ) π -1 cut (µ • s |P cut )+π -1 suf ( • a-µ • s |P suf ) = π -1 suf ( • a|P suf )+(µ v -µ u ) = • r+cost(w) Then π -1 cut (µ • s.a |P cut ) = π -1 cut (µ • s |P cut ) max(req(w), • r + cost(w)) = req(w.r). (d) ı u -→ q r -→ q ′ and ı s -→ q a -→ q ′ . 3. q a -→ pre q ′ . Then τ -1 pre (a) is an arc q r -→ S q ′ . Moreover π -1 pre ( • a|P pre ) = • r and π -1 pre (a • |P pre ) = r • . We observe first that (a) π -1 cut (µ • s.a |P cut ) + π -1 pre (µ • s.a |P pre ) = µ v -π -1 pre ( • a|P pre ) + π -1 pre (a • |P pre ) = µ v.r (b) π -1 suf (µ • s.a |P suf ) + π -1 pre (µ • s.a |P pre ) = µ u -π -1 pre ( • a|P pre ) + π -1 pre (a • |P pre ) = µ u.r (c) π -1 cut (µ • s.a |P cut ) = π -1 cut (µ • s |P cut ) req(w) (d) q r -→ q ′ in S. Since µ • s • a, we have π -1 pre (µ • s |P pre ) π -1 pre ( • a|P pre ). On the other hand, π -1 cut (µ • s |P cut ) req(w), hence π -1 pre (µ • s |P pre ) + π -1 cut (µ • s |P cut ) π -1
pre ( • a|P pre ) + req(w), i.e µ v • r + req(w). By Lemma 3.9, (u.r, v.r, w) is a partial computation.

We are now ready to prove Prop. 3.2. Let µ be the marking reached by a prefix K ′ of a process K ∈ [[S]]. According to Prop. 3.6, there exists some partial computation (u, v, w) such that µ v = µ. By Lemma 3.8, there exists some firable rule sequence s in S • such that

π -1 cut (µ • s |P cut ) + π -1 pre (µ • s |P pre ) = µ v = µ. Conversely if π -1 cut (µ • s |P cut ) + π -1 pre (µ • s |P pre ) =
µ for some firable rule sequence s in S • then Lemma 3.10 ensures that there exists some partial computation (u, v, w) such that π -1 cut (µ

• s |P cut ) + π -1 pre (µ • s |P pre ) = µ v .
Moreover Prop. 3.6 asserts that µ v is the marking reached by some prefix K ′ of some process K ∈ [[S]].

Analysis of prefix-reachable markings

At present we make use of the properties of the PNS S • , in particular Prop. 3.2, in order to derive some techniques to analyse the set of prefix-reachable markings of S. First, the prefix-boundedness problem asks whether the set of prefix-reachable markings of a given PNS S is finite. It is easy to prove that the PNS S is prefix-bounded if and only if the PNS S • is bounded, which can be checked by means of the usual linear simulation by a Petri net. Moreover, prefix-boundedness is equivalent to boundedness in the particular case of Petri nets because the set of processes of a Petri net is closed by prefixes. Thus, Theorem 3.11. The prefix-boundedness problem of PNSs is computationally equivalent to the boundedness problem of Petri nets.

Proof. It is clear from Prop. 3.2 that if S • is bounded then there are finitely many prefixreachable markings in S. Conversely, assume that S is prefix-bounded. Then there exists some M ∈ N such that µ v (p) M and µ u (p) M for all partial computations (u, v, w) of S and all places p ∈ P . Then Lemma 3.10 ensures that if a firable rule sequence of S • leads to some marking µ then µ(p) M for each place p ∈ P S • . Second, the prefix-covering problem asks whether a given multiset of places µ ∈ N P is covered by some prefix-reachable marking µ ′ ∈ N P , i.e. µ(p) µ ′ (p) for all p ∈ P . It is easy to see that µ is prefix-covered in S if and only if the multiset of places π cut (µ) is covered by some reachable marking of S • . Thus, Theorem 3.12. The prefix-covering problem for PNSs is computationally equivalent to the covering problem in Petri nets.

Theorem [START_REF] Büchi | Weak second-order arithmetic and finite automata[END_REF] which states the equivalence between the definability of a set of words by an MSO formula and its recognizability by a finite word automaton.

In the rest of this section, we fix a bounded PNS S with an initial marking µ in over the finite set of places P and the finite set of rules R. In order to simplify the presentation of our result, we consider in this section that the events of a process are labeled by a rule instead of a rule name. The MSO logic we consider applies to the class of partial orders whose nodes are labeled by letters from the disjoint union Σ = P ∪R, which includes in particular the processes of each rule sequence s ∈ R ⋆ . Thus the models we consider here are triples (N, , λ) where N is a finite set of nodes, is a partial order over N, and λ is a mapping from N to Σ = P ∪R.

MSO logic over words and labeled partial orders

Formulae of the MSO logic that we consider involve first-order variables x, y, z... for nodes and second-order variables X, Y, Z... for sets of nodes. They are built up from the atomic formulae P a (x) for a ∈ Σ (which stands for "the node x is labeled by the letter a"), x y, and x ∈ X by means of the Boolean connectives ¬, ∨, ∧, →, ↔ and quantifiers ∃, ∀ (both for first order and for set variables). Formulae without free variables are called sentences.

The satisfaction relation |= between a labeled partial order (N, , λ) and a sentence is defined canonically with the understanding that first order variables range over nodes of N and second order variables over subsets of N. The class of labeled partial orders which satisfy a sentence ϕ is denoted by Mod(ϕ). We say that a class of labeled partial orders L is MSO-definable if there exists a sentence ϕ such that L = Mod(ϕ).

A technique to decide S |= ψ

Since S is bounded, we can compute and fix some natural number B such that each reachable marking µ of S is B-bounded, that is, µ(p) B for each p ∈ P . A rule sequence s = r 1 ...r m ∈ R ⋆ firable from µ in is said to be B-bounded if the marking reached by each subsequence r 1 ...r l is B-bounded. In particular any firable computation sequence of S is B-bounded.

We fix a word w in ∈ P ⋆ that is a linear extension of µ in , i.e. |w in | p = µ in (p) for all p ∈ P . Similarly, for each rule r ∈ R, we fix a word w r = r.w ′ r where |w ′ r | p = r • (p) for all p ∈ P . Then for each rule sequence s = r 1 ...r m ∈ R ⋆ , the sequence w s = w in .w r 1 ...w rm is called the representative word of s. As usual, we will regard w s as a linearly ordered set of nodes labeled by letters from Σ and we will write w s = (N, , λ) where N is a set of nodes, is a total order over N, and λ : N → Σ is a labeling. Nodes labeled by a place are called place nodes whereas nodes labeled by a rule are called rule nodes. Interestingly, w s is a linear extension of any process of s, where the place nodes following a rule node labeled by r correspond to the multiset of tokens r • produced by this occurrence of r.

In order to recover a process of s from the representative word w s , we need to specify which available tokens are consumed by each occurrence of rule. To do so, we use a coloring of the place nodes of w s so that at each step all available tokens in a given place get distinct colors. Moreover we also provide rule nodes with a series of other colors in order to specify which tokens are consumed at each step of s. It ensures also that the tokens produced in some place by the occurrence of a rule get distinct colors. Consequently, at each step all available tokens in a place have distinct colors. In order to recover a process of s from a process coloring of w s , we have to make sure that there are enough available tokens when each rule is applied. The last requirement PC 3 guarantees that for each rule node which consumes a token colored by k in place p, some token of this kind occurred before the rule and has not been consumed in between. We can show that the notion of process coloring characterizes the linear extensions of processes and allows to recover a process from a word. This property is established by the two next statements (Prop. 4.2 and 4.3). Consider for instance the rule sequence s = pc from the initial marking µ in = {x, y, z} where p : x ¨x + z and c : y + z ¨y. A process coloring of w s = xyzpzxcy with B = 2 is given by the tabular on the left-hand side of Fig. 16. The corresponding process is depicted on the right-hand side of Fig. 16.

Proof. We proceed by induction over the length of s. The base case where |s| = 0 is trivial because µ in is B-bounded. Induction step. Let K = (B∪E, F * , λ) be a process of s = r 1 ...r m of length m 1 with set of conditions C and set of events E. We consider the subsequence s ′ = r 1 ...r m-1 and the prefix K ′ = (B ′ ∪ E ′ , F * , λ) of K in which the event e • ∈ E corresponding to the last occurrence of r m and the subsequent conditions are removed. Clearly K ′ is a process of s ′ . By induction hypothesis, there exists a process coloring (C ′ , D ′ ) of w s ′ such that K C ′ ,D ′ (s ′ ) = (N ′ , C ′ ,D ′ , λ) is isomorphic to K ′ = (B ′ ∪ E ′ , F, λ). We let σ : B ′ ∪ E ′ → N ′ denote an isomorphism from K ′ to K C ′ ,D ′ (s ′ ), i.e. a bijection such that x 1 F * x 2 iff σ(x 1 ) C ′ ,D ′ σ(x 2 ) for all x 1 , x 2 ∈ B ′ ∪ E ′ and λ(σ(x)) = λ(x) for all x ∈ B ′ ∪ E ′ .

We extend the bijection σ : B ′ ∪ E ′ → N ′ to a bijection σ : B ∪ E → N such that σ(e • ) is the rule node from N \ N ′ , and each condition c from B\B ′ maps to a place node σ(c) ∈ N \N ′ such that λ(σ(c)) = λ(c).

We extend also the process coloring (C ′ , D ′ ) to a process coloring (C, D) of w s in two steps:

1. For all places p ∈ P and for all colors k ∈ [1..B], the rule node σ(e • ) belongs to D p,k if the event e • covers a condition c such that the corresponding node σ(c) is labeled by p and colored by k, i.e. λ(c) = p and σ(c) ∈ C ′ k . 2. The colors of the additionnal place nodes from N \ N ′ are chosen arbitrarily such that all maximal conditions of K labeled by the same place p have distinct colors. This is possible because the marking reached by s is B-bounded.

We can check that the resulting coloring (C, D) is a process coloring. Recall that σ maps each condition from B \ B ′ to a place node from N \ N ′ with the same label. All these conditions cover e • and all these place nodes cover σ(e • ). To conclude, we need to check that for each place node n ∈ N ′ , we have n • ≺ C,D n • in K C,D (s) if and only if σ -1 (n)F e • in K.

any safe PNS is bounded. This constraint is interesting because checking whether a PNS is bounded and computing a bound is hard and requires exponential space [START_REF] Esparza | Decidability issues for Petri nets -a survey[END_REF]. Yet the technique presented in this section allows us to check effectively MSO properties of the processes derived from a bounded (non-safe) cMSG or more generally a bounded PNS. Since MSO behaviours can be characterized by some MSO sentence, this result extends the main result from [START_REF] Madhusudan | Beyond message sequence graphs[END_REF] which asserts that the model-checking problem for safe cMSGs is decidable (see also [START_REF] Genest | A Kleene theorem and model checking algorithms for existentially bounded communicating automata[END_REF]Cor 6.1]). As opposed to [START_REF] Genest | A Kleene theorem and model checking algorithms for existentially bounded communicating automata[END_REF][START_REF] Madhusudan | Beyond message sequence graphs[END_REF], we do not assume FIFO behaviours and consequently we cannot make use of the notion of representative linearizations. The fact is that, as already mentionned, a computation sequence can correspond to several nonisomorphic processes depending on the order identical particles are consumed. Therefore we need the notion of process coloring (Def. 4.1) to recover a process from a word. This is the main difference with the setting of MSCs because these are completely specified by any of their linearizations. Still, the FIFO restriction can be formalized in MSO logic and our technique applies also in this special case. Second Petri nets and VASSs abstract away from the notions of sites and channels in the setting of MSCs: A place can describe the local state of a site, a communication channel, a shared-variable, etc. In particular our approach applies to any bounded Petri net. To the best of our knowledge, the model checking problem of bounded Petri nets against MSO formulae under the process semantics has not been investigated so far in the literature. We show with an example below that the process semantics of Petri nets can be used to model and check systems with specific behavioural constraints, such as FIFO channels, causal communication, or private keys, as soon as these restrictions can be formalized by an MSO sentence. Note finally that it may be possible to encode a bounded Petri net with a safe cMSGs. However this requires to represents each reachable marking by a distinct control state so the size of the resulting cMSG would be exponential in the size of the Petri net even for 1-safe Petri nets.

Conclusion

We introduce a natural partial order semantics for vector addition systems with states (and Petri nets with states) which extends the non-branching process semantics of Petri nets and follows the asynchronous approach of message sequence charts. We show how basic problems about the set of markings reached along concurrent executions, such as boundedness, covering and reachability, can be solved similarly to the analogous problems for Petri nets. We show also how to check effectively any MSO property of these partial orders provided that the system is bounded. This result generalizes results known for message sequence graphs and is new, even in the restricted case of Petri nets.

However vector addition systems with states are not always as easy as Petri nets to handle. We have observed that vector addition systems with states are more expressive than (pure) Petri nets under this process semantics. Moreover the synthesis problem of Petri nets from prefix-bounded vector addition systems with states turns out to be undecidable. As a consequence we have illustrated the gap between Petri nets and vector addition systems with states as follows: It is undecidable whether two prefix-bounded vector addition systems with states are semantically equivalent, contrary to Petri nets.

Introduced as a formal model for the semantics of elementary Petri nets, Mazurkiewicz traces [START_REF] Mazurkiewicz | Concurrent program schemes and their interpretation[END_REF] are particular labeled partial orders that benefit from a rich and still growing theory [START_REF] Diekert | The Book of Traces[END_REF]. In particular we have made use of the undecidability of the universality problem for rational trace languages to establish all undecidability results presented in this paper. We have shown that Mazurkiewicz traces can be described as the processes of very particular prefix-bounded systems. However Mazurkiewicz trace theory enjoys several nice positive results for particular rational languages. Most of these results have been already adapted to the setting of message sequence charts (see in particular [START_REF] Henriksen | A theory of regular MSC languages[END_REF]). Thus, this study leads us to investigate an extension of Mazurkiewicz trace theory to the whole setting of prefix-bounded Petri nets with states. Moreover some classes of Petri nets with states for which realizability and prefix-realizability become decidable might arise from this study.

Fig. 1 .

 1 Fig. 1. A PNS with two control states Fig. 2. A labeled causal net and a prefix

Fig. 5 .

 5 Fig. 5. Simulation of a PNS by a Petri net

Fig. 6 .Fig. 7 .

 67 Fig. 6. Rule a : x + y ¨x + 2z Fig. 7. Two processes from x + y + z

Fig. 8 .

 8 Fig. 8. Sliding window protocol Fig. 9. A process with n = 1

Fig. 10 .

 10 Fig. 10. A non prefix-realizable PNS Fig. 11. Some implied process

Fig. 12 .

 12 Fig. 12. Some process corresponding to the rule sequence ρ(abcab) with a b

  (a)} and µ in = P . Note that there is exactly one rule (a, Loc(a), Loc(a)) ∈ R Σ for each action a ∈ Σ. Moreover these rules are synchronisation rules according to the next definition. Definition 2.7. A rule r = (λ, α, β) is a synchronisation rule if α = β and α(m) 1 for each m ∈ P . We consider the mapping ρ : Σ → R Σ such that ρ(a) = (a, Loc(a), Loc(a)). This bijection extends naturally to mapping between words over Σ and words over R Σ . Example 2.8. Let Σ = {a, b, c} provided with the independence relation a b. We consider P = {x, y} together with Loc(a) = {x}, Loc(b) = {y} and Loc(c) = {x, y}.

  Figure 12 depicts some process corresponding to the rule sequence ρ(abcab).

Theorem 2 . 10 .

 210 The property [[N]] ⊆ [[S]] is undecidable for a prefix-bounded PNS S and a bounded Petri net N.

1 .

 1 a ∈ R 2 or b ∈ R 2 . Then π(u 1 ) = π(u 2 ) hence π(u 1 ) ≃ π(u 2 ). 2. a ∈ R 1 and b ∈ R 1 . Since u 1 and u 2 are two linear extensions of K, the guards of a and b are disjoint. It follows that π(u 1 ).π(a).π(b) ≃ π(u 1 ).π(b).π(a) hence π(u 1 ) ≃ π(u 2 ).

Fig. 15 .

 15 Fig. 15. Verification of prefix-reachable markings

Fig. 16 .

 16 Fig. 16. A process coloring of ws = xyzpzxcy and the corresponding process

PC 1 :

 1 Let p ∈ P and n • = σ(e • ). Since K is a process, #{k ∈ [1..B] | n • ∈ D p,k } ( • λ(n • ))(p). We can check that all conditions labeled by p and covered by the event e• have distinct colors, because of PC 2 . Thus #{k ∈ [1..B] | n • ∈ D p,k } = ( • λ(n • ))(p).PC 2 : The required property holds for any two place nodes from w s ′ because (C ′ , D ′ ) is a process coloring. It holds also by construction for any two place nodes from N \N ′ . It holds also obviously if one place node belongs to N ′ and the other to N \ N ′ because the rule node n • occurs in between. PC 3 : The required property holds for each rule node n ∈ N ′ . Let p ∈ P and k ∈ [1..B] be such that n • ∈ D p,k . By definition of D p,k the event e • covers a condition c such that the corresponding node n = σ(c) is labeled by p and colored by k. Moreover there is no rule node n ′ between n and n • with n ′ ∈ D p,k .Otherwise the condition c would be also covered by some event in K ′ , hence c would be a branching condition in K.

  Any rule from R 1 occurs in some process of S 1 , so it must occur in some process of S ′ : Therefore it occurs on a self-loop in S ′ . Any other rule occurring on a self-loop in S ′ cannot occur in a firable computation sequence. Therefore we can remove it from S ′ without affecting the set of processes of S ′ . In other words we can assume S ′ = S 2 . A similar argument holds for realizability. Note that R 1 can be computed from S 1 (Prop. 1.4). Clearly Pref([[S 1

Petri net are prefix-closed. Further considering prefixes is often a means to focus on deadlock-free implementations of systems provided with a notion of accepting states. The next basic observation exhibits a canonical candidate for the synthesis of a Petri net from a Petri net with states.

Proposition 2.3. Let S 1 be a Petri net with states and R 1 be the subset of rules occurring in some firable computation sequence of S 1 . Let S 2 be the PNS provided with a single state and the same initial marking as S 1 such that a rule occurs on a self-loop in S 2 if and only if it belongs to R 1 . Then

1. S 1 is realizable if and only if [[S

1 ]] = [[S 2 ]]. 2. S 1 is prefix-realizable if and only if Pref([[S 1 ]]) = [[S 2 ]]. Proof. Assume first that S 1 is not prefix-realizable. Then Pref([[S 1 ]]) = [[S 2 ]

] because S 2 is equivalent to a Petri net. Assume now that S 1 is prefix-realizable. Then there exists some PNS S ′ with a single state such that Pref([

[S 1 ]]) = [[S ′ ]].

  is undecidable for two vector addition systems with states S 1 and S 2 .

Observe now that [[S

′ ]] = Pref([[S ′ ]]). It follows that [[S 1 ]] = Pref([[S 2 ]]) is

undecidable for two given chemical rule systems S 1 and S 2 . Finally, S is prefix-realizable if and only if Pref([[S]]) = Pref([[S ′ ]]). It follows from Theorem 2.15 that Pref([[S 1

  Definition 4.1. Let w = (N, , λ) be a linear order of nodes labeled by Σ. A process coloring of w consists of a partition C = {C 1 , ..., C B } of the set of place nodes; a place node n ∈ N is said to be colored by k in place p if λ(n) = p and n ∈ C k . -for each place p ∈ P and each k ∈ [1..B], a subset of rule nodes D p,k ; we say that a rule node n ∈ N consumes a token colored by k in place p if n ∈ D p,k .Thus the condition PC 1 asserts that n consumes the appropriate multiset of tokens in each place, provided that these tokens have distinct colors. Precisely PC 2 guarantees that the colors given to new tokens produced by the occurrence of a rule in a place differ from the colors used by available tokens in this place.

Moreover the three next conditions must be satisfied:

PC 1 : For each rule node n, for each place p ∈ P : #{k ∈ [1..B] | n ∈ D p,k } = ( • λ(n))(

p); PC 2 : For each place p ∈ P and each color k ∈ [1..B], any two place nodes colored by k in place p are separated by some rule node which consumes a token colored by k in place p; PC 3 : For each rule node n which consumes a token colored by k in place p, there exists some preceding place node n ′ < n colored by k in place p such that no rule node between n ′ and n consumes a token colored by k in place p. Intuitively a place node belongs to C k if it describes a token colored by k in place λ(n) ∈ P . A rule node n belongs to D p,k if it describes an occurrence of the rule λ(n) ∈ R which consumes a token colored by k in place p.

Proposition 3.3. Let µ ∈ N P . The class of processes of a rule sequence u ∈ R ⋆ satisfies the three following properties:

-If u is empty, i.e. u = ε, then each process from [[ε]] µ consists of p∈P µ(p) conditions and no event.

for all rules r ∈ R, [[u.r]] µ is empty if [[u]] µ is empty or • r µcost(u).

for all rules r ∈ R, if [[u]] µ is not empty and • r µcost(u) then [[u.r]] µ collects all processes from K • r for all processes K ∈ [[u]] µ .

Proof. By Definition 1.5, a process of the empty rule sequence from a marking µ consists of a set of labeled places which represents µ. Consider a rule sequence u and a rule r. Assume that [[u.r]] µ is not empty. Let K be a labeled causal net from [[u.r]] µ . We have already noticed that some prefix K ′ of K is a process of u from µ. Therefore [[u]] µ is not empty. Moreover K belongs to K ′ • r. Since u.r is a firable rule sequence, • r is smaller than the marking reached by u from µ, i.e. • r µcost(u). Thus, if [[u]] µ is empty or • r > µcost(u) then [[u.r]] µ is empty. On the other hand, if [[u]] µ is not empty and • r µcost(u) then any labeled causal net from K ′ • r where K ′ ∈ [[u]] µ is clearly a process of u.r from µ. Further any process from [[u.r]] µ can be obtained in this way. Given two multisets of places µ 1 , µ 2 ∈ N P , the maximum max(µ 1 , µ 2 ) collects the maximal number of tokens in each place: max(µ 1 , µ 2 )(p) = max(µ 1 (p), µ 2 (p)) for each p ∈ P . We will make use of the following requirement function req : R ⋆ → N P . Definition 3.4. The requirement of a rule sequence u ∈ R ⋆ is the multiset of places defined inductively as follows:

req(ε) = 0, -req(u.a) = max(req(u), • a + cost(u)) for all u ∈ R ⋆ and all a ∈ R.

The next observation shows that the requirement of a rule sequence u is the minimal marking µ such that u is firable from µ, i.e. [[u]

Proof. We proceed by induction over the length of u. If u = ε then req(u) = 0 hence µ req(u). Moreover [[ε]] µ contains each labeled causal net with no event and with a set of conditions representing the marking µ. For each rule sequence u = r 1 ...r n ∈ R ⋆ firable from µ in , we let µ u denote the marking reached by u from µ in , i.e.

Similarly for each transition sequence s ∈ T ⋆ N firable from the initial marking µ • in , µ • s denotes the marking reached by s in S • . We shall use the following notion of partial computation:

A partial computation is used as a witness for a process K u of u and a prefix K v of K u with K v ∈ [[v]] µ in . Note that v need not to be a prefix of u, nor to be a computation sequence of S. Partial computations are closely related to prefix-reachable markings, as the next basic observation shows. Proposition 3.6. For each partial computation (u, v, w), the marking µ v is prefix-reachable. Conversely, for any prefix-reachable marking µ, there exists some partial computation (u, v, w) such that µ = µ v .

Proof. Let (u, v, w) be a partial computation: There exists some labeled causal net

] µ in with u ∈ CS(S) and K ′ be a prefix of K. Let v be a linear extension of the partial order of rules occurring in

] µ in and µ v is the marking reached by K ′ . Let w be a linear extension of the partial order of rules occurring in the suffix K \ K ′ . Then v.w is a linear extension of the partial order of rules occurring in Proof. The prefix-covering problem is equivalent to the covering problem in the particular case of Petri nets. Thus the prefix-covering problem of PNSs is as difficult as the covering problem of Petri nets. Moreover checking the coverability of a given marking by the reachable markings of a PNS can be checked by means of the linear simulation of a PNS by a Petri net. Thus we need simply to show that a marking µ 0 is prefix-covered in S if and only if the multiset of places π cut (µ 0 ) is covered by some reachable marking of S • .

Let µ 0 ∈ N P be a multiset of places. Assume first that µ 0 is covered by some prefixreachable marking µ of S: µ 0 µ. By Prop. 3.2, there exists some reachable marking µ

Conversely, assume now that π cut (µ 0 ) µ • for some reachable marking µ • of S • . Then, by Lemma 3.10 and Prop. 3.6, µ 0 π -1 cut (µ • |P cut ) µ for some prefix-reachable marking µ of S.

Last but not least, the prefix-reachability problem asks whether a given multiset of places is prefix-reachable in S. Let us consider a slight modification S ′ of S • where for each place p ∈ P suf , each state q ∈ S • is provided with an additional self-loop labeled arc which carries a rule that consumes a token from p and produces nothing. Then a multiset µ of places is prefix-reachable in S if and only if π cut (µ) is reachable in S ′ . Thus, Theorem 3.13. The prefix-reachability problem of PNSs is computationally equivalent to the reachability problem of Petri nets.

Proof. The prefix-reachability problem is equivalent to the reachability problem in the particular case of Petri nets. Thus the prefix-reachability problem of PNSs is as difficult as the reachability problem of Petri nets. Moreover checking the reachability of a given marking in a PNS can be checked by means of the linear simulation of a PNS by a Petri net. Thus we need simply to show that a multiset µ of places is prefix-reachable in S if and only if π cut (µ) is reachable in S ′ .

Let µ ∈ N P be a multiset of places. Assume first that µ is prefix-reachable in S. By Prop. 3.2, there exists some reachable marking µ

Due to the self-loop labeled arcs from -→ cut in S • , we can assume that µ • |P pre = 0 hence π cut (µ) = µ • |P cut . Then π cut (µ) is reachable in S ′ because the additional self-loop labeled arcs of S ′ enable us to remove all tokens in all places from P suf . Conversely, assume that π cut (µ) is reachable in S ′ . Then there exists some reachable marking µ • in S • such that π cut (µ) = µ ′ |P cut and µ • |P pre = 0. It follows from Lemma 3.10 and Prop. 3.6 that µ is prefix-reachable in S.

Checking MSO properties of processes

In this section we show how to check effectively whether all processes of a given bounded Petri net with states S satisfy a formula ψ expressed in monadic second-order (MSO) logic. To the best of our knowledge, this model-checking problem has not been tackled yet, even in the particular case of Petri nets. Our approach is rather simple and relies only on Büchi either x is a rule node and y is a following place node with no rule node in between or y is a rule node and x is a preceding place node colored by k in place p such that y consumes a token colored with k in place p and no rule node between x and y consumes a token colored with k in place p.

Let be the reflexive and transitive closure of • ≺ . Then the labeled partial order (N, , λ) is a process of s firable from µ in , denoted by K C,D (s). Moreover s is B-bounded.

Proof. We proceed by induction over the length of s. The base case where |s| = 0 is trivial because • ≺ is empty and µ in (p) B for each p ∈ P . Induction step. Let s = r 1 ...r m be a sequence of length m 1 and w s = (N, , λ) be its representative word. Let (C, D) be a process coloring of w s . We consider the subsequence s ′ = r 1 ...r m-1 and its representative word w s ′ = (N ′ , , λ) with N ′ N. It is easy to check that the restriction of the process coloring (C, D) to the nodes from N ′ is a process coloring of w s ′ . Let • ≺ s ′ be the corresponding binary relation over N ′ and s ′ be the corresponding partial order. By induction hypothesis, (N ′ , s ′ , λ) is a process K ′ of s ′ and s ′ is a rule sequence firable from µ in and B-bounded. Note that the binary relation • ≺ is acyclic. Moreover the restriction of (N, , λ) to nodes of N ′ is precisely the process K ′ = (N ′ , s ′ , λ) of s ′ . We need to check that adding the nodes from N \ N ′ to K ′ according to • ≺ yields a process of s. To do so, we check the three next properties:

1. For each place p ∈ P , the rule node n • ∈ N \ N ′ corresponding to r k covers at most

• r k (p) place nodes labeled by p, i.e. #{n

. This follows from PC 1 and PC 2 . 2. For each place p ∈ P , the rule node n • ∈ N \ N ′ corresponding to r k covers at least

• r k (p) place nodes labeled by p, i.e. #{n

. This follows from PC 1 and PC 3 . 3. The conditions do not branch, i.e. for each place node n ∈ N, if n • ≺ n 1 and n • ≺ n 2 then n 1 = n 2 . This is ensured by the definition of • ≺ itself.

It follows that the labeled partial order K = (N, , λ) is a process of s. Thus s is firable from µ in . Finally for each place p and each color k, PC 2 guarantees that at most one place node colored by k in place p is not covered by a rule node. Therefore the marking µ reached by the process K satisfies µ(p) B for all p ∈ P . Thus s is B-bounded.

Thus each process coloring of w s yields a process from [[s]] µ in . Consequently s is firable from µ in as soon as it admits a process coloring. With no surprise s has to be B-bounded, too. Conversely the next result asserts that each process of any rule sequence s firable from µ in can be obtained by some process coloring of w s , provided that s is B-bounded. Conversely, assume now that σ -1 (n)F e • in K. Let p = λ(n) and k be the color such that n ∈ C k . We have n • ∈ D p,k according to the definition of D p,k . No event in K ′ covers σ -1 (n) so there exists no rule node in w s ′ after n which is colored by D p,k . It follows that n • ≺ C,D n • . Thus the notion of process coloring characterizes the processes of any B-bounded rule sequence firable from µ in .

Following the easy part of Büchi Theorem, we can design an MSO formula φ S which defines the words w = (N, , λ) over Σ which are representative words of a computation sequence of S. We can also design a formula Let ψ be an MSO sentence for labeled partial orders over Σ. We consider the following formula ψ S for words over Σ:

where the formula ψ ′ (C, D) is obtained from ψ by replacing each occurrence of x y by φ (x, y, C, D). Thus a word satisfies ψ S if (and only if) it is a representative word of a computation sequence s of S for which there exists a process coloring which describes a process satisfying ¬ψ. In this way we get the main result of this section. Theorem 4.4. Let S be a bounded PNS and ψ be an MSO sentence over causal nets. All processes of S satisfy ψ if and only if the word sentence ψ S is not satisfiable.

Thus the model-checking problem for a bounded PNS against an MSO-sentence is decidable. In practice, the unsatisfiability of ψ S is reduced to the emptiness problem of a finite automaton. It is of course more efficient not to include the sentence φ S and to compare the resulting automaton with the automaton that recognizes the representative words of computation sequences of S. Noteworthy we could provide the PNS S with a subset of accepting states and check alternatively that all processes derived from an accepting computation sequence satisfy ψ.

Comparisons to related works

This result subsumes previous works in several extents. A cMSG is said to be safe if all paths from the initial state to some fixed state lead to the same marking. Consequently,