=Paper=
{{Paper
|id=Vol-1492/Paper_27
|storemode=property
|title=Controlling Petri Net Behavior Using Time Constraints
|pdfUrl=https://ceur-ws.org/Vol-1492/Paper_27.pdf
|volume=Vol-1492
|dblpUrl=https://dblp.org/rec/conf/csp/LomazovaP15
}}
==Controlling Petri Net Behavior Using Time Constraints==
https://ceur-ws.org/Vol-1492/Paper_27.pdf
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