In this paper we examine how it is possible to control Petri net behavior with the help of time constraints. Controlling here means to force a process to behave in a desirable way by ascribing priorities to transitions and hence transforming a classic Petri net into a Priority Petri net. Liveness and boundedness are crucial properties in many application areas, e.g. work ow modeling and bioinformatics. The main correctness property for work ow models is soundness, which can be reduced to the liveness and boundedness of a modi ed net. In biological models, liveness and boundedness are important for system stability. The problem of transforming a given live, but unbounded Petri net into a live and bounded one by adding priority constraints is studied in this paper. We specify necessary conditions for the solvability of this problem and present a method for ascribing priorities to net transitions in such a way that the resulting net becomes bounded while staying live.
Petri nets are widely used for modeling and analysis of distributed systems. These can range from technical systems to systems of business processes, or biological systems. Although such systems are very di erent in their substance they all have common properties, such as reiteration of all subprocesses or returning to some initialization in the system, or containing nitely or in nitely many different states etc. The rst two properties concern the liveness of the model, the second two are covered by boundedness studies. In most of the practical systems the niteness of all possible situations is a highly desired property, i.e., the model should be bounded.
A typical example is a business process model, represented by a work ow net
| a special kind of a Petri net. The crucial correctness property for work ow
nets is soundness, also called proper termination [
Checking soundness of work ow 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 work ow net. Thus ensuring
liveness and boundedness of a model can be applied for asserting soundness of
work ow nets. In biological systems liveness and boundedness ensure system
stability [
In practice it could be 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 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 scheduling. In
[
Priority scheduling is an appropriate solution for work ow systems. For
biological system it is not so appropriate, since there is no mechanism to give priority
to this or that action in biological systems. Scheduling biological systems with
the help of time constraints would provide a much more natural solution [
In this paper we study adding priorities in order to transform a live and unbounded model, represented by a Petri nets, into a live and bounded model. Thereby we want to fully preserve the structure of the net.
The paper is organized as follows. In Section 2 we recall some basic de nitions in the theory of Petri nets and subsequently in Section 3 we give a motivating example. In Section 4 we represent a su cient condition for transforming a live and unbounded Petri net into a live and bounded one by adding priorities and nally Section 5 contains some conclusions. 2
Let Nat denote the set of natural numbers (including zero).
Let P and T be disjoint sets of places and transitions and let F (P T ) [ (T P ) ! Nat be a ow relation. Then N = (P; T; F ) is a unmarked Petri net. A marking in a Petri net is a function m : P ! Nat, mapping each place to some natural number (possibly zero). A Petri net (N ; m0) is an unmarked Petri net N with its initial marking m0. We use vector notation for marking, xing some ordering of places in a Petri net.
Pictorially, P -elements are represented by circles, T -elements by boxes, and the ow relation F by directed arcs. Places may carry tokens represented by lled circles. A current marking m is designated by putting m(p) tokens into each place p 2 P .
For a transition t 2 T an arc (x; t) is called an input arc, and an arc (t; x) { an output arc.
A transition t 2 T is enabled in a marking m i 8p 2 P m(p) F (p; t). An enabled transition t may re yielding a new marking m0, such that m0(p) = m(p) F (p; t) + F (t; p) for each p 2 P (denoted m !t m0, or just m ! m0). Then we say that a marking m0 is directly reachable from a marking m.
A marking m is called dead i it enables no transition.
A run in N is a nite or in nite sequence of rings m1 !t1 m2 !t2 : : : . An initial run in (N ; m0) is a run, starting from the initial marking m0. A cyclic run is a nite run starting and ending at the same marking. A maximal run is either in nite, or ends with a dead marking.
We say that a marking m is reachable from a marking m0 i there is a run m0 = m1 ! m2 ! ! mn = m; m is reachable in (N; m0) i m is reachable from the initial marking. For an unmarked Petri net N by R(N ; m) we denote the set of all markings reachable in N from the marking m, by R(N ) { the set of all markings reachable in N from its initial marking. A run in (N ; m) is called feasible i 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 2 N at such that after ring 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 marking m, to a vertex v0, corresponding to a marking m0 i m !t m0 in N .
A reachability graph may be also represented in the form of a reachability tree, which can be de ned in a constructive form. We start from the initial marking as a root. If for a current leave v labeled with a marking m, there is already a node v0 6= v lying on the path from the root to v and labeled with the same marking m, we notify v to be a leave 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 nite paths from nodes to leaves.
A place p in a Petri net is called bounded i for every reachable marking the number of tokens residing in p does not exceed some xed bound 2 Nat. A marked Petri net is bounded i all its places are bounded.
It is easy to see, that a Petri net (N ; m0) is bounded i its reachability set R(N ; m0), and hence its reachability graph, are nite.
A marking m0 covers a marking m (denoted m0 m) i for all places p from P , m0(p) m(p). The relation is a partial ordering on markings in N . By the ring rule for Petri net, if a sequence of transitions is enabled in a marking m, and m0(p) m(p), then this sequence of transitions is also enabled in m0. A marking m0 strictly covers a marking m (denoted m0 > m) i m0(p) m(p) and m 6= m.
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 on a place. Formally, a generalized marking is a mapping m : P ! Nat [ f!g. A coverability tree is de ned constructively. It is started from the initial marking and is successively constructed as a reachability tree. The di erence is that when a marking m0 of a current leave v0 in a reachability tree strictly covers a marking m of a node v, lying on the path from the root to v0, then in a coverability tree the node v0 gets a marking m!, where m!(p) = !, if m0(p) > m(p), and m!(p) = m0(p), if m0(p) = m(p). For generalized markings enabling of a transition and a ring rule is de ned as for usual markings except that !-marked places are ignored. Each place p, which was marked by !, remains !-marked for all possible run continuations.
Let N = (P; T; F ) be an unmarked Petri net. A priority relation for N is a partial order (T; ), i.e., the relation is re exive, antisymmetric and transitive. For a subset S T a minimal element in S (w.r.t. ) is a transition t 2 S, such that for all t 2 S, t0 6= t implies t0 6 t. Obviously, there can be several minimal elements in S.
A (marked or unmarked) Petri net with priorities is a (marked or unmarked) Petri net together with a priority relation. For P = (N ; ) being a Petri net with priorities, we call the Petri net N the skeleton of P and denote it with S(P). A priority relation can be speci ed by assigning a priority label (natural number) (t) 2 Nat to each transition t. Then we set t t0 i (t) < (t0) and represent priority graphically by priority labels, given in curly brackets.
Fig. 2 gives an example of a Petri net with priorities. Here (a) = 1; (b) = 3; (c) = 2; (d) = 2, and hence a c; a d; c b; d b.
S1 a {1}
{3} b S2
S3 2
S4 c {2}
{2} d S5
The ring rule for a Petri net P = (N; ) with priorities is de ned as follows. Let m be a marking in N , and Q be a set of transitions enabled in m (according to usual rules for Petri nets). Then only minimal w.r.t. transition may re in m, i.e. transitions with higher priorities are always preferred over transitions with lower priorities.
For the Petri net P1 = (N1; ; m0) in Fig. 2 the ring sequence baba is feasible and leads to the marking m1 = (0; 1; 2; 1; 0). Both transitions c and b are enabled in m1, but only c can re in m1, since b c.
Liveness can be de ned in several ways for Petri nets [
In [
Consider now two Petri nets in Fig.3. These two Petri nets di er only in their initial markings. The left Petri net has the empty initial marking, and the right one has initially three tokens in the place B. Both nets are live and unbounded. Actually, all their places are unbounded. Both nets are covered by (the same) two minimal transition invariants, since these nets have the same net structure.
However, there is a great di erence between these nets. The right net can
be transformed into a live and bounded net by ascribing time durations to its
transitions, which are graphically represented in angle brackets here. This turns
the right net into a Timed Petri net. The reader can nd ring rules for Timed
Petri nets in [
These examples show, that a possibility to transform a live and unbounded net into a bounded one can depend not only on transition invariants, but on initial markings as well.
Live and unbounded Petri nets were considered also in [
pro_A <0>
A r1
B r4 E <2> <2> <1> r6 r5 F <1> r2
C <0> con_C the execution in such a way, that the number of tokens in each place will be not greater that some xed 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 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. 4
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 Petri net with priorities (with the same skeleton), i.e. by adding priorities to its transitions. To solve this problem we shall try for transition priorities, which would exclude runs leading to unboundedness.
We start by studying some properties of live and bounded Petri nets. Proposition 1. Let (N ; m0) be a live and bounded Petri net. Then there exists a feasible cyclic run, including all transitions in N .
Proof. Since (N ; m0) is live, no dead marking is reachable in it, and all maximal runs are in nite. The net (N ; m0) is bounded, hence its reachability set is nite, and each in nite run includes a cycle. Moreover, such a run has a form ?, where is a (pre x) nite initial run, and is a feasible cyclic run.
Liveness means that each transition may potentially re from any reachable marking. Then there exists a run, which includes all net transitions in nitely often. The cyclic part of this run contains all net transitions.
Proposition 2. Let (N ; m0) be a Petri net, and let (N ; ; m0) be a Petri net with priorities, obtained from N by adding a transition priority relation . Then the reachability tree for (N ; ; m0) is a subgraph of the reachability tree for (N ; m0).
Theorem 1. Let (N ; m0) be a Petri net. If for some priority relation the Petri net (N ; ; m0) with priorities is live and bounded, then there exists a feasible cyclic run in (N ; m0), which includes all transitions in N .
Corollary 1. Let (N ; m0) be a live and unbounded Petri net. If there exists a priority relation on the set T of transitions in N , s.t. the Petri net (N ; ; m0) with priorities is live and bounded, then there exists a transition invariant without zero components for N , i.e. all transitions in N are covered by some T-invariant.
So, given a live and unbounded Petri net (N ; m0), before looking for constraints, which would transform the net into a bounded (and still live) Petri net, it makes sense rst to check necessary conditions. First one could compute transition invariants for the net N . If there is no a transition invariant, covering all transitions in N , then the net cannot be recovered. Note, that transition invariants can be computed in polynomial time on the size of the net.
If there is such a transition 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 transition invariants
with non-zero components. To do this check the algorithm, proposed in [
Now let (N ; m0) be a live and unbounded Petri net, and let necessary conditions hold for it. We would like to nd transition priorities, that will make the net bounded, keeping its liveness. The procedure will be illustrated on the net N1 in Fig. 2.
We do this in four stages.
Stage 1. Find all minimal feasible cycles, which include all
transitions. As already mentioned, this can be done by the technique described by
J. Desel in [
If (N; m0) does not have such cycles, then due to the Theorem 1 the problem does not have a solution. So, let
C(N ; m0) := f j ? is an initial run in (N ; m0); does not include and includes all transitions in N g be a set of all minimal feasible cyclic runs together with pre xes leading to the cycles.
Thus, for example, the net (N1; m0) in Fig. 2 has ve minimal cyclic runs with all transitions. Three of them have empty pre xes, and two have pre xes 1 = b and 2 = ba, respectively: babcda babcad babacd and
1= z}|{ abacbd bba bacbad . |{2z=}
Stage 2. Construct a spine tree. A spine tree is a subgraph of a reachability tree, containing exactly all runs from C(N ; m0).
The spine tree for Petri net (N1; 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 de ned constructively by the following algorithm:
Step 1. Start with the spine tree for (N ; m0). Color all leaves in the spine tree in green.
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 m0, directly reachable from m and not t included in the current tree. For each such marking m0, where m ! m0: (a) Add a node v0 labeled with m0 as well as the corresponding arc from v to v0 labeled with t. (b) If the marking m0 strictly covers a marking in some node on the path from the root to v0, then v0 becomes a leave and gets the red color. b d d 0,1,1,0,1 a 1,0,1,0,1
a 1,0,2,1,0 1,0,0,0,1 c d 1,0,1,1,0 1,0,1,1,0 0,1,2,1,0 b a b c
a
d d
a (c) Otherwise, if the marking m0 coincides with a marking labeling some node on the path from the root to v0, then v0 becomes a leave and gets the green color.
(d) Otherwise, leave v0 uncolored. 2. Color the node v in yellow.
The spine-based coverability tree for our example net N1 is shown in Fig. 4. Here node colors are used to illustrate the tree construction. A leave and some inner node have the same color, if they have the same markings, or the leave 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.
Stage 4. Compute a priority relation. Let T be a spine-based coverability tree. By the construction of T , all its leaves are colored either in green, or red. In this stage we construct a priority relation R T T . Initially R is empty. b 1,0,1,0,1 0,1,ω2,0,1 b b d d 0,1,1,0,1
a 1,0,2,1,0 c d 1,0,1,1,0 0,1,2,1,0 b a b
b 0,1,ω1,0,1 c
a
d d
a
Let v be one of the leaves in with the maximal distance from the root, let u be the parent of v. Two cases are possible.
(1) All children of u (including v) have the same color (green, or red). Then delete all children of u from the tree, make u a leave and color it with the color of v.
(2) Some children nodes are colored in red, and some { in green. { If u is not in the spine of T , then delete all children of u from the tree, make u a leave and color it in red. { If not, let Tr be the set of all transitions, corresponding to arcs going from u to nodes colored in red, and similarly, Tg { the set of all transitions labeling arcs going from u to nodes colored in green. Note, that Tr \ Tg = ;. Then de ne Ru = f(t1; t2)jt1 2 Tr; t2 2 Tgg, and add all pairs from Ru to the priority relation R, i.e. R := R [ Ru. After that delete all children nodes of u, and make u a leave colored in green.
Repeat this procedure until there are no more red leaves in T . Finally, de ne the relation for (N ; m0) as the transitive and re exive closure of R.
Applying the procedure of the stage 4 to the spine-based coverability tree for our example net (N1; m0) (cf. Fig. 4) we sequentially obtain: d b, c b. That means, that we could choose even weaker priorities, than shown in Fig. 2, i.e. transitions a, c and d could have the same priorities to guarantee liveness and boundedness.
Theorem 2. Let (N ; m0) be a live and unbounded Petri net, for which there exists a feasible cyclic run, which includes all transitions in N . Let then be the relation constructed for (N ; m0) according to the algorithm described above. If is a partial order (i.e. is antisymmetric), then is a priority relation for N , and the Petri net (N ; ; m0) with priorities is live and bounded. Proof. (Sketch) Note, that if a node in a spine-based coverability tree has a descendant leave, colored in red, then the marking of this node can enable an unbounded run, leaving to a !-marking. If it has a descendant leave, colored in green, then the marking of this node can enable a cycle, which includes all transitions in N .
At each step at the stage 4 the relation R is extended in such a way, that cyclic runs prioritize unbounded runs.
Each step at the stage 4 reduces the number of nodes in a spine-based coverability tree, so the process on the stage 4 will terminate. Initially, the spine tree for (N ; m0) is not empty, and the root has descendant nodes colored in green, so the process will terminate correctly, i.e. with only green leaves (possibly one).
The resulting Petri net (N ; ; m0) with priorities is live, because it retains all initial cycles with all transitions.
The net (N ; ; m0) is bounded, because all unbounded branches in (N ; m0) are cut by priorities.
The above algorithm allows to compute priorities needed for the net boundedness, only in the case, when such priorities exist and the algorithm computes a partial order. We have presented some necessary conditions for existence of needed priorities, but we do not know whether these conditions are su cient.
Note also, that in the above algorithm we keep all feasible cycles, containing all transitions. The algorithm can be modi ed to keep at least one such cycle. It is an open problem, whether a failure of the modi ed algorithm, i.e. the computed relation is contradictory (not a partial order), means that required priorities do not exist. 5
In this paper we have investigated the possibility for obtaining a live and bounded Petri net from a live and unbounded one by adding priorities. We have presented necessary conditions for existence of such priorities. This conditions are not sufcient, but help to exclude unsolvable cases. Then an algorithm for computing transition priorities for transforming a live and unbounded Petri net into live and bounded net by ascribing priorities to transition was developed. When terminates successfully, this algorithm guarantees that computed priorities solve the problem, i.e. the net with priorities is live and bounded. It's an open problem, whether a solution exists, when the algorithm fails to compute consistent priorities. The further research will concern this open problem and the study of the existence of more e ective methods.
Another challenging question { to translate the priorities into time intervals or time durations for transitions. This problem is rather important for biological systems, because priorities do not go with a primary eligibility criterion.