Controlling Petri Net Behavior Using Time Constraints Irina A. Lomazova1⋆ and Louchka Popova-Zeugmann2 1 National Research University Higher School of Economics (HSE), Moscow, 101000, Russia ilomazova@hse.ru 2 Department of Computer Science, Humboldt University Berlin, Germany popova@informatik.hu-berlin.de Abstract. In this paper we study how it is possible to control Petri net behav- ior using time constrains. Controlling here means forcing a process to behave in a stable way by associating time intervals to transitions and hence transforming a classic Petri net into a Time Petri net. For Petri net models stability is often ensured by liveness and boundedness. These properties are crucial in many ap- plication areas, e.g. workflow modeling, embedded systems design, and bioin- formatics. This paper deals with the problem of transforming a given live, but unbounded Petri net into a live and bounded one by adding time constraints. We specify necessary conditions for the solvability of this problem and present an al- gorithm for adding time intervals to net transitions in such a way that the resulting net becomes bounded while staying live. 1 Introduction Distributed systems range in almost all areas: from technical systems to biological sys- tems or to systems of business processes. Although such systems are very different in their subject matter they all have common properties, such as reiteration of all sub- processes or returning to some initialization in the system, or containing finitely or infinitely many different states etc. Petri nets are widely used for modeling and analysis of distributed systems. The first two properties concern the liveness of the model, the second two are the subject of boundedness studies. In most of the practical systems the infiniteness of all reachable states is an undesired property. A typical example is a business process model, represented by a workflow net — a special kind of a Petri net. The essential property for workflow nets is soundness, also called proper termination [1]. Soundness is intensively studied in the literature [1, 2, 7, 11, 13, 16]. Checking soundness of workflow nets can be reduced to checking liveness and boundedness for the extended net obtained by connecting the source place with the sink place through a new transition in the initial workflow net. Thus ensuring live- ness and boundedness of a model can be applied for asserting soundness of workflow nets. In biological systems liveness and boundedness ensure system stability [8, 9]. In embedded systems scheduling is often necessary due to the resource limitations [10]. In practice it may often happen that a given live Petri net is not bounded. Then it would be helpful to "repair" the model by adding priorities or time to transitions so, that ⋆ This study was supported by the National Research University Higher School of Economics’ Academic Fund. 20 the net becomes bounded staying live. In other words, the question is whether we can "repair" the model with the help of priority or time constrains. In [5] J. Desel proposed an approach for a brute-force-scheduling to ensure bounded behavior, employing tran- sitions of a given subset infinitely often. Here we study when and how time constraints can ensure boundedness of a given live Petri net, retaining its liveness. In contrast to brute-force approach, time constraints allow local and more flexible control — not just forcing one ’good’ execution. In [12] we have considered a way to add priorities in order to transform a live and unbounded model, represented by a Petri nets, into a live and bounded one. For this reason we have defined a sub-tree of the reachability tree, the so-called "spine tree". The spine tree contains all minimal cyclic runs together with prefixes leading to the cycles. In this paper we use the spine-based coverability tree, derived from the spine tree, in order to add time intervals to the transitions in such a way that the resulting Time Petri net is live and bounded. Of course, this is not always possible. Priority scheduling is an appropriate solution for workflow systems. For biological systems it is not so good, since there is no mechanism to assign priorities to events in biological systems. Scheduling biological systems with the help of time constraints would provide a much more natural solution [18]. In this work we show how to associate time constrains to a given live and unbounded Petri net in such a way that the resulting time-dependent net is live and bounded. Thereby we want to fully preserve the structure of the given net. For that we use the spine tree and the spine-coverability tree, introduced in [12] and compute a parametri- cal state space for a Time Petri net, for which the underlying timeless Petri net is the given one. The paper is organized as follows. In Section 2 we first give a more detailed moti- vation for this work and then recall some basic definitions in the theory of Petri nets. Section 3 presents the main contributions of the paper: a sufficient condition for trans- forming a live and unbounded Petri net into a live and bounded one by adding time intervals and an algorithm for computing these intervals, as well as, an example illus- trating the algorithm. Section 5 contains some conclusions. 2 Preliminaries 2.1 Motivation Liveness in bounded Petri nets is considered in numerous works. In [19] Ridder and Lautenbach considered the relationship between liveness in bounded nets and T- invariants. For marked graph Petri nets characterization of liveness and boundedness in terms of reachability graphs was done in [3]. Scedulability analysis of Petri nets, aimed at ensuring infinitely repeated firing sequences within a bounded stated space, was studied in [10]. In [9] and [8] M. Heiner considered the problem of transforming live and unbounded Petri nets into live and bounded nets by adding time durations to transitions. It is shown in these works, that when a Petri net is covered by T-invariants (i.e. each transition enters into at least one T-invariant with a non-zero component), T-invariants can be used for 21 computing time durations for transitions, making the net bounded. In other words, this method allows to transform a live and unbounded Petri net, covered by T-invariants, into a live and bounded Timed Petri net [18] with the same structure. Unfortunately this method does not always work, as it was shown in [9]. Furthermore, as it is shown in [12], a possibility to transform a live and unbounded net into a bounded one can depend not only on T-invariants, but on initial markings as well. So, the algorithm for making a live Petri net also unbounded with the help of transition priorities, which we presented in [12], essentially takes into account initial states. This is the case also for the algorithm assigning time intervals to the transitions and represented in this article. Live and unbounded Petri nets were considered also in [6]. The notion of weak boundedness was introduced there. A Petri net N is called weakly bounded, iff it is unbounded, but for every reachable marking m in N a bounded run is enabled in m, i.e. from every reachable marking we can find a way to continue the execution in such a way, that the number of tokens in each place will be not greater that some fixed value. The distinction between bounded, weakly bounded and not weakly bounded Petri nets is very important for applications. However, till now, there is no algorithm for distinguishing weakly bounded and not weakly bounded Petri nets. There is a reason to believe that these notions are connected with a possibility to transform an unbounded Petri net into a bounded one by adding some time, or priority constraints. 2.2 Basics Let N denote the set of natural numbers (including zero) and let Q+ 0 be the set of all non-negative rational numbers including zero. All notions and notations used here are generally known and can be found in [4]. Let P and T be disjoint sets of places and transitions with P ∪ T 6= ∅ and let F ⊆ (P × T ) ∪ (T × P ) → N be a flow relation. Then N = (P, T, F ) is a (unmarked) Petri net. A marking in a Petri net is a function m : P → N, mapping each place to some natural number (possibly zero). A (marked) Petri net (N , m0 ) is an unmarked Petri net N with its initial marking m0 . Further we call marked Petri nets just Petri nets and use vector notation for marking by fixing some ordering of places in a Petri net. Pictorially, P -elements are represented by circles, T -elements by boxes, and the flow relation F by directed arcs. Places may carry tokens represented by filled circles. A current marking m is designated by putting m(p) tokens into each place p ∈ P . For a transition t ∈ T an arc (x, t) is called an input arc, and an arc (t, x) – an output arc. A transition t ∈ T is enabled in a marking m iff ∀p ∈ P m(p) ≥ F (p, t). An enabled transition t may fire yielding a new marking m′ , such that m′ (p) = m(p) − t F (p, t) + F (t, p) for each p ∈ P (denoted m → m′ , or just m → m′ ). Then we say that a marking m′ is directly reachable from a marking m. A marking m is called dead iff it enables no transition. 1t 2 t A run in N is a finite or infinite sequence of firings m1 → m2 → . . . . An initial run in (N , m0 ) is a run, starting from the initial marking m0 . A cyclic run is a finite 22 run starting and ending at the same marking. A maximal run is either infinite, or ends with a dead marking. We say that a marking m is reachable from a marking m′ in N iff there is a run ′ m = m1 → m2 → · · · → mn = m; m is reachable in (N , m0 ) iff m is reachable from the initial marking. By R(N , m) we denote the set of all markings reachable in N from the marking m. A run σ in (N , m) is called feasible iff σ starts from a reachable marking. A T-invariant in a Petri net with n transition t1 , . . . , tn is an n-dimensional vector α = (α1 , · · · , αn ) with αi ∈ N at such that after firing of every transition sequence containing exactly αi occurrences of each transition ti in an arbitrary marking m (if possible) leads to the same marking m. A reachability graph of a Petri net (N , m0 ) presents detailed information about the net behavior. It is a labeled directed graph, where vertices are reachable markings in (N , m0 ), and an arc labeled by a transition t leads from a vertex v, corresponding to a t marking m, to a vertex v ′ , corresponding to a marking m′ iff m → m′ in N . A reachability graph may be also represented in the form of a reachability tree, which can be defined in a constructive form. We start from the initial marking as a root. If for a current leaf v labeled with a marking m, there is already a node v ′ 6= v lying on the path from the root to v and labeled with the same marking m, we notify v to be a leaf in the reachability tree. If not, nodes directly reachable from m and the corresponding arcs are added. Note, that in a reachability tree run cycles are represented by finite paths from nodes to leafs. A place p in a Petri net is called bounded iff for every reachable marking the number of tokens residing in p does not exceed some fixed bound κ ∈ N. A marked Petri net is bounded iff all its places are bounded. It is easy to see, that a Petri net (N , m0 ) is bounded iff its reachability set R(N , m0 ), and hence its reachability graph, are finite. A marking m′ covers a marking m (denoted m′ ≥ m) iff for each place p ∈ P , m′ (p) ≥ m(p). The relation ≥ is a partial ordering on markings in N . By the firing rule for Petri net, if a sequence of transitions is enabled in a marking m, and m′ ≥ m, then this sequence of transitions is also enabled also in m′ . A marking m′ strictly covers a marking m (denoted m′ > m) iff m′ ≥ m and m 6= m. redundantly For an unbounded Petri net, a coverability tree gives a partial information about the net behavior. It uses the notion of a generalized marking, where the special symbol ω designates an arbitrary number of tokens in a place. Formally, a generalized marking is a mapping m : P → N ∪ {ω}. A coverability tree is defined constructively. It is started from the initial marking and is successively constructed as a reachability tree. The difference is that when a marking m′ of a current leaf v ′ in a reachability tree strictly covers a marking m of a node v, lying on the path from the root to v ′ , then in a coverability tree the node v ′ obtains a marking mω , where mω (p) = ω, if m′ (p) > m(p), and mω (p) = m′ (p), if m′ (p) = m(p). For generalized markings enabling of a transition and a firing rule is defined as for usual markings except that ω-marked places are ignored. Each place p, which was marked by ω, remains ω-marked for all possible run continuations. 23 Let N = (P, T, F ) be an unmarked Petri net and let I : T −→ Q+ + 0 × (Q0 ∪ {∞}) be a function such that for each t ∈ T holds: I(t) = (at , bt ) and at ≤ bt . Thus, the function I associates an interval [at , bt ] with each transition t in T . We notate at with eft(t) (earliest firing time for t) and bt with lft(t) (latest firing time for t). Here at and bt are relative to the time, when t was enabled last. When t becomes enabled, it can not fire before at time units have elapsed, and it has to fire not later than bt time units, unless t got disabled in between by the firing of another transition. The firing itself of a transition takes no time. The time interval is designed by real numbers, but the interval bounds are nonnegative rational numbers. It is easy to see (cf. [18]) that w.l.o.g. the interval bounds can be considered as integers only. Thus, the interval bounds at and bt of any transition t are natural numbers, including zero and at ≤ bt or bt = ∞. A comprehensive introduction can be found in [18]. Z = (N , m0 , I) is called Time Petri net (TPN) and it was first introduced by Merlin [14]. The marked Petri net (N , m0 ) := S(Z) is called the skeleton and I - the interval function of Z. p1 2 t1 [1,5] t2 [0,3] t3 [2,4] t4 [2,3] p2 p3 Fig. 1. The Time Petri net Z Every possible situation in a given TPN can be described completely by a state z = (m, h), consisting of a (place) marking m and a transition marking h. The (place) marking, which is a place vector (i.e. the vector has as many components as places in the considered TPN), is defined as the marking notion in classic Petri nets. The time marking, which is a transition vector (i.e. the vector has as many components as transitions in the considered TPN), describes the time circumstances in the considered situation. In general, each TPN has infinite number of states. The state space of a TPN can be characterized parametrically and it is shown that knowledge of the integer-states, i.e. states whose time markings are (nonnegative) inte- gers, is sufficient to determine the entire behavior of the net at any point in time (cf. [17] and [18]. Thus, a reachability graph for a TPN can be defined so that the nodes of the graph are the reachable integer-states and a directed edge connects two nodes, from z1 to z2 if there is possible to change from z1 to z2 , considered as states in the TPN. And finally, a reachability tree can be then also defined for TPN considering the reachable p-markings. 24 In this paper we use the parametric states in order to restrict the behavior of a live and unbounded PN to a live and bounded one. The notions parametric state and parametric run can be easily defined by recursion. Let Z = (P, T, F, V, m0 , I) be a Time Petri net and let σ = t1 · · · tn be a firing sequence in Z. Then, the parametric run (σ(x), Bσ ) of σ in Z with σ(x) = x0 t1 x1 · · · xn−1 tn xn and the parametric state (zσ , Bσ ) in Z are recursively defined as follows: Basis: σ = ε, i.e., σ(x) = x0 . Then zσ = (mσ , hσ ) and Bσ are defined as follows: 1. mσ := mo ,  x0 if t− ≤ mσ 2. hσ (t) := , ♯ otherwise 3. Bσ := { 0 ≤ hσ (t) ≤ lft(t) | t ∈ T ∧ t− ≤ mσ } Step: Assume that zσ and Bσ are already defined for the sequence σ = t1 · · · tn . For σ = t1 · · · tn tn+1 = wtn+1 we set | {z } :=w 1. mσ := mw + ∆tn+1 ,    ♯ if t− 6≤ mσ hw (t) + xn+1 if t− ≤ mσ ∧ t− ≤ mw ∧  2. hσ (t) := • ,   tn+1 ∩• t = ∅  xn+1 otherwise 3. Bσ := Bw ∪ { eft(tn+1 ) ≤ hw (tn+1 ) } ∪ { 0 ≤ hσ (t) ≤ lft(t) | t ∈ T ∧ t− ≤ mσ }. A short example should illustrate the calculation of parametric states. We use Kσ as a shorthand for {zσ | Bσ }. Let us consider the Time Petri net Z in Fig. 1. It is easy to see that Kε = {( (0, 1, 1), (x0 , ♯, ♯, x0 ) ) | {0 ≤ x0 ≤ 3}}. | {z } | {z } | {z } mε hε Bε After firing the sequence σ = t4 the net Z2 is in a state belonging to Kσ = Kt4 . Kt4 = {( (1, 1, 0), (x0 + x1 , ♯, x1 , ♯) ) | {2 ≤ x0 ≤ 3, x0 + x1 ≤ 5, 0 ≤ x1 ≤ 4}}. | {z } | {z } | {z } mt4 ht4 Bt4 The set of conditions Bt4 is the union of the three sets −  Bε , {eft(t4 )≤ hε (t4 )} = {2 ≤ x0 } and {0 ≤ hσ (t) ≤ lft(t) | t ≤ mσ } = x0 + x1 ≤ 5, . 0 ≤ x1 ≤ 4 By repeatedly firing the transitions t3 and t4 we obtain the parametric states zt4 t3 and zt4 t3 t4 and Kt4 t3 and Kt4 t3 t4 : 25 2 ≤ x0 ≤ 3, x0 + x1 ≤ 5, Kt4 t3 = {((0, 1, 1), (x0 + x1 + x2 , ♯, ♯, x2 )) | 2 ≤ x1 ≤ 4, x0 + x1 + x2 ≤ 5, } 0 ≤ x2 ≤ 3 2 ≤ x0 ≤ 3, 2 ≤ x1 ≤ 4, 2 ≤ x2 ≤ 3, Kt4 t3 t4 = {((1, 1, 0), (x0 + x1 + x2 + x3 , ♯, x3 , ♯)) | 0 ≤ x3 ≤ 4, x0 + x1 ≤ 5, x0 + x1 + x2 ≤ 5, }. x0 + x1 + x2 + x3 ≤ 5 Obviously, some of the inequalities are redundant. For instance, the inequalities of the set Bt4 t3 t4 can be reduced to the set   2 ≤ x0 ≤ 3, 2 ≤ x1 ≤ 4, 2 ≤ x2 ≤ 3, . 0 ≤ x3 ≤ 4, x0 + x1 + x2 + x3 ≤ 5  In general, the number of inequalities in Bσ is at most min{2 · n · |T | + 1 , (n + 1) · (n2 + 2)} (cf. [18]). Liveness can be defined in several ways for Petri nets [15]. We will use the standard “L4-live” variant, which states that every transition in a PN is potentially enabled in any reachable marking. More exactly, a transition t in a Petri net (N , m0 ) is called live in (N , m0 ) iff for every reachable marking m in (N , m0 ) there exists a sequence of firings starting from m, which includes t. 3 Time Constrains for Boundedness Let (N , m0 ) be a live and unbounded Petri net. We would like to check, whether it is possible to make this net bounded, not losing its liveness, by transforming it into a Time Petri net (with the same skeleton), i.e. by adding intervals to its transitions. To solve this problem we will associate transition intervals (if possible), which would exclude runs leading to unboundedness. We start by recalling some properties of live and bounded Petri nets considered in our article [12]. Then, instead to assign priorities to the transitions we add intervals. We will show that this time solution is more precise than the solution with priorities. In this connection "more precise" means that the set of reachable markings in the time- dependent net (sometimes properly) covers the set of reachable markings in the net with priorities. It is clear that if a live PN is bounded then there exists a feasible cyclic run, including all transitions of the PN. Furthermore, a TPN is obtained from a PN by a adding time interval to each transition. Then the reachability tree is a subgraph of the reachability tree of the PN. Hence, it is obvious that if for some interval function I the TPN Z = (N , m0 , I) is live and bounded, then there exists a feasible cyclic run in (N , m0 ) which includes all transitions of N . Proposition 1. Let (N , m0 ) be a live and unbounded Petri net. If there exists an in- terval function I such that the TPN (N , I, m0 ) is live and bounded, then there exists a T-invariant without zero components for N , i.e. all transitions in N are covered by some T-invariant. As we already set in [12], given a live and unbounded Petri net (N , m0 ), before looking for times, which would transform the net into a bounded (and still live) Petri net, it makes sense first to check necessary conditions. First one could compute T-invariants 26 for the net N . If there is no T-invariant, covering all transitions in N , then the net cannot be recovered, i.e., the net cannot become live due to adding time, priorities etc. If there is such a T-invariant, then a more strong necessary condition can be checked: whether there exists a feasible cyclic run in (N , m0 ), which includes all transitions in N , i.e. a cyclic run realizing one of T-invariants with non-zero components. To do this check the algorithm, proposed in [5] by J. Desel, can be used. This algorithm is based on constructing a coverability net — a special extension of a coverability graph, and can take an exponential time. However, if a net does not have too much concurrency and a small number of unbounded places, this method can be acceptable. Now let (N , m0 ) be a live and unbounded Petri net, and let the above necessary conditions are satisfied. We would like to find time intervals for the transition that will make the net bounded, keeping its liveness. The procedure will be illustrated by the net (N ∗ , m∗0 ) in Fig. 2. S1 S4 2 c a b d S3 S2 S5 Fig. 2. An example of a live and unbounded marked Petri net (N ∗ , m∗0 ). The following algorithm is a modification of the algorithm given in [12]. Here reason we use the stages 1,2 and 3 of the ’old’ algorithm and add new stages 4 and 5. Stage 1. Find all minimal feasible cycles, which include all transitions. As al- ready mentioned, this can be done by the technique described by J. Desel in [5]. More- over, following this technique for each minimal feasible cyclic run σ we can simultane- ously find a finite initial run τ , such that τ σ ⋆ is an initial run in (N , m0 ). If (N, m0 ) does not have such cycles, then the problem does not have a solution. So, let C(N , m0 ) := { τ σ | τ σ ⋆ is an initial run in (N , m0 ), τ does not include σ and σ includes all transitions in N } be a set of all minimal feasible cyclic runs together with prefixes leading to the cycles. Thus, for example, the net (N ∗ , m∗0 ) in Fig. 2 has five minimal cyclic runs with all transitions. Three of them have empty prefixes, and two have prefixes τ1 = b and τ2 = ba, respectively: 27 τ = 1 babcda z}|{ b abacbd babcad and . babacd |{z} bacbad ba τ2 = Stage 2. Construct a spine tree. A spine tree is a subgraph of a reachability tree, containing exactly all runs from C(N , m0 ). 1,0,0,1,0 b 0,1,1,1,0 a 1,0,1,1,0 b 0,1,2,1,0 a c 1,0,2,1,0 0,1,0,0,1 c a d 1,0,0,0,1 1,0,0,0,1 0,1,0,1,0 b d d a 0,1,1,0,1 1,0,0,1,0 1,0,0,1,0 1,0,0,1,0 a d 1,0,1,0,1 0,1,1,1,0 d 1,0,1,1,0 Fig. 3. The spine tree for the net (N ∗ , m∗0 ). The spine tree for Petri net (N , m0 ) from our example is shown in Fig. 3. Note, that a spine tree contains the behavior that should be saved to keep a Petri net live. Stage 3. Construct a spine-based coverability tree. A spine-based coverability tree is a special kind of a coverability tree, that includes a spine tree as a backbone. Leaves in a spine-based coverability tree will be additionally colored with green or red. This coloring will be used then for computing transition priorities. The spine-based coverability tree for a Petri net (N , m0 ) is defined constructively by the following algorithm: Step 1. Start with the spine tree for (N , m0 ). Color all leaves in the spine tree in green. 28 Step 2. Repeat until all nodes are colored: For each uncolored node v labeled with a marking m: 1. check whether there is a marking m′ , directly reachable from m and not included t in the current tree. For each such marking m′ , where m → m′ : (a) Add a node v labeled with m as well as the corresponding arc from v to v ′ ′ ′ labeled with t. (b) If the marking m′ strictly covers a marking in some node on the path from the root to v ′ , then v ′ becomes a leaf and gets the red color. (c) Otherwise, if the marking m′ coincides with a marking labeling some node on the path from the root to v ′ , then v ′ becomes a leaf and gets the green color. (d) Otherwise, leave v ′ uncolored. 2. Color the node v in yellow. The spine-based coverability tree for our example net (N ∗ , m∗0 ) is shown in Fig. 4. Here node colors are used to illustrate the tree construction. A leaf and some inner node have the same color, if they have the same markings, or the leaf marking strictly covers the marking of its ancestor. Strictly covering leaves are marked with the ω-symbol, they are ’red’ leaves. All other leaves are ’green’ leaves. 1,0,0,1,0 1,0,0,1,0 b b 0,1,1,1,0 0,1,1,1,0 a a 1,0,1,1,0 1,0,1,1,0 b b 0,1,2,1,0 0,1,2,1,0 a c a c 1,0,2,1,0 0,1,0,0,1 1,0,2,1,0 0,1,0,0,1 b c a d b c a d 0,1,2,1,0 1,0,0,0,1 1,0,0,0,1 0,1,0,1,0 0,1,2,1,0 1,0,0,0,1 1,0,0,0,1 0,1,0,1,0 ω ω b d b d a b d b d a 0,1,1,0,1 1,0,0,1,0 0,1,1,0,1 1,0,0,1,0 1,0,0,1,0 0,1,1,0,1 1,0,0,1,0 0,1,1,0,1 1,0,0,1,0 1,0,0,1,0 ω ω a d a d 1,0,1,0,1 0,1,1,1,0 1,0,1,0,1 0,1,1,1,0 b d b d 0,1,2,0,1 1,0,1,1,0 0,1,2,0,1 1,0,1,1,0 ω ω Fig. 4. The spine-based coverability tree for (N ∗ , m∗0 ): Left: A leaf and some inner node have the same color, if they have the same markings, or the leaf marking strictly covers the marking of its ancestor. Strictly covering leaves are marked with the ω- symbol. Right: The spine-based coverability tree for (N ∗ , m∗0 ) after finishing stage 3. Stage 4. Compute a parametric state space. Let T be a spine-based coverability tree. Consider the TPN (N , m0 , I) with time interval [at , bt ] for each transition t ∈ T . 29 All at , bt are unknown and have to be calculated in stage 5. By the construction of T , all its leaves are colored either in green, or red. In this stage we construct an interval function I : T → Q+ + 0 × Q0 . For this we consider every path from the root to a green leaf as a parametric run. Additionally, we forbid a branching to a red leaf using strict inequality. (1) Let vg be a green leaf and let σ be the path from the root to this leaf. Consider the parametric run (σ(x), Bσ ). (2) Let vr be a red leaf. Consider the path σ from the root to this leaf. Let v ∗ be the youngest ancestor of vr such that at least one run goes from v ∗ to a green leaf vg . The initial node v0 is labeled with the marking m0 . Let the node v ∗ be labeled with m∗ , vr with mr and vg with mg . Finally, let σ ∗ be the path from the root to the node v ∗ , σr the path from the node v ∗ to vg and tr σr the path from the node v ∗ to vr . That means, we have the situation σ∗ σg σ∗ t σ m0 → m∗ → vg , m0 → m∗ → r r → v, σ = σ ∗ tr σ r and there is not a path from a node in σr to a green one. Hence, using time, we will forbid the firing of the transition tr in m∗ . For this reason we add to Bσ∗ the constrain (strong inequality) hσ∗ (tr ) < atr . Stage 5. Compute a parametric state space. Let [ B := {Bσ | σ is an initial run to a green node} ∪ {0 ≤ at ≤ bt | t ∈ T }. B is the set of all constrains which have to be fulfilled in order to keep the live behavior of the net and to forbid all transition sequences leading to unboundedness. Clearly, B is a system of linear inequalities and it can be solved in Q+ 0 . Actually, we are interested in finding solutions for all at ’s and bt ’s such that the resulting system of inequalities is solvable. Of course, when we can find rational values for solutions for all at ’s and bt ’s then we can find also integer values for them. At this point we would like to notice that instead of the full parametric space of the spine-based coverability tree we can use only a part of them, consisting of paths including together all transitions of the net. In this case it is possible that some markings which does not lead to unboundedness in the PN will be not reachable in the TPN. Applying the procedure of the stages 4 and 5 to the spine-based coverability tree for our example net (N ∗ , m∗0 ) (cf. Fig. 4) we sequentially obtain the following parametric state space and eventually the following inequality system B: Kε = { (1, 0, 0, 1, 0), (♯, x0 , ♯, ♯) | 0 ≤ x0 ≤ bb },  Kb = { (0, 1, 1, 1, 0), (x1 , ♯, ♯, ♯) | ab ≤ x0 ≤ bb , 0 ≤ x1 ≤ ba },  Kba = { (1, 0, 1, 1, 0), (♯, x2 , ♯, ♯) | ab ≤ x0 ≤ bb , aa ≤ x1 ≤ ba 0 ≤ x2 ≤ bb },    ab ≤ x0 ≤ bb , aa ≤ x1 ≤ ba , ab ≤ x2 ≤ bb , Kbab = (0, 1, 2, 1, 0), (x3 , ♯, x3 , ♯) , 0 ≤ x3 ≤ ba , x3 ≤ bc    ab ≤ x0 ≤ bb , aa ≤ x1 ≤ ba , ab ≤ x2 ≤ bb , Kbabc = (0, 1, 0, 0, 1), (x3 + x4 , ♯, ♯, x4 ) , ac ≤ x3 ≤ bc , x3 + x4 ≤ ba , 0 ≤ x4 ≤ bd     ab ≤ x0 ≤ bb , aa ≤ x1 ≤ ba , ab ≤ x2 ≤ bb ,  Kbabcd = (0, 1, 0, 1, 0), (x3 + x4 + x5 , ♯, ♯, ♯) ac ≤ x3 ≤ bc , ad ≤ x4 ≤ bd , 0 ≤ x5 ,  x3 + x4 + x5 ≤ ba ,      ab ≤ x0 ≤ bb , aa ≤ x1 ≤ ba , ab ≤ x2 ≤ bb ,  Kbabcda = (1, 0, 0, 1, 0), (♯, x6 , ♯, ♯) ac ≤ x3 ≤ bc , ad ≤ x4 ≤ bd , 0 ≤ x5 ,  aa ≤ x3 + x4 + x5 ≤ ba , 0 ≤ x6 ≤ bb  30     ab ≤ x0 ≤ bb , aa ≤ x1 ≤ ba , ab ≤ x2 ≤ bb ,  Kbabca = (1, 0, 0, 0, 1), (♯, x7 , ♯, x7 ) ac ≤ x3 ≤ b c , a a ≤ x3 + x4 ≤ b a , 0 ≤ x4 ≤ b d ,  0 ≤ x7 ≤ bd , x7