The notion of persistency, based on the rule “no action can disable another one” is one of the classical notions in concurrency theory. In this paper, we deal with arbitrary place/transition nets, but concentrate on their persistent computations. It leads to an interesting decision problem: Is a given marking reachable with a persistent run? In order to study the persistent-reachability problem we define a class of nets, called nonviolence nets. We show that inhibitor nets can be simulated by the nonviolence nets, and that reachability and coverability problems are undecidable in the class of the nonviolence nets. Then we prove more: nonviolence nets can be simulated by the inhibitor nets, thus they are computationally equivalent to Turing machines.
An action of a concurrent system is said to be persistent if, whenever it becomes
enabled, it remains enabled until executed. This classical notion, introduced by
Karp/Miller [
It is well known that the classical versions of the problems (Is a given marking
reachable (coverable) in a given place/transition net?) are decidable (coverability:
Karp/Miller [
Many extensions of Petri nets are known to be Turing powerful: inhibitor nets,
priority nets (Hack [
In the concluding section we notice that the free-choice nonviolence nets are easy transformable to place/transition nets (not necessarily free-choice ones). Hence, the coverability and reachability problems are decidable in the class of the free-choice nonviolence nets.
The set of non-negative integers is denoted by . Given a set X, the cardinality (number of elements) of X is denoted by |X|, the powerset (set of all subsets) by 2X, the cardinality of the powerset is 2|X|. Multisets over X are members of X, i.e. functions from X into . For convenience, if the set X is finite, multisets of X will be represented by vectors of |X|. 2.1
Petri Nets and Their Computations
The definitions concerning Petri nets are mostly based on Desel/Reisig [
For all a∈T we denote: •a = {p∈P | (p,a)∈F} - the set of entries to a a• = {p∈P | (a,p)∈F} - the set of exits from a Petri nets admit a natural graphical representation. Nodes represent places and transitions, arcs represent the flow relation. Places are depicted by circles, and transitions by boxes. The set of all finite strings of transitions is denoted by T*, the empty string is denoted by ε, the length of w∈T* is denoted by |w|, number of occurrences of a transition a in a string w is denoted by |w|a.
Place/transition net (shortly, p/t-net) is a quadruple S = (P,T,F,M0), where: • N = (P,T,F) is a net, as defined above; • M0∈ P is a multiset of places, named the initial marking; it is marked by tokens inside the circles, capacity of places is unlimited.
Multisets of places are named markings. In the context of place/transition nets, they are mostly represented by nonnegative integer vectors of dimension |P|, assuming that P is strictly ordered. The natural generalizations, for vectors, of arithmetic operations + and - , as well as the partial order ≤, all defined componentwise, are well known and their formal definitions are omitted. A transition a∈T is enabled in a marking M whenever •a≤M (all its entries are marked). If a is enabled in M, then it can be executed, but the execution is not forced. The execution of a transition a changes the current marking M to the new marking M'=(M- •a)+a• (tokens are removed from entries, then put to exits). We shall denote: Ma for “a is enabled in M ” and MaM' for “a is enabled in M and M' is the resulting marking”. Then we say that MaM' is a step. This denotation we extend to strings of transitions: the empty string ε is enabled in any marking (always MεM), a string w=au (a∈T, u∈T*) is enabled in a marking M whenever MaM' and u is enabled in M'. Predicates Mw and MwM' are defined like those for single transitions. If MwM' then we say that MwM' is a computation from M to M'. Note that any computation MwM' unambiguously defines all intermediate markings between M and M'.
If MwM', for some w∈T*, then M' is said to be reachable from M. The set of all
markings reachable from M is denoted by [M〉. Given a place/transition net
S=(P,T,F,M0), the set [M0〉 of all markings reachable from the initial marking M0 is
called the reachability set of S, and markings in [M0〉 are said to be reachable in S.
We assume that the notions of reachability and coverability graphs are known to the
reader. Their definitions can be found in any monograph or survey about Petri nets
(see [
Let S=(P,T,F,M0) be a place/transition net, and let M be a marking. The step MaM' is persistent iff (∀b≠a) if Mb then M'b. The empty computation MεM is persistent; the computation MaM'uM" is persistent iff the step MaM' is persistent and the computation M'uM" is persistent. [In words: A computation is said to be persistent if any transition once enabled during this computation remains enabled until executed.] A p/t net is said to be persistent if it admits only persistent computations.
a
c
a
b
c
The problem of persistency (“Is a place/transition net persistent?”), raised by
Landweber and Robertson in [
Let S=(P,T,F,M0) be a place/transition net, and let M∈
Reachability Problem: Is there a computation M0wM?
In other words: Is the marking M reachable in the net S?
The Reachability Problem has been proved to be decidable by Mayr [
Let S=(P,T,F,M0) be a place/transition net, and let M∈
Persistent-Reachability Problem: Is there a persistent computation M0wM ? In other words: Is the marking M reachable in the net S with a persistent run? Obviously, if a p/t-net is persistent, then the persistent-reachability problem is equivalent to the classical one, thus decidable. We shall study the problem in general, for arbitrary p/t-nets. The following examples show difference between complete behaviours and persistent behaviours. Example 2.2. Comparison of the complete and persistent behaviours The above net is bounded (i.e. its reachability set is finite) and has infinite set of persistent computations. The example below shows an unbounded net (i.e. with infinite reachability set) with finite set (a singleton) of persistent computations. Example 2.3. Unbounded p/t-net with finite persistency graph d a b
c 1 2 a c b 3 1 2 c c 0-0-0 0-0-1 d d
In this section, we introduce the notion of nonviolence Petri nets. They differ from place/transition nets only by the execution rule. Namely, an enabled transition can be executed only if it is executable persistently (i.e. if its execution does not disable any other enabled transition). Therefore, we have to distinguish the notion “enabled” and “executable”, that are synonymic in place/transition nets, but not in nonviolence nets.
Nonviolence net is a quadruple S = (P,T,F,M0), exactly the same as in definition of place/transition nets. It differs from p/t-net by execution rules: A transition a∈T is enabled in a marking M whenever •a≤M (all its entries are marked). A transition a∈T is executable in M if it is enabled in M, and moreover the step MaM' is persistent. The execution of a leads to the resulting marking M'=(M- •a)+a• (exactly same as in p/tnets). We shall denote: Ma for “a is executable in M ” and MaM' for “a is executable in M and M' is the resulting marking”. Then we say that MaM' is a nonviolent step. This denotation is naturally extended to strings w∈T*. If MwM' then we say that MwM' is a nonviolent computation. Only nonviolent steps and computations are permitted in the nonviolence nets.
And now we can formulate the reachability and coverability problems for the nonviolence nets.
Let S = (P,T,F,M0) be a nonviolence net, and let M∈ P be a marking. NV-Reachability Problem: Is there a nonviolence computation M0wM in S? NV-Coverability Problem: Is there a marking M' ≥ M and a nonviolence computation M0wM' in S? 3.2 From Place/Transition Nets to Nonviolence Nets We shall show that every p/t-net can be simulated by a nonviolence net. It will be done by joining an external control to each transition of the net.
Let us consider an arbitrary p/t-net S. We transform it to the nonviolence net S' in the following way. To each transition a in the net S we join a switching transition a' and two new places pa and qa. We add the place qa to the set of entries to a and to the set of exits from a'. We also add the place pa to the set of exits from a and to the set of entries to a'. In initial marking we add one token to the place pa. One can treat the constructed loop as a preparation of the transition a to execution. Let us also define, for every marking M in the net S, the marking 10M in the net S' as follows. For each place p in the net S we set 10M(p)=M(p), for each new place pa we pa qa set 10M(pa)=1 and for each new place qa we set 10M(qa)=0. With such definition, the initial marking in the net S' is 10M0, where M0 is the initial marking in S. An obvious observation is that if transition a is executable in a marking M in the net S, then the sequence a'a is executable in the marking 10M in the net S'.
Proposition 3.2. A marking M is reachable in a place/transition net S if and only if the marking 10M is reachable in the nonviolence net S'.
Proof. (⇒) Let M0wM be a computation in S. Then replacing each a in w by a'a we get a computation 10M0w'10M in the nonviolence net S'. (⇐) Let 10M0w'10M in the nonviolence net S'. The only difference between behaviours of S and S' is that before every transition a a transition a' must be executed. Subsequent execution of two (or more) primed actions may sometimes disable the nonviolence execution of actions that were executable in S. However, it would not make any new action executable. Therefore, erasing all primed actions in w', we get a computation w such that M0wM is a computation in the p/t-net S. 4 Comparison of Nonviolence Nets and Inhibitor Nets In this section, we recall the notion of inhibitor nets and some of their properties (undecidability of the the reachability and coverability problems). Then we show that their computational power is equal to that of the nonviolence nets.
Definition 4.1. Inhibitor Petri Nets Inhibitor net is a quintuple S = (P,T,F,I,M0), where (P,T,F,M0) is a place/transition net and I ⊆ P×T is the set of inhibitor arcs (depicted by edges ended with a small empty circle). Sets of entries and exits are denoted by •a and a•, as in p/t-nets; the set of inhibitor entries to a is denoted by °a={p∈P | (p,a)∈I}.
A transition a∈T is enabled in a marking M whenever •a≤M (all its entries are marked) and (∀p∈°a) M(p)= 0 – all inhibitor entries to a are empty. And “executable” means “enabled”, like in p/t-nets. The execution of a leads to the resulting marking M'= (M- •a)+a•.
It is known that the inhibitor nets are computationally equivalent to Turing machines
and the reachability problem in them is undecidable (Minsky [
Let S = (P,T,F,I,M0) be an arbitrary inhibitor net with P = {p1, … , pk}, and let M = [i1, … , ik] be a marking to be checked to be reachable. We extend it to an inhibitor net S', as follows: We add three new places p0, pk+1, pk+2 and two new transitions x, y, connected p0→x→pk+1→y→pk+2 (see figure 5). Moreover, we join the place p0 with every transition of the net S by a self-loop (it is depicted symbolically on Figure 5), we add the arcs from pn to x, weighted by in (for n=1,…,k), [We use here the weighted arcs; see remark below.] and the inhibitory arcs from all original places of S to y. And the initial marking M'0 in S' is the following: M'0(p0)=1, M'0(pn)=M0(pn) for n=1,…,k and M'0(pk+1)=M'0(pk+2)=0.
Net S:
Net S': p1 pk . . .
p1 pk . . .
i1 . . . . . .
ik
x
y
p0
pk+1
pk+2
Remark. In this construction, we have used weighted (multiple) arcs. They are not
mentioned, for simplicity, in our definitions; we assume that the notion is commonly
known. Moreover, (place/transition or inhibitor) nets with multiple arcs can be
transformed to the equivalent nets without them (Hack [
From Inhibitor Nets to Nonviolence Nets Let us consider an arbitrary inhibitor net S. In the transformation to the nonviolence net S' we will use the same idea as in the previous transformation. Like in that one, to each transition a, we add a transition a' and places pa and qa. Moreover, to each place p, in the net S, belonging to °a (i.e. being an inhibitor entry to a), we add a new transition ap. Both places, p and qa, are joined by self-loops with the new transition ap.
Finally, we remove all inhibitor arcs. Net S:
Net S': p a p a ap a' pa qa Similarly to the construction of figure 4, for every marking M in the net S we define the marking 10M in the net S', in the same way. And the initial marking in the net S' is 10M0, where M0 is the initial marking in the net S. In the same manner as in the previous case, if the transition a is executable in the marking M in the inhibitor net S, then the computation a'a is executable in the marking 10M in the nonviolence net S'. Proposition 4.4. The marking M is reachable in the inhibitor net S if and only if the marking 10M is reachable in the nonviolence net S'.
Proof. The proof is similar to that of Proposition 3.2. Remark that if an action a' is executed while a token resides in the place p (so a is not enabled in S), then a token will stuck in the place qa and no marking of the form 10M will be reachable. Corollary 4.5. The NV-Reachability Problem is undecidable.
Proof. Directly from Proposition 4.4 and Fact 4.2.
Proposition 4.6. The marking M is coverable in the inhibitor net S if and only if the marking 10M is coverable in the nonviolence net S'.
Proof. (⇒) If M is coverable in S then there is a marking M' ≥ M reachable in S. Hence, by Proposition 4.4, the marking 10M' is reachable in the nonviolence net S'. And clearly, 10M' covers 10M. (⇐) Notice that any marking (reachable in S') covering 10M is of the form 10M'. And then M' ≥ M and M' is reachable in S (Proposition 4.4). So M is coverable in S. Corollary 4.7. The NV-Coverability Problem is undecidable.
Proof. Directly from Proposition 4.6 and Fact 4.3. 4.2
From Nonviolence Nets to Inhibitor Nets The inverse construction, transforming a nonviolence net into an inhibitor net, is more involved. Once more, we use the idea of predicting an executablement of transitions.
Net S:
xapb tapb taqb yapb Let S be a nonviolence net; we extend it to an inhibitor net S', as follows. First, we add one global place s, called the switch, which is an exit from every transition of the net S. Then, for every transition a of the net S, we add a transition a'; the switch place s is an entry to each of these primed transitions. An execution of a transition a' means a belief in the executablement of transition a in the nonviolence net S. After executing the transition a', the net S' checks, if the transition a was really executable in the nonviolence net S. It means that transition a is enabled and no other transition blocks its execution. In order to check it, we add, for every pair (p,b) such that b≠a and the place p is a common entry to the transitions a and b, the places xapb and yapb and the transition tapb, as depicted on figure 7 above. The transition tapb is able to move the token from xapb to yapb only if at least two tokens reside in the place p. [We use here the weighted arcs; see remark after figure 5.] By the nonviolence rules, a transition b blocks nothing if it is not enabled; it means that one of its entries is empty. In order to check it, we add the transitions taqb, for every entry q to transition b, different from p. Each of the transitions has one entry xapb, one exit yapb and one inhibitor arc from the place q, checking if q is empty. This construction allows to check, whether the transition b blocks the execution of a or not. If not, then a token moves from xapb to yapb, enabling a in S' if and only if it was executable in S.
For every marking M in the nonviolence net S we define a marking 10M in the inhibitor net S' as follows. For each place p inside the net S we set 10M(p)=M(p). For additional switch place s we set 10M(s)=1 and for every place r added by the construction (i.e. for all places xapb and yapb) we set 10M(r)=0. Directly from our construction, if a transition a is executable in a marking M in nonviolence net S then it is potentially executable in the marking 10M in inhibitor net S' (before executing a transition a we execute a transition a' and positively check all conditions to fill all places yapb). The initial marking of S' is assumed to be 10M0.
Proposition 4.8. The marking M in the nonviolence net S is reachable if and only if the marking 10M is reachable in the inhibitor net S'.
Proof. (⇒) In the net S' we can reach marking 10M, from the initial marking 10M0, by executing a transition a' before each transition a and checking the conditions. (⇐) Executing any transition a from the original net S is possible only by predicting this execution by executing the transition a'. If we do a mistake, making wrong prediction, our net S' would reach a dead marking and stops. It means that if a marking 10M in the inhibitor net S' is reachable, then the only scenario of reaching that marking is correctly predicting and executing transitions from the net S. The correctness of our process of predicting means that we could just execute these transitions in the original, nonviolence net S, reaching marking M. Finally, marking M is reachable in the nonviolence net S, which ends the proof.
We have proved (Propositions 4.4 + 4.8) that nonviolence nets are equivalent (in the marking reachability sense) to inhibitor nets. As the latter are Turing powerful, one can say that the former allow to do everything what possible without any fight. It is quite surprising, because persistent executions are only a part of arbitrary executions. But the price for the peace is undecidability. We have shown (Corollary 4.7) that even coverability, decidable in many extensions of place/transition nets, is undecidable in the class of the nonviolence nets.
Notice that free-choice (if •a∩•b ≠ ∅ then •a = •b) nonviolence nets can be simulated by place/transition nets (Figure 8), thus the classical decision problems (reachability, coverability) are decidable in the class of free-choice nonviolence nets.
Net S: a b
b Net S': a 2 Let S be a free-choice nonviolence net. We replace every arc from a place, being a common entry of two (or more) transitions and is not a part of a self-loop, by two arcs: an arc from the place to the transition, weighted with 2, and an arc from the transition to the place, weighted with 1. And self-loops remain not changed. And the initial marking remains the same. Clearly, the place/transition net S' built this way works exactly as the free-choice nonviolence net S. A case of the free-choice nonviolence net is shown by Example 2.2. The above construction does not work for non-free-choice nonviolence nets, see Example 2.3, for instance.
It would be interesting to study some other subclasses of the class of nonviolence nets. Especially, to find a subclass of the class of nonviolence nets, computationally equivalent to the class of place/transition nets.
The paper was inspired by the Example 2.2. Great thanks are due to Ulla Goltz, who recalled to us that very old example.