The notion of persistency is one of the most frequently discussed issues in the Petri net theory - [4,7,8,11,12] and many others. It is being studied not only in terms of theoretical properties, and also as a useful tool for designing and analyzing software environments [3]. In software engineering, persistency is a desirable property and many systems may not work properly without it.
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 [10]. Also interesting, with practical applications, is the notion of weak persistency introduced and investigated in [16,15,9]. In section 3, we bring to mind two generalizations of the classical notion (defined in [2]): l/l persistency and e/l-persistency. An action is said to be l/l-persistent if it remains live until executed, and is e/l-persistent if, whenever it is enabled, it cannot be killed by another action. For uniformity, we name the traditional persistency notion e/epersistency. Next, we recall that those kinds of persistency are decidable in the class place/transition nets.
In section 4, we extend the hierarchy mentioned above with an infinite hierarchy of e/l-persistent steps. A step M aM 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.
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 2 X , the cardinality of the powerset is 2 |X| . Multisets over X are members of N X , i.e. functions from X into N.
The definitions concerning Petri nets are mostly based on [5].
Net is a triple N = (P, T, F ), where:
-P and T are finite disjoint sets, of places and transitions, respectively;
For all a ∈ T we denote:
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.
Definition 2 (Place/Transition Nets). Place/transition net (shortly, p/tnet) is a quadruple S = (P, T, F, M 0 ), where:
-N = (P, T, F ) is a net, as defined above; -M 0 ∈ N P 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 , 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 = (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 for the predicate "a is enabled in M and M 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 (v ∈ T * , a ∈ T ) iff M vM and M aM .
If M wM , 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 p/t-net S = (P, T, F, M 0 ), the set [M 0 of markings reachable from the initial marking M 0 is called the reachability set of S, and markings in [M 0 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 and a transition b = a is enabled (live) in M and not enabled (not live) in M , then we say that (the execution of) a disables (kills) b.
Inhibitor net is a quintuple S = (P, T, F, I, M 0 ), where:
-(P, T, F, M 0 ) 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 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
The following well-known fact follows easily from Definitions 1 and 2.
Fact 1 (Diamond and big diamond properties) Any place/transition net possesses the following property: Big Diamond Property:
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, v ∈ Ω k be ω-vectors such that v ≤ v , then we say that v covers v ( v is covered by v ) .
Let us recall the well known important fact known as the Dickson's Lemma.
). Any subset of incomparable elements of Ω k is finite. Definition 5. We say that a Petri net S = (P, T, F, M 0 ) has the monotonicity property if and only if
Fact 2 P/t-nets have the monotonicity property.
Proof. Obvious, since in p/t-nets the tokens of M −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 M 1 < M 1 . M 1 a holds but M 1 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 [5,13] or arbitrary else). The notion of persistency is one of the classical notions in concurrency theory. The notion is recalled in [2] (named in the sequel e/e-persistency). Some of its generalizations: l/l-persistency and e/l-persistency are also introduced there.
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. Definition 6 (Three kinds of persistency). Let S = (P, T, F, M 0 ) be a place/transition net.
The classes of e/e-persistent (l/l-persistent, e/l-persistent) p/t-nets will be denoted by P e/e , P l/l and P e/l , respectively.
It is shown in [2] that the following decision problems are decidable:
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?
4 Hierarchy of e/l-persistency
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.
Definition 7 (E/l-persistent steps -an infinite hierarchy).
Let S = (P, T, F, M 0 ) be a p/t-net, let M be a marking. W call a step M aM :
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 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, M 0 ) be a p/t-net, let M be a marking. If the step M aM 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, M 0 ) 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, M 0 ) 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 P e/l−k .
The direct conclusion from Fact 4 and Definition 8 is as follows:
Fact 5 Let S = (P, T, F, M 0 ) 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.
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, M 0 ): 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 ), where M 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 = b and b is enabled in M , there is a path in the (k+1)-component of the reachability tree of (N, M ) containing an arc labeled by b.
Let us introduce another problem:
Instance:P/t-net S = (N, M 0 ), 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, M 0 ), 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, M 0 ) 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.
Lemma 2. Let S be a p/t-net. For an arbitrary a ∈ T there exists a natural number k a ∈ N, such that in every marking M the transition a is k a -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 k -enabled for some k > k. Thus, there exists an infinite sets of markings M 1 , M 2 , . . . and integers k 1 < k 2 < . . ., such that the action a is live in each marking M i and it is not k i -enabled in M i for all i = 1, 2, . . .. Let us choose (by Fact 6) an infinite increasing sequence of markings
As the strictly increasing sequence k 1 < k 2 < . . . is infinite, k < k ij for some j. By the monotonicity property (Fact 2), the action a is k-enabled, hence k ij -enabled in the marking M ij . 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 k a -enabled. Let us take K = max{k a |a ∈ T }, for the numbers k a 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. Fig. 2. A p/t-net that is e/l-3 persistent but not e/l-2 persistent 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, M 0 ), 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, M 0 ) be an arbitrary p/t-net.
Let us define the following set of markings: Proof. Let M = minE a,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 such that M 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[M 0 be a set of minimal (wrt ≤) reachable markings of the net S. As members of Min[M 0 are incomparable, the set Min[M 0 is finite, by Lemma 1.
Le us denote by RE a,b the set of all reachable markings of the net S enabling actions a and b simultaneously:
Let Min(RE a,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, M 0 ) and a set X ⊆ N |P | . Question:Is there a marking M ∈ X, reachable in S?
Theorem 5. If X ⊆ N k is a rational convex set, then the X-Reachability Problem is decidable in the class of p/t-nets.
Proof. In [2]. 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 E a,b is reachable. (a) If not, we answer NO. (b) Otherwise: i. We build the set Min(RE a,b ).
ii. For all markings M 1 ∈ Min(RE a,b ):
We build a part of the depth of k+1 (the (k+1)-component) of the reachability tree of (N, M 2 ). 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. From [2] we know that the problems are decidable.
It is shown in [1] that if we change the firing rule in the following way: only e/e-persistent computations are permitted, then we get a new class of nets (we call them nonviolence nets) which are computationally equivalent to Turing machines. We plan to investigate net classes, with firing rules changed (only e/l-kpersistent computations are allowed) and answer the question:
Question 1: 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.
The study is cofounded by the European Union from resources of the European Social Fund.Project PO KL "Information technologies: Research and their interdisciplinary applications", Agreement UDA-POKL.