The notion of persistency, based on the rule "no action can disable another one" is one of the classical notions in concurrency theory. We recall two ways of generalization of this notion: the first is "no action can kill another one" and the second "no action can kill another enabled one". Afterwards we present an infinite hierarchy of computations in which one action disables another one for no longer than a specified number of steps (e/l-k-persistency). We prove that if an action is disabled, and not killed, by another one, it can not be postponed indefinitely. Finally we deal with decision problems about e/l-k persistency. We show that this kind of persistency is decidable with respect to steps, markings and nets.
The notion of persistency is one of the most frequently discussed issues in the
Petri net theory - [
We say that an action of a processing system is persistent if, whenever it
becomes enabled, it remains enabled until executed. A system is said to be
persistent if all its actions are persistent. This classical notion is introduced by
Karp/Miller [
In section 4, we extend the hierarchy mentioned above with an infinite hierarchy of e/l-persistent steps. A step M aM 0 is said to be e/l-k-persistent for some k ∈ N if the execution of an action a pushes the execution of any other enabled action away for at most k steps. We prove that if an action is disabled by another one, it can not be postponed indefinitely. We show that if a p/t-net is e/l-persistent, then it is e/l-k-persistent for some k ∈ N (Theorem 3) and such a k can be effectively found (Theorem 9). We also point, that the above-cited result does not hold for nets which do not have the monotonicity property (for example for inhibitor nets).
Afterwards, we investigate the set of markings in which two actions are enabled simultaneously, and also the set of reachable markings with that feature. We show that the minimum of the latter is finite and effectively determined. We also prove that if some action pushes the enabledness of another one away for more than k steps, then it also needs to happen in some minimal reachable marking enabling these two actions.
Finally, we show that e/l-k-persistency is decidable with respect to steps (Theorem 1), markings (Theorem 2) and nets (Theorem 7).
The concluding section contains some questions and plans for further investigations. 2 2.1
The set of non-negative integers is denoted by N. 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
2.2
The definitions concerning Petri nets are mostly based on [
Net is a triple N = (P, T, F ), where: – P and T are finite disjoint sets, of places and transitions, respectively; – F ⊆ P × T ∪ T × P is a relation, called the flow relation .
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 indicated by circles, and transitions by boxes.
The set of all finite strings of transitions is denoted by T ∗, 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, two strings u, v ∈ T ∗ such that (∀a ∈ T ) |u|a = |v|a are said to be Parikh equivalent.
net) is a quadruple S = (P, T, F, M0), where: Place/transition net (shortly, p/t– N = (P, T, F ) is a net, as defined above; – M0 ∈ NP is a multiset of places, named the initial marking; it is marked by tokens inside the circles, capacity of places in unlimited.
Multisets of places are named markings. In the context of p/t-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 oder 6, all defined componentwise, are well known and their formal definitions are omitted.
In this context, by •a(a•) we understand a vector of dimension |P | which has 1 in every coordinate corresponding to a place that is an entry to (an exit from, respectively) a and 0 in other coordinates.
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 0 = (M −• a) + a• (tokens are removed from entries, then put to exits). The execution of an action a in a marking M we call a (sequential) step. We shall denote M a for the predicate "a is enabled in M " and M aM 0 for the predicate "a is enabled in M and M 0 is the resulting marking".
This notions and predicates we extend, in a natural way, to strings of transitions: M εM for any marking M , and M vaM 00 (v ∈ T ∗, a ∈ T ) iff M vM 0 and M 0aM 00 .
If M wM 0, for some w ∈ T ∗, then M 0 is said to be reachable from M ; the set of all markings reachable from M is denoted by [M i . Given a p/t-net S = (P, T, F, M0), the set [M0i of markings reachable from the initial marking M0 is called the reachability set of S, and markings in [M0i are said to be reachable in S.
A transition a ∈ T is said to be live in a marking M if there is a string u ∈ T ∗ such that ua is enabled in M . A transition a ∈ T that is not live in a marking M is said to be dead in a marking M . If M aM 0 and a transition b 6= a is enabled (live) in M and not enabled (not live) in M 0, then we say that (the execution of) a disables (kills) b. Definition 3 (Inhibitor nets ). Inhibitor net is a quintuple S = (P, T, F, I, M0), where: – (P, T, F, M0) is a p/t-net, as defined above; – 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/tnets; the set of inhibitor entries to a is denoted by ◦a = {p ∈ P | (p, a) ∈ I}. A transition a ∈ T (of an inhibitor net) 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. The execution of a leads to the resulting marking M 0 = (M −• a) + a•.
The following well-known fact follows easily from Definitions 1 and 2.
possesses the following property:
Big Diamond Property: If M uM 0 & M vM 00 & u ≈ v (Parikh equivalence), then M 0 = M 00. Its special case with |u| = |v| = 2 is called the Diamond Property: If M abM 0 & M baM 00, then M 0 = M 00.
Definition 4 ( ω-extension). Let Ω = N ∪ {ω}, where ω is a new symbol (denoted infinity). We extend, in a natural way, arithmetic operations: ω + n = ω, ω − n = ω, and the order: (∀n ∈ N) n < ω. The set of k-dimensional vectors over Ω we shall denote by Ωk, and its elements we shall call ω-vectors. Operations +, − and the order ≤ in Ωk are componentwise.
For X ⊆ Ωk, we denote by Min(X) the set of all minimal (wrt ≤) members of
X, and by Max(X) the set of all maximal (wrt ≤) members of X. Let v, v0 ∈ Ωk
be ω-vectors such that v ≤ v0, then we say that v0 covers v ( v is covered by v0) .
Let us recall the well known important fact known as the Dickson’s Lemma.
Lemma 1 ([
Proof. Obvious, since in p/t-nets the tokens of M 0 −M can be regarded as frozen (disactive) tokens.
Fact 3 Inhibitor nets do not have the monotonicity property.
Proof. Let us look at the example of Fig. 1. It can be easily seen that M1 < M10 . M1a holds but M10 a doesn’t hold.
Remark: In the paper we will use the notions of reachability graph (tree) and
coverability graph (tree). We assume that the notions are known to the reader.
Their definitions can be found in any monograph or survey about Petri nets (see
[
Let us sketch the notions informally. The classical e/e-persistency means "no action can disable another one", the l/l-persistency means "no action can kill another one" and the e/l-persistency means "no action can kill another enabled one". Let us go on to formal definitions.
place/transition net.
If (∀M ∈ [M0i) (∀a, b ∈ T )
M a ∧ M b ∧ a 6= b ⇒ M ab, then S is said to be e/e-persistent; M a ∧ (∃u)M ub ∧ a 6= b ⇒ (∃v)M avb, then S is said to be l/l-persistent; M a ∧ M b ∧ a 6= b ⇒ (∃v)M avb, then S is said to be e/l-persistent. The classes of e/e-persistent (l/l-persistent, e/l-persistent) p/t-nets will be denoted by Pe/e, Pl/l and Pe/l, respectively.
It is shown in [
EE Net Persistency Problem: Is the net S e/e-persistent? LL Net Persistency Problem: Is the net S l/l-persistent? EL Net Persistency Problem: Is the net S e/l-persistent? Let S = (P, T, F, M0) be a 4
In the previous section we defined three kinds of persistency. Now, we extend the hierarchy mentioned above with an infinite hierarchy of e/l-persistent steps.
Let S = (P, T, F, M0) be a p/t-net, let M be a marking. W call a step M aM 0: – e/l-0-persistent iff it is e/e-persistent (the execution of an action a does not disable any other action); – e/l-1-persistent iff (∀b ∈ T, b 6= a) M b ⇒ [M ab ∨ (∃c ∈ T )M acb] (the execution of an action a pushes the execution of any other enabled action away for at most 1 step); – e/l-2-persistent iff (∀b ∈ T, b 6= a) M b ⇒ (∃w ∈ T ∗)[|w| ≤ 2 ∧ M awb] (the execution of an action a pushes the execution of any other enabled action away for at most 2 steps); . . . – e/l-k-persistent for some k ∈ N iff (∀b ∈ T, b 6= a) M b ⇒ (∃w ∈ T ∗)[|w| ≤ k∧ M awb] (the execution of an action a pushes the execution of any other enabled action away for at most k steps); . . . – e/l-∞-persistent iff (∀b ∈ T, b 6= a) M b ⇒ (∃w ∈ T ∗) M awb (the execution of an action a pushes the execution of any other enabled action away).
Remark: Note that e/l-∞-persistent steps are exactly e/l-persistent steps. Directly from Definition 7 we get the Fact 4 Let S = (P, T, F, M0) be a p/t-net, let M be a marking. If the step M aM 0 is e/l-k-persistent for some k ∈ N, then it is also e/l-i-persistent for every i ≥ k. Definition 8. Let S = (P, T, F, M0) be a p/t-net, M be a marking and k ∈ N. Marking M is e/l-k-persistent iff for every action a ∈ T that is enabled in M the step M a is e/l-k-persistent. P/t-net S = (N, M0) is e/l-k-persistent iff every marking reachable in S is e/l-k-persistent. We denote the class of e/l-k-persistent p/t-nets by Pe/l−k.
The direct conclusion from Fact 4 and Definition 8 is as follows: Fact 5 Let S = (P, T, F, M0) be a p/t-net, M be a marking, and k ∈ N. If the marking M is e/l-k-persistent, then it is also e/l-i-persistent for every i ≥ k. If the net S is e/l-k-persistent, then it is also e/l-i-persistent for every i ≥ k. Now we can formulate the problem:
Instance: P/t-net S, marking M , action a ∈ T enabled in M .
Question:Is the step M a e/l-k-persistent? Theorem 1. The EL-k Step Persistency Problem is decidable (for any k ∈ N). Proof. An algorithm of checking if a step M a is e/l-k-persistent (for some k ∈ N) for a given net S = (N, M0): Let us build the part of the depth of k+1 (we call it the (k+1)-component) of the reachability tree of (N, M 0), where M 0 is a marking obtained from M by execution of a. The step M a is e/l-k-persistent if for every action b ∈ T , such that a 6= b and b is enabled in M , there is a path in the (k+1)-component of the reachability tree of (N, M 0) containing an arc labeled by b.
Let us introduce another problem:
Instance:P/t-net S = (N, M0), marking M .
Question:Is the marking M e/l-k-persistent? Theorem 2. The EL-k Marking Persistency Problem is decidable (for any k ∈ N).
Proof. For every action a ∈ T that is enabled in a marking M , we check if a step M a is e/l-k-persistent (for some k ∈ N) for a given net S = (N, M0), using the algorithm of Theorem 1.
Let us recall the well-known fact, that follows from the Dickson’s Lemma 1. Fact 6 Every infinite sequence of markings contains an infinite increasing (not necessarily strictly) subsequence of markings.
Recall also that p/t-nets have the monotonicity property - Fact 2. Let us define the notion of k-enabledness.
Definition 9 (k-enabledness). Let S = (P, T, F, M0) be a p/t-net, let M be a marking. For k ∈ N we say that the action a ∈ T is k-enabled in the marking M if and only if ∃w ∈ T ∗, such that |w| ≤ k ∧ M wa.
Now, we can show: Lemma 2. Let S be a p/t-net. For an arbitrary a ∈ T there exists a natural number ka ∈ N, such that in every marking M the transition a is ka-enabled or it is dead.
Proof. Suppose that the lemma does not hold for some action a ∈ T . It means that for each k ∈ N there is a marking M such that M is not k-enabled but not dead. This means that M is k0-enabled for some k0 > k. Thus, there exists an infinite sets of markings M1, M2, . . . and integers k1 < k2 < . . ., such that the action a is live in each marking Mi and it is not ki-enabled in Mi for all i = 1, 2, . . .. Let us choose (by Fact 6) an infinite increasing sequence of markings Mi1 ≤ Mi2 ≤ . . .. Since the action a is live in Mi1, it is k-enabled in Mi1, for some k ∈ N. As the strictly increasing sequence k1 < k2 < . . . is infinite, k < kij for some j. By the monotonicity property (Fact 2), the action a is k-enabled, hence kij-enabled in the marking Mij. Contradiction.
Remark: Note that the proof of Lemma 2 is purely existential, it does not present any algorithm for finding k.
Now, we are ready to formulate the main theorem of the chapter: Theorem 3. If a p/t-net is e/l-persistent, then it is e/l-k-persistent for some k ∈ N.
In words: Whenever an action is disabled by another one, it is pushed away for not more than k-steps.
Proof. If the net is e/l-persistent, then no action kills another enabled one. From the Lemma 2 we know, that if an action a ∈ T is not dead then it is ka-enabled. Let us take K = max{ka|a ∈ T }, for the numbers ka from the Lemma 2. One can see that every action in the net that is not dead, is K-enabled. Thus, the execution of any action may postpone the execution of an action a for at most K steps. So we have the implication: if a p/t-net is e/l-persistent, then it is e/l-K-persistent, for K defined above. Example 1. Let us look at the example of Fig. 2. The only possible situation for temporary disabling an action by another one is the execution of a that disables b. And then b could be enabled again after the execution of the sequence cde, so after 3 steps. Hence, the net is e/l-3-persistent, and obviously not e/l-2persistent.
The following example shows that Theorem 3 does not hold for nets without the monotonicity property.
Example 2. Let us look at the example of Fig. 3. We can see an inhibitor net and its computation such that for every k ∈ N one can push an action away for a distance greater than k steps.
This net is life, hence it is e/l-persistent, but it is not e/l-k-persistent for any k ∈ N.
In the infinite computation acbcdaecbcddaeecbcdddaeeecb . . . the first a pushes b away for 1 step, the second - for 2 steps and every k-th a - for k steps. In the previous section, we established that an action can not postpone another action indefinitely (Theorem 3). We proved, that if a p/t-net is e/l-persistent, then it is e/l-k-persistent for some k ∈ N. We showed that such a k exists but we did not present any algorithm for finding this k.
In view of the statements above, let us consider the following problem:
Instance:P/t-net S = (N, M0), k ∈ N.
Question:Is the net S e/l-k-persistent? To solve this problem we must prove a set of auxiliary facts.
From this moment, let S = (N, M0) be an arbitrary p/t-net.
Let us define the following set of markings: Ea,b = {M ∈ N|P | | M a ∧ M b}- the set of markings enabling actions a and b simultaneously.
Let us define minEa,b ∈ N|P |, the minimum marking enabling actions a and b simultaneously: if (•a[i] = 1 ∨ •b[i] = 1) then minEa,b[i] := 1 else minEa,b[i] := 0 (for i = {1, . . . , |P |}).
Note that minEa,b = minEa,b + N|P |.
Let us formulate an auxiliary problem:
Instance:P/t-net S = (N, M0), actions a, b ∈ T .
Question:Is there a marking M such that M ∈ Ea,b and M ∈ [M0i ? (Is there a reachable marking M such that actions a and b are both enabled in M ?) Theorem 4. The Mutual Enabledness Reachability Problem is decidable. Proof. Let M = minEa,b. We build a coverability graph for the p/t-net S. We check whether in the graph exists a vertex corresponding to an ω-marking M 0 such that M 0 covers M . If so, then actions a and b are simultaneously enabled in some reachable marking of the net S. Otherwise, those transitions are never enabled at the same time.
Let Min[M0i be a set of minimal (wrt ≤) reachable markings of the net S. As members of Min[M0i are incomparable, the set Min[M0i is finite, by Lemma 1. Le us denote by REa,b the set of all reachable markings of the net S enabling actions a and b simultaneously: REa,b = {M ∈ [M0i | M a ∧ M b} = Ea,b ∩ [M0i. Let Min(REa,b) be a set of all minimal reachable markings of the net S enabling action a and b simultaneously.
Let us recall the Set Reachability Problem.
Instance:P/t-net S = (N, M0) and a set X ⊆ N|P |.
Question:Is there a marking M ∈ X, reachable in S? Theorem 5. If X ⊆ Nk is a rational convex set, then the X-Reachability Problem is decidable in the class of p/t-nets.
Proof. In [
Proposition 1. The set Min(REa,b) can be effectively constructed.
Proof. Sketch of the proof: We put into work the theory of residue sets of
Valk/Jantzen [
Now, we are ready to introduce the following problem:
Instance:P/t-net S = (N, M0), ordered pair (a, b) ∈ T × T, b 6= a, k ∈ N. Question:Is there a reachable marking M ∈ [M0i such that
M a ∧ M b ∧ ¬[(∃w ∈ T ∗)|w| ≤ k ∧ M awb]? (Does a postpone b for more than k steps?) Theorem 6. The EL-k Transition Persistency Problem is decidable. Proof. We introduce an algorithm of deciding if an action a pushes the execution of an action b away for more than k steps in some reachable marking M . 1. We check whether any markings from the set Ea,b is reachable. (a) If not, we answer NO. (b) Otherwise: i. We build the set Min(REa,b). ii. For all markings M1 ∈ Min(REa,b):
M2 := M1a.
We build a part of the depth of k+1 (the (k+1)-component) of the reachability tree of (N, M2). If the piece has an edge labeled by b, we answer NO. Otherwise we answer YES.
And now the proof of decidability of the EL-k Net Persistency Problem is ready.
Theorem 7. The EL-k Net Persistency Problem is decidable (for any k ∈ N).
Proof. S is e/l-k-persistent iff the algorithm solving EL-k Transition Persistency
Problem answers NO for all ordered pairs (a, b) ∈ T × T , a 6= b.
Finally, let us bring to mind decision another problems defined in [
Instance:P/t-net S = (N, M0), and transitions a, b ∈ T, a 6= b.
Questions (informally):
EE-Persistency Problem: Does a disable an enabled b? LL-Persistency Problem: Does a kill a live b?
EL-Persistency Problem: Does a kill an enabled b?
From [
Theorem 8. For a given p/t net S = (N, M0) and a pair of transitions a, b ∈ T one can calculate a minimum number ka,b ∈ N such that a postpones an enabled b for at most ka,b steps (if such a number exists).
Proof. We ask whether a kills an enabled b (EL-Persistency Problem). If YES then ka,b does not exist (a kills b) else: We compute a set Min(REa,b).
We build the reachability tree as long as from every M ∈ Min(REa,b) a path leads to a vertex M 0 (it can be an empty path) such M 0b. The maximum length of such paths is the desired number ka,b.
Theorem 9. If a p/t-net S = (N, M0) is e/l-persistent, then it is e/l-k-persistent for some k ∈ N and such a k can be effectively computed.
Proof. For every pair (a, b) of transitions we find ka,b defined above. The number we are looking for is k = max(ka,b : a, b ∈ T ). 5
It is shown in [
What is the computational power of nets created this way? We investigated p/t-nets because they are easy to examine (mainly due to their convenient properties such as the monotonicity property). We would like to study the hierarchy of e/l-k-persistency in more difficult extensions of p/t-nets. The authors are very grateful to the anonymous referees, for their very sound remarks and suggestions.