A transition t eventually stops a place/transition Petri net if each reachable marking of the net enables only finite occurrence sequences without occurrences of t (i.e., every infinite occurrence sequence enabled at this marking contains occurrences of t). Roughly speaking, when t is stopped then all transitions of the net stop eventually. This contribution shows how to identify stopping transitions of bounded nets using the reachability graph and of unbounded nets using the coverability graph.
We consider the following problem in this paper: Assume a place/transition Petri net and a transition t of this net. Can we eventually stop the behavior of the net by forbidding occurrences of t in occurrence sequences enabled at an arbitrary reachable marking m, or, equivalently, does no reachable marking m enable an infinite occurrence sequence without occurrences of t? If this is the case then we say that transition t eventually stops the Petri net. If t does not stop the net eventually, then some reachable marking enables an infinite occurrence sequence without occurrences of t. However, even if t does not stop the net eventually, there might be occurrence sequences (with or without occurrences of t) leading to a deadlock.
Apparently, this question is relevant for several applications of Petri nets. For example, given a robot (or any kind of machine) modeled by a Petri net, can some component modeled by a particular transition be used as an off switch? As we know from our computers, immediate stops are not always desirable, but rather forced shut down processes. A transition t stops a Petri net model eventually if it enforces a shutdown process which will eventually lead to a marking which enables no transition, except possibly transition t.
The problem tackled in this article could be solved by any standard mechanism involving temporal logics, for example the temporal logic LTL. In [5] it is shown that the model checking problem for Petri nets and LTL formulas is decidable, although according algorithms applied to unbounded Petri nets have a huge complexity. Instead, this article provides a solution which is purely based on Petri net analysis techniques. A typical advantage of these techniques is that the user gets more insight to the actual behavior of the net. Often, analysis methods tailored for Petri nets are more efficient as analysis techniques based on a translation to other languages, at least for certain classes of inputs. This might also be the case for the approach presented in this paper; a detailed study to identify such classes is, however, still missing and a topic for further research.
Throughout this paper we consider place/transition Petri nets without arc weights, capacity restrictions or inhibitor arcs. We call these place/transition Petri nets just nets. For definitions and notations, see any textbook on Petri nets, e.g. [7] or [4]. As usual, we assume that the sets of places and transitions of a net are finite. We do, however, consider unbounded nets, i.e., nets with unbounded places (a place is unbouded if, for any number b, some reachable marking assigns more than b tokens to the place). We assume the concepts of reachability graph and tree to be known, and also the concept of coverability graph for unbounded nets (this concept goes back to [6]). The coverability graph represents aspects of infinite behavior by finite means, and thus abstracts heavily from behavioral details. However, it can be used to identify unbounded places. Notice that often the coverability graph is defined as a result of a non-deterministic algorithm and is hence not unique. The algorithm constructs the finite reachability graph for bounded nets and a finite coverability graph otherwise.
Recall that a (reachability or coverability) graph is a directed graph with initial vertex and arcs labeled by transition names. Vertices of reachability graphs represent reachable markings of the considered net, whereas vertices of coverability graphs represent so-called ω-markings, which assign to each place either a non-negative integer, representing its actual token count, or the symbol ω, representing arbitrarily many tokens.
Notice that every two vertices of a (reachability or coverability) graph can be connected by two distinct arcs, labeled by two different transition names, whenever both transitions lead from the same source vertex to the same target vertex. Recall also that the source vertex and the target vertex of an arc can be identical.
A path of a graph is a finite nonempty sequence of arcs such that the target vertex of each (except the last) arc coincides with the source vertex of its subsequent arc. A path is a closed path if the target vertex of its last arc coincides with the source vertex of its first arc. A closed path is a cycle if moreover no vertex is source of more than one arc of the path, i.e., the path does not pass through any vertex more than once.
Let us finally recall some important properties of reachability and coverability graphs: – The reachability graph of a net is finite if and only if the net is bounded. – A coverability graph of a net is always finite. – Reachability and coverability graphs are deterministic, i.e., no vertex is source of two distinct arcs with the same label. – For each finite occurrence sequence of a net enabled at the initial marking, there is a unique path of the reachabilty / coverability graph starting at the initial vertex.
To warm up, we first consider the question whether a net terminates eventually, i.e., whether all its occurrence sequences are finite.
Obviously, a bounded net terminates if and only if its reachability graph has no cycles. In fact, if the reachability graph has a cycle, then each occurrence sequence from the initial marking to any marking represented by a vertex of the cycle can be extended infinitely, following the arcs of the cycle (remember that each vertex of the reachability graph represents a reachable marking). Conversely, a bounded net has only finitely many reachable markings, because the set of places of the net is finite. If the net does not terminate, it has an infinite occurrence sequence and therefore finite occurrence sequences of arbitrary length. Since each finite occurrence sequence corresponds to a directed path of the reachability graph, each occurrence sequence of sufficient length (choose the number of reachable markings) corresponds to a directed path that passes through at least one vertex more than once; thus the reachability graph has a closed path, and therefore it has a cycle.
Unbounded nets do not terminate anyway. To see this, consider the construction of the reachability tree. Since the set of transitions is finite, each vertex of this tree has finitely many immediate successors. By K¨onig’s Lemma, the tree has an infinite path, corresponding to an infinite occurrence sequence.
Hence, an obvious algorithm to check termination of a net first checks boundedness, for example by the coverability graph construction. In case the considered net is bounded, the algorithm constructs the reachabilty graph and checks whether this graph has a cycle. Actually, this two-step approach is not necessary, because the coverability graph of a bounded net equals its reachability graph, and cyclicity of this graph is implicitly checked during the coverability graph construction. A perhaps more elegant algorithm1 first adds a place to the net which has all transitions of the net in its pre-set and no transition in its post-set, and then checks boundedness of this place, again by construction of the coverability graph. Obviously, this additional place is bounded if and only if the length of all occurrence sequences is bounded. Since the set of transitions is finite, this is the case if and only if there is no infinite occurrence sequence. 3
We now come back to the question asked initially: Does a transition t of a net stop the net eventually? This is the converse of the question: Is there an infinite occurrence sequence, enabled at some reachable marking, without occurrences of t? An even simpler formulation of the same property is: Is there an initially enabled infinite occurrence sequence with only finitely many occurrences of t? In fact, an infinite occurrence sequence enabled at a reachable marking m is suffix 1 communicated by Karsten Wolf of an infinite sequence enabled initially, and the finite prefix up to m can contain only finitely many occurrences of t. Conversely, assume an infinite occurrence sequence containing only finitely many occurrences of t. Then the minimal prefix containing all these t-occurrences leads to a reachable marking which enables the according infinite suffix without occurrences of t.
For bounded nets, there is thus a very simple algorithmic solution to the problem whether a transition t eventually stops its net, based on the following proposition.
Proposition 1. A transition t of a bounded net eventually stops the net if and only if the reachability graph of the net has no cycle without an arc labeled by t. Proof. Assume that the reachability graph has a cycle without a t-labeled arc. Then some initially enabled infinite occurrence sequence starts with a finite sequence leading to some marking represented by a vertex of this cycle (which might include occurrences of t) and then runs along the cycle infinitely. Hence this infinite occurrence sequence has only finitely many occurrences of t.
Conversely, assume that each cycle of the reachability graph has at least one t-labeled arc. Let m be an arbitrary reachable marking. Each sufficiently long occurrence sequence enabled at m passes through some marking at least twice, because the net is bounded. Hence the according path of the reachability graph passes through some vertex at least twice. The subsequence starting and ending with that vertex corresponds to a closed path. Each closed path contains all arcs of at least one cycle, and thus by assumption also an arc labeled by t. Therefore, the subsequence contains an occurrence of t, and so does the infinite occurrence sequence. tu
So a very simple algorithm constructs the reachability graph and checks whether every cycle of this graph contains at least one arc labeled by t. A more elegant solution is to first delete all t-labeled arcs of the reachability graph (which does not necessarily lead to a connected graph) and then check for cycles. 4
Now we consider the case that the considered net is unbounded. Does it eventually terminate, provided a given transition t occurs only finitely often? For unbounded nets, the reachability graph is infinite, but the coverability graph is finite. However, unfortunately the coverability graph does not bring immediate help. Consider the simple example of a net with only one initially unmarked place, a single input transition i, and a single output transition o, as shown in Figure 1.
In this example, transition i eventually stops the net, whereas transition o does not. However, both transitions occur in the coverability graph in quite the same way, namely as labels of arcs leading from and to the vertex labeled by [ω]. These are the only cycles of this coverability graph. While the coverability graph does thus not lead to an algorithmic solution, we can solve the problem considering additional information, as shown below.
Remember that, during the (nondeterministic) construction of the coverability graph, we compare new ω-markings with already constructed ω-markings. When a new vertex of the coverability graph is constructed, the algorithm compares the ω-marking m corresponding to this new vertex with the ω-markings m0 corresponding to vertices which are on paths from the initial vertex (representing the initial marking) to the new one, according to the graph constructed so far. If, for all places, the new ω-marking m is identical to m0, then the new vertex is identified with the vertex corresponding to m0. Otherwise, if m(s) ≥ m0(s) for each place s (where ω > n for every integer n), then m is modified as follows: For each place s with m(s) > m0(s), we set m(s) := ω, because the sequence from the vertex corresponding to m0 to the newly constructed vertex can be repeated arbitrarily often, leading to an unbounded token growth on the place s. For all other places s, m(s) remains unchanged.
In the example of Figure 1, the marking reached by the occurrence of transition i is greater than the initial marking for the only place of the net. Hence, this place receives an ω-entry for the corresponding ω-marking [ω], represented by the vertex [ω] of the coverability graph. Further occurrences of transition i are possible, leading to the same ω-marking, because ω already means “arbitrarily many”. Observe that transition i of the net can occur infinitely often, no matter if transition o occurs, whereas o cannot occur arbitrarily often without i, and in particular there is no infinite occurrence sequence o o o . . . enabled at any marking, a fact which is not reflected by the coverability graph.
In general, we are looking for infinite occurrence sequences, enabled by some reachable marking, without occurrences of t. Since occurrence sequences correspond to paths of the coverability graph and sufficiently long occurrence sequences have to pass through some vertex more than once, we have a closer look to closed paths of coverability graphs in the sequel.
Since ω-entries are only added during the construction of the coverability graph, and are never removed, all ω-markings appearing as vertices in a closed path of the coverability graph agree on the set of ω-marked places, whereas the non-negative integers assigned to the other places still represent the token game. Therefore, cycles and closed paths of coverability graphs do not necessarily correspond to cyclic behavior, because according occurrence sequences might increase or decrease the token count of places which have ω-entries in ω-markings of the path. If the token count of each place is not decreased, then the path can be repeated arbitrarily, leading to an infinite occurrence sequence. Otherwise, it can not.
Consider a path π of the coverability graph of a net and let σπ be the sequence of labels of arcs of π. We call the path π non-decreasing, if, for each place s, the number of occurrences of transitions in the pre-set of s in σπ is not smaller than the number of occurrences of transitions in the post-set of s in σπ, i.e., if at least as many tokens are added as are removed, and hence the effect of σπ is non-negative for each place. Otherwise, the effect of transition occurrences in σπ is negative for some place, and then we call π decreasing.
Proposition 2. Given an unbounded net N and a coverability graph of N , a transition t stops N eventually if and only if there is no non-decreasing closed path of the coverability graph without an arc labeled by t.
Proof. Assume that the coverability graph has a non-decreasing closed path π without an arc labeled by t. Let mπ be the ω-marking corresponding to the source vertex of the first arc of π. It is well-known that all ω-marked places of mπ are simultaneously unbounded, i.e., for each number b there is a reachable marking mb of N satisfying mb(s) ≥ b if mπ(s) = ω and mb(s) = mπ(s) if mπ(s) 6= ω. Now, choosing b as the length of π, the sequence of labels of π is an occurrence sequence σπ enabled at mb. This follows from the construction rule of the coverability graph, which considers places not marked by ω as in the reachability graph construction. Places marked by ω carry sufficiently many tokens to allow the occurrences of all transitions in the sequence σπ. Since π is assumed to be non-decreasing, the marking m0 reached by σπ satisfies m0(s) ≥ mb(s) for each place s. Therefore, σπ can be repeated arbitrarily. Thus, there is an infinite sequence without occurrences of t, enabled at the reachable marking mb.
For the converse direction, consider an infinite occurrence sequence σ enabled at the initial marking of N with only finitely many occurrences of transition t. Let σ = σ1 σ2 such that σ2 contains no occurrences of t and σ1 is minimal with this property (i.e., σ1 is empty or ends with t). Let σ2 = t1 t2 t3 . . . and let, for i ≥ 0, mi be the marking reached by the sequence σ1 t1 . . . ti. By repeated application of Dickson’s Lemma, we find indices k1, k2, k3, . . . such that, for j > i, mkj (s) ≥ mki (s) for each place s. By the construction of the coverability graph, for each finite occurrence sequence enabled at the inital marking, there is unique path from the initial vertex such that the sequence of labels of its arcs equals the occurrence sequence. Since the coverability graph is finite, the vertices reached by the paths corresponding to the sequences σ1 t1 . . . tki (i > 0) cannot be pairwise different, whence some vertex is visited at least twice. Assume this is the case for the sequences σ1 t1 . . . tkn and σ1 t1 . . . tkm , where n < m. Then the subsequence tkn+1 . . . tkm corresponds to a closed path of the coverability graph, which does not contain an arc labeled by t. By construction, this path is non-decreasing. tu
Throughout this section, let N be an unbounded net and let t be a transition of
N . We refer to the characterization given in Proposition 2 and collect properties
of a non-decreasing closed path π without an arc labeled by t of a coverability
graph of N .
(
(
If a place is marked by ω in an ω-marking, then this place is also marked
by ω in a subsequent marking in the coverability graph, by the construction
rule of coverability graphs. The claim follows because π is a closed path.
(
For places s of N which are not marked by ω, the number of occurrences of
transitions in arcs of π that belong to the pre-set of s equals the number of
occurrences of transitions in arcs of π that belong to the post-set of s by the
construction rule of coverability graphs. For places marked by ω, the claim
follows because π is non-decreasing by assumption.
(
Proposition 3. If t does not stop the net N eventually, then conditions (
All the above conditions (
Proposition 4. Assume a coverability graph of N with arcs {a1, . . . , ak}, and a
mapping f : {a1, . . . , ak} → {0, 1, 2, . . .} (a multiset of arcs) satisfying f (ai) > 0
for at least one arc and moreover the following conditions:
(
Then there is a non-decreasing closed path π without arcs labaled by t. Proof. We show that there exists such a path π such that, for each arc ai, this arc occurs f (ai) times in π.
First, we construct the following sub-graph of the considered coverabiliy
graph: We delete all arcs ai of the coverablitiy graph satisfying f (ai) = 0, and
then delete all isolated vertices. Since at least one arc ai satisfies f (ai) > 0, this
subgraph has at least one arc and hence at least one vertex. By condition (
It is a well-known theorem that a directed multigraph has an Euler Circuit
(which is a closed path in our terminology), if it is connected and every vertex
has the same in- and out-degree. If the multiplicity of arcs of the subgraph is
given by the mapping f , we obtain a directed multigraph. Then the in-degree of
a vertex v of the subgraph is the sum of all f (ai) for arcs ai with target vertex
v, and its out-degree is the sum of all f (ai) for arcs ai with source vertex v. So,
by condition (
All conditions of the previous proposition except the first can be expressed in terms of inequalities. Let again a1, . . . , ak denote the arcs of a coverability graph of N . Given a path π of this coverability graph, the variables x1, . . . , xk indicate how often a particular arc appears in the path π. Using this notation, we rewrite the above conditions (the additional condition (6’) just states that all xi are non-negative): (2’) For a vertex v of the coverability graph, let in(v) be the set of arcs with target v and let out(v) be the set of arcs with source v.
For each vertex v,
X xi =
X
xi . ai∈in(v)
ai∈out(v) (3’) For each arc ai connecting two vertices representing ω-markings with different sets of ω-marked places, we have xi = 0. (4’) For each place s with pre-set •s and post-set s• satisfying m(s) = ω in the ω-markings appearing in π, we have
X
X u∈•s λ(ai)=u xi ≥
X
X u∈s• λ(ai)=u xi , where λ(a) denotes the label of arc a, i.e., the occurring transition. (5’) For each arc ai labeled by t, we have xi = 0. (6’) For i = 1, . . . , k, we have xi ≥ 0 .
It remains to find a solution x1, . . . , xk of the according homogeneous system
of linear inequalities such that not all xi are zero, which additionally satisfies
condition (
Fortunately, all solutions of the inequality system can be represented as linear combinations (with non-negative coefficients) of a finite basis. See e.g. [1] for an algorithm to compute such a basis. Let B = {b1, b2, . . . , bl} be a basis, with bi = [bi,1, bi,2, . . . , bi,k] for 1 ≤ i ≤ l. Then each solution to the system of inequalities can be represented as
μ1 · b1 + μ2 · b2 + · · · μl · bl , where all μi are non-negative integers.
The following simple proposition shows that we do not have to consider all these (infinitely many) solutions, but may restrict on solutions where all coefficients belong to the set {0, 1}.
Proposition 5. Let μ1 ·b1 +· · ·+μl ·bl be a solution of the system of inequalities (2’) to (6’). Define, for 1 ≤ i ≤ l, μ0i by μ0i := 0 if μi = 0, and μ0i := 1 if μi > 0.
Then μ01 · +b1 + μ02 · b2 + · · · μ0l · bl is a solution of the system of inequalities (2’) to (6’), too, and the subgraphs generated by both solutions conincide. In particular, the subgraph generated by the first solution is strongly connected if and only if the subgraph generated by the second solution is strongly connected. tu
Combining Propositions 2,3,4 and 5 yields the main result of this contribution: Theorem 1. Transition t does not stop the net N eventually if and only if, for any coverability graph of N and for any basis B of the solutions of the system of inequalities (2’) to (6’), the sum of all solutions of a nonempty subset of B generates a connected subgraph of the coverability graph. tu
An algorithm can directly be derived from this theorem. The worst case complexity of this algorithm is apparently quite poor, because it requires the construction of the coverability graph, the construction of a basis of the derived system of inequalities, and finally it requires to consider all (exponentially many) subsets of these basis solutions. 6
Instead of considering all subsets of basis solutions to find a set of solutions generating a strongly connected subgraph of the coverability graph, such a set can be found by means of the following efficient divide-and-conquer algorithm:
We define an algorithmic function which, given a set S of solutions of the system of inequalities, first constructs the generated subgraph of the coverability graph, i.e., this graph has all arcs ai of the coverability graph which have positive coefficients in any solution of S. If this subgraph is strongly connected, we are finished and conclude that the considered transition t eventually stops the net. Otherwise this subgraph has more than one strongly connected component. For each strongly connected component, we consider the subset of solutions S0 ⊂ S with the property that all its positive coefficients refer to arcs of this component. If this set S0 is not empty for a strongly connected component, it again generates a subgraph of the coverability graph. This subgraph is entirely located within the considered strongly connected component, but it is not necessarily strongly connected itself. We recursively apply this function, for each strongly connected component with nonempty according set S0, to this set S0. If the set S0 is empty for all strongly connected components, the algorithm returns to its calling instance. If the algorithm terminates without finding a strongly connected subgraph generated by a set of solutions, it concludes that no such set exists and that therefore transition t eventually stops the net.
Initially, the function is applied to a basis B of solutions to the system of inequalities.
Proposition 6. The algorithm terminates and outputs the correct answer. It runs in linear time with respect to the size of the basis B.
Proof. The algorithm terminates because the function is only called recursively for a set S0 if the current set S does not generate a strongly connected graph and S0 generates a smaller strongly connected subgraph.
The algorithm only stops before proper termination if it found a stronly connected subgraph generated by a solution, and hence the output that transition t eventually stops the net is correct.
It remains to show that, if the algorithm reaches its proper end and hence did not find a set generating a strongly connected subgraph, then no such set exists. So assume a set S ⊆ B of solutions exists such that the generated subgraph is strongly connected. Now assume that S ⊂ S0. Then, obviously the subgraph generated by S is still in one strongly connected component of the subgraph generated by S0. Therefore, whenever the function is called for some set S0 satisfying S ⊂ S0, and from this instance it is called for subsets S1, S2, . . ., then the set S is included in one of the sets Si. Since S is included in B, it will eventually be found by the algorithm (unless another suitable set of solutions is found before).
Finally, the algorithm runs in linear time with respect to the size of the basis B because each function call performs a proper split of the set B, and B can be splitted at most |B| − 1 times. tu 7
We have shown how to decide if a single transition is able to stop an entire net eventually, i.e., if no infinite occurrence sequences has only finitely many occurrences of t. The approach can easily be generalized to sets of transitions (if we stop all transitions of this set at some marking, will the net eventually terminate?). Another generalization refers to arc weights; the procedure works for nets with arc weights with only small changes. The usual complement place construction makes the approach also available for nets with capacity restrictions.
Experimental results and comparisons to other approaches, in particular to model checking algorithms for temporal logics, will be topics of further research.
Another tool for identifying transitions that stop a net is given by transition invariants, which are closely related to cyclic occurrence sequences, and by transition sur-invariants, which are related to occurrence sequence with non-negative effect to all places. Both types of invariants can be derived by linear algebraic means, see e.g. [2]. These techniques lead to much more efficient algorithms, but unfortunately provide only sufficient criteria for termination problems.
Yet another approach to solve the problem is to consider cycles in coverability graphs (see [3]), representing cyclic behavior. The calculation of such cycles requires, however, by far more effort than the algorithms suggested in the present contribution.