PII. S0161171204403378 http://ijmms.hindawi.com
© Hindawi Publishing Corp.
LOWER AND UPPER BOUNDS OF SHORTEST PATHS IN REACHABILITY GRAPHS
P. K. MISHRA Received 22 March 2004
We prove the following property for safe marked graphs, safe conflict-free Petri nets, and live and safe extended free-choice Petri nets. We prove the following three results. If the Petri net is a marked graph, then the length of the shortest path is at most(|T|−1)·|T|/2.
If the Petri net is conflict free, then the length of the shortest path is at most(|T|+1)·|T|/2.
If the Petri net is live and extended free choice, then the length of the shortest path is at most|T|·|T+1|·|T+2|/6, whereT is the set of transitions of the net.
2000 Mathematics Subject Classification: 68R10, 90C35, 94C15.
1. Introduction. LetM1,M2be the two markings of the reachability graph of a safe Petri net such thatM2is reachable fromM1. Since a safe Petri net withnplaces has at most 2nmarkings, this length is less than 2n. However, in some situations, we would like to have a better bound. An example is a system with some state—a state reachable from any other reachable state—which should be reached after a recovery action. If the home state can be only reached after an exponential number of actions, then the system cannot recover in reasonable time.
Another reason to study this question is that the length of shortest paths between pairs of markings is related to the complexity of the model checker for arbitrary safe Petri nets.
If the Petri net is a marked graph, then the length of the shortest path is at most (|T|−1)·|T|
2 . (1.1)
If the Petri net is conflict free, then the length of the shortest path is at most (|T|+1)·|T|
2 . (1.2)
If the Petri net is live and extended free-choice, then the length of the shortest path is at most
|T|·|T+1|·|T+2|
6 , (1.3)
whereT is the set of transitions of the net.
The paper is organized as follows.Section 2contains basic definitions and results.
Section 3studies so-called biased sequences. Using the results ofSection 3, our three
results are proved in Sections4and5. Finally,Section 6shows that for safe persistent systems there exist no polynomial bounds for the lengths of shortest paths.
2. Preliminaries. LetSandTbe finite and nonempty disjoint sets and let
F⊆(S×T )∪(T×S). (2.1)
If for eachx∈Sandy∈Tit happens that(x,y)∈For(y,x)∈F, thenN=(S,T ,F) is called a net.Sis the set of places andTis the set of transitions ofN. Pre- and postsets of elements are denoted by the dot notation
•x=
y|(y,x)∈F , x• =
y|(x,y)∈F
. (2.2)
This notion is extended to the set of elements also. A set c of transitions ofN is a conflict set if eitherc=s•for some placessorc= {t}for some transitiontsatisfying
•t=φ.
A marking ofNis a mappingM:S→N+, whereN+is the set of nonnegative integers.
A placesis called marked by a markingMifM(s) >0. A markingMenables a transition tif it marks every place of•t. The occurrence of an enabled transitiontleads to the successor markingM1(writtenM→M1) which is defined for every place ofsby
M1(s)=
M(s)−1 ifs∈•t/t•, M(s)+1 ifs∈t•/•t,
M(s) ifs∈•t∪t•ors∈•t∩t•.
(2.3)
If M0 t1→M1 t2→ ··· tn→Mn, then σ =t1t2···tn is called an occurrence sequence and we writeM0 σ→Mn. This notion includes the empty sequenceε:M ε→Mfor each markingM.
A sequence σ is enabled at a marking M ifM σ→M1 for some marking M1. We callM1 reachable fromM if M σ→M1 for some occurrence sequenceσ. The set of all markings reachable fromM is denoted by[M. Given a sequenceσ of transitions and a transitiont, #(t,σ )denotes the number of occurrences oft inσ. For a set of transitions, #(u,σ )is the sum of all #(t,σ )fort∈u. Ifuis the set of all transitions of the net, then #(u,σ )is called the length ofσ.
A sequenceσ of transitions is a permutation of a sequenceτ if #(t,σ )=#(t,τ) for every transition t. A net system is a pair(N,M0) whereN is a net and M0 is a marking ofN, called initial marking of(N,M0). A marking is called reachable in a system (N,M0)if it is reachable fromM0. A system(N,M0)is called live if for every reachable markingM and every transitiontthere exists a markingM1∈[Mthat enablest. It is called safe if every reachable marking M satisfiesM(s)≤1 for every places. The reachability graph(V ,E)of a system(N,M0)is the directed graph defined byV=[M0 andE= {(M1,M2)∈V×V|M1 t
→M2for some transitionst}.
We use the following two results, which follow immediately from the occurrence rule and are well known.
Lemma2.1. (i)LetM1 σ→M2be an occurrence sequence. Then, for every places, M2(s)=M1(s)+#(•s,σ )−#(s•,σ ). (2.4) (ii)LetM1 σ→M2and letM1 τ→M3be an occurrence sequence. Ifτis a permutation of σ, thenM2=M3.
3. Biased occurrence sequences. The purpose of this section is to proveTheorem 3.4, which yields an upper bound for the shortest paths between two markings M1
andM2, whenM2can be reached fromM1by means of a so-called biased occurrence sequence. This theorem will easily lead to our first two results concerning marked graphs and conflict-free systems. Moreover, it will be used as a lemma in the proof of our third result on extended free-choice systems.
Definition3.1. A sequenceσof transitions of a netNis called biased if, for every conflict setcofN, at most one transition ofcoccurs inσ.
Lemma3.2. LetM1 σ→M2 be a biased occurrence sequence of a net. Ifσ =σ1σ2t such that
(i) tis a transition that does not occur inσ1,
(ii) every transition occurring inσ2also occurs inσ1, thenM1 σ1tσ→2 M2is also an occurrence sequence.
Proof. By induction on the length ofσ2. Base. Ifσ2=ε, thenσ1σ2t=σ1t=σ1tσ2.
Step. Ifσ2≠ε, thenσ2t=σ21ufor some sequenceσ2and some transitionu. LetM1 σ1→M3 σ2→M4 u→M5 t→M2.
We first prove M4 t→M6 u→M2 for some marking M6. If t=u, we are done; so assumet≠u.
We claim thatM4enablest. Letsbe an arbitrary place in the preset oft; we prove thatM4(s) >0. Consider the following two cases.
(i) Ifs∈u•, thenM4(s)≥M5(s). Sincetis enabled atM5, we haveM5(s) >0.
(ii) Ifs∈u•, we have
M5(s)=M1(s)+#
•s,σ1σ2
−#
s•,σ1σ2
. (3.1)
ByLemma 3.2(ii) and sinceuoccurs inσ2,uoccurs at least twice inσ1σ2. Sinceu∈ •s, we get #(•s,σ1σ2)≥2.
Sinceσ is biased andtoccurs inσ,tis the only transition in the postset ofs that occurs in σ. ByLemma 3.2(i) and (ii), t does not occur in σ1σ2. So #(s•,σ1σ2)=0.
ThereforeM5(s)≥2. SinceM u→M5, we getM4(s)≥1. SinceM4enablest,M4 t→M6
for some markingM6. Sinceσ is biased,
•u∩•t=φ; (3.2)
so the occurrence oftdoes not disableu, and henceuis enabled atM6. Sinceutand tuare permutations of each other, we finally getM4 t→M6 u→M2.
The application of the induction hypothesis toσ1σ21t(taking σ21forσ2) yields an occurrence sequenceM4
σ1tσ21
→M6. The result follows becauseM6 u→M2andσ21u= σ2.
Lemma3.3. LetM1 σ→M2be a biased occurrence sequence of a net. There exists a permutationσ1σ2ofσ such thatM1 σ1σ2
→M2; no transition occurs more than once in σ1and every transition occurring inσ2also occurs inσ1.
Proof. By induction on the length ofσ. Base. Ifσ=ε, takeσ1=σ2=ε.
Step. Ifσ≠ε, thenσ=τtfor some sequenceτ and some transitiont.
By the induction hypothesis, there is a permutationτ1τ2ofτ, enabled atM1, such that no transition occurs more than once inτ1and every transition inτ2also occurs inτ1.
Iftoccurs inτ1, thenσ1=τ1andσ2=τ2tsatisfy the requirements.
Iftdoes not occur inτ1, thenτ1τ2tsatisfies the conditions ofLemma 3.2, and so M1 τ1tτ2
→M2is an occurrence sequence. Takeσ1=τ1tandσ2=τ2.
Theorem3.4. LetM1be a reachable marking of a safe system and letM1 σ
→M2be a biased occurrence sequence. Letkbe the number of distinct transitions occurring in σ. There exists an occurrence sequenceM1 τ→M2such that the length ofτ is at most k·(k+1)/2.
Proof. By induction on the length ofσ. Base. Forσ≠ε, chooseτ=ε.
Step. Ifσ =ε, then byLemma 3.3there exists a permutationτ1τ2ofσ such that M1 τ1τ2
→M2; every transition occurring inτ2occurs inτ1and no transition occurs in τ1more than once. Sinceσ is not the empty sequence,τ1is not empty, and therefore τ2is shorter thanσ. LetM1 τ1
→M3 τ2
→M2. We distinguish two cases.
(i) Every transition occurring inτ1 occurs in τ2. Again by Lemma 3.3there are a permutationp1and a permutationp2ofτ2such thatM3 p1p2→M2with every transition occurring inp2andp1, and no transition occurs inp1more than once. Then a transition occurs inτ1if and only if it occurs inp1. Moreover, no transition occurs more than once in either sequence. So every transitiontsatisfies #(t,τ1)=#(t,p1), that is,τ1andp1
are permutations of each other. LetM1 τ1
→M3 p1
→M4, then for each place it holds that
M4(s)=M1(s)+#
•s,τ1
−# s,τ1
+#
•s,p1
−# s•,p1
(3.3) and hence
M4(s)=M1(s)+2
#
•s,τ1
−# s•,τ1
. (3.4)
Thus, sinceM1,M4∈[M0and(N,M0)is safe, we get
#
•s,τ1
−# s•,τ1
=0. (3.5)
So
M3(s)=M1(s)+#
•s,τ1
−# s•,τ1
=M1(s). (3.6)
Therefore,
M1=M3, M1 →M2. (3.7)
Sinceτ2is shorter thanσ, we can apply the induction hypothesis to it, which yields an occurrence sequenceM1 τ→M2of the desired length.
(ii) There exists a transition which occurs inτ. We apply the induction hypothesis to M3 τ2→M2. Since the number of distinct transitions occurring inτ2is at mostk−1, we get a sequenceM3
p→M2such that the length ofpis at mostk·(k−1)/2. Since no transition occurs inτ1more than once, its length is justk. Let
τ=τ1p. (3.8)
We haveM1 τ→M2. Moreover, the length ofτis at most k+k·(k−1)
2 =k·(k+1)
2 . (3.9)
4. T-systems, marked graphs, and conflict-free systems. If a system has no for- ward branching places (i.e.,|s•| ≤1 for every place), then all its occurrence sequences are biased, soTheorem 3.4 applies to every occurrence sequence and we get the fol- lowing result.
Theorem 4.1. Let(N,M0) be a safe system whereN=(S,T ,F) and|s• | ≤1for everys∈S, and letM1be a reachable marking. LetM2be a marking reachable from M1. There exists an occurrence sequenceM1 τ→M2such that the length ofτis at most (|T|+1)·|T|/2.
Proof. SinceM2is a reachable marking from M1, there exists an occurrence se- quenceM1 σ→M2. σ is biased because every conflict set of N contains exactly one transition, and the number of distinct transitions occurring inσ is at most |T|and, using theTheorem 3.4, the result is obvious.
4.1.T-systems. Theorem 4.1applies in particular toT-systems, in which|s• | ≤1 and, moreover,| •s| ≤1 for every places. The bound of the theorem is reachable for T-systems, that is, there exist aT-system and pairs of reachable markingsM1,M2for which the bound is the exact value of the length of the shortest path leading fromM1
toM2.
4.2. Marked graphs. T-systems satisfying|•s| =1= |s•|for every placesare called marked graphs in [6] or synchronization graphs in [10]. For this class of systems, we can obtain a stronger result.
Theorem4.2. Let(N,M0)be a safe system whereN=(S,T ,F)and|•s| =1= |s•|
for everys∈S. LetM1be a reachable marking. LetM2be a marking reachable fromM1.
There exists an occurrence sequenceM1 τ→M2 such that the length ofτ is at most (|T|−1)·|T|/2.
Proof. SinceM2is a reachable marking from M1, there exists an occurrence se- quenceM1 σ
→M2. We can further assume thatσ has minimal length. We claim that at least one transition ofNdoes not occur inσ. The result then follows fromTheorem 3.4 takingk= |T|−1.
Assume that every transition ofNoccurs inσ. ByLemma 3.3, there exists a permuta- tion ofσ such thatM1 σ1σ2
→M2, no transition occurs more than once inσ1, and every transition occurring inσ2also occurs inσ1. Therefore every transition ofNoccurs in σ and, moreover, they occur exactly once. LetM3be the marking such thatM1 σ1
→M3. We claim thatM1=M3. Letsbe an arbitrary place ofN; byLemma 2.1we have
M3(s)=M1(s)+#
•s,σ1
−# s•,σ1
. (4.1)
Sinceshas exactly one input and one output place, we get
#
•s,σ1
=1=# s•,σ1
. (4.2)
SoM3(s)=M1(s), which proves the claim. SinceM3=M1, we haveM1 σ2
→M2. Since σ1is nonempty,σ2is shorter thanσ, which contradicts the minimality ofσ.
Like the bound ofT-systems, the bound ofTheorem 4.2is also tight. Consider the family of systems. Adding a transitiontn+1such that
•tn+1= s2n
, t•n+1= s2n−1
(4.3) yields a marked graph with|T| =n+1 transitions. The transitiontn+1does not occur in the shortest path fromModdtoMeven. As shown before, the shortest path fromModd
toMevenneeds
n·(n+1)
2 =(|T|−1)·|T|
2 (4.4)
transition occurrences.
4.3. Conflict-free systems. Theorem 4.1 can also be generalized to conflict-free nets, a well-known class of nets studied in [16].
Definition4.3. A netNis called conflict-free if every placesofNsatisfies either
|s•| ≤1 ors• ⊆ •s. A system(N,M0)is conflict-free ifNis conflict-free.
Theorem 4.4. Let(N,M0)be a safe conflict-free system, where N=(S,T ,F) and M1is a reachable marking. LetM2 be a marking reachable fromM1. There exists an occurrence sequenceM1 τ
→M2such that the length ofτis at most(|T|+1)·|T|/2.
Proof. LetRbe the set of places ofNwith more than one transition in their postset.
We proceed by induction on|R|.
Base. ForR=φ, the result follows byTheorem 4.1.
Step. ForR≠φ, lets∈Rbe an element.
Using the definition of conflict-free systems [3,12,13] and by induction hypothesis, the result is obvious.
5. Extended free-choice systems. In this section, we obtain an upper bound for the length of the shortest paths between two reachable markings of a live and safe extended free-choice system. It is never greater than|T|·|T+1|·|T+2|/6, whereTis the set of transitions of the net. Extended free-choice systems are a generalization of a free-choice system introduced in [11].
Definition5.1. A netNis extended free-choice if every two placess,s1ofNsatisfy eithers• =s1•ors•∩s1• =φ; that is, if its conflict sets constitute a partition of its set of transitions. A system(N,M0)is extended conflict-free ifNis extended conflict-free.
Note that every net without forward branching places is extended free-choice [5]. The proof of our result is based on the notion of conflict order.
Definition5.2. LetNbe an extended free-choice net and letT be the set of transi- tions ofN. A conflict order≤⊆T×T is a partial order such that two transitionstand uare comparable (i.e.,t≤uoru≤t) if and only if they belong to the same conflict set. For elementsu,t∈T, the expressionu < tdenotes u≤tand u≠t. Letσ be a sequence of transitions ofN. A conflict order≤is said to agree withσ if, for every conflict setc, either no transition ofcoccurs inσ or the last transition ofcoccurring inσ is maximal, that is, the greatest transition ofcwith respect to≤.
We can now define, given an occurrence sequenceσ and a conflict order≤, the set of permutations ofσ which are ordered with respect to≤.
Definition5.3. LetNbe an extended free-choice net and let≤be a conflict order.
A sequenceτ is called sorted with respect to≤(or≤-sorted) if every two transitions t,usatisfyt < uandtdoes not occur afteruinτ.
Prefixes of sorted permutations of given sequenceσwill play a particular important role in the sequel [8,17]. We will need the following lemma.
Lemma5.4. Letσ be a sequence of transitions of an extended free-choice net and let≤be a conflict order. Let τ be a prefix of a≤-sorted permutation ofσ. Lett be a transition satisfying
(i) #(t,τ) <#(t,σ ),
(ii) #(u,τ)=#(u,σ )for every transitionusatisfyingu < t. Then, the sequenceτtis also a prefix ofa≤-sorted permutation ofσ.
Proof. Sinceτ is a prefix of a≤-sorted permutation ofσ, there exists a sequence psuch thatτp is a≤-sorted permutation ofσ. ByLemma 5.4(i),toccurs inp. Letp be the sequence obtained frompby deletion of the first occurrence oftinp. Then the sequenceτtpis again a permutation ofσ. It is sorted because byLemma 5.4(ii), no transitionusatisfyingu < toccurs inpandp.
We outline the proof of the result. Let(N,M0)be a live and safe extended free choice system, letM1be a reachable marking, and letM1 σ
→M2be an occurrence sequence.
We show that
(i) there exist a conflict order≤that agrees withσ and a≤-sorted permutationτ ofσ such that
M1 τ
→M2, (5.1)
(ii) τ=τ1,τ2,...,τk, whereτiis a biased sequence for everyi, andkis less than or equal to the number of transitions ofN.
Using (ii) and Theorem 3.4, we prove that there exists a sequence p1,p2,...,pk of bounded length. Of these two steps, (i) is more involved; (ii) follows easily from the definition of≤-sorted permutation. To prove (i), we make use of the well-known de- composition theorem of the theory of free-choice system. We recall both the definition ofS-component and the decomposition theorem.
Definition5.5. AnS-net is a net which does not satisfy| •t| = |t• | =1 for each transitiont. A system(N,M0)is anS-system ifNis anS-net [9].
Definition5.6. A strongly connectedS-net,N1, is anS-component of a netNif for every placesofN1the following hold:
(1) sis a place ofN;
(2) the preset ofsinN1equals the preset ofsinN; (3) the postset ofsinN1equals the postset ofsinN.
A netNis covered by a set of S-components{N1,...,Nn}if every place ofNis contained in somescomponentNiof this set.
Theorem5.7. Let(N,M0)be a live and safe extended free-choice system. ThenNis covered by a set ofs-components{N1,...,Nn}such that eachNihas exactly one place marked byM0(this place contains only one token because(N,M0)is safe).
It is first shown that (i) holds for s systems then usingTheorem 5.7 it is proved that it holds for live and safe extended free-choice systems. The meaning of (i) can be illustrated with an example. There existM1 σ
→M2for the sequence
σ=t2t4t3t1t2t5t1t2t4t2. (5.2) The conflict sets of the net are{t1},{t2,t3}, and{t4,t5}. The last transition of{t2,t3} occurring inσist2and the last transition of{t4,t5}occurring inσ ist4. Therefore, the only conflict order that agrees withσ is the one given byt3< t2andt5< t4.
Now, (i) asserts the existence of≤-sorted permutationτofσ such thatM1 τ→M2, that is, a permutation ofσ wheret3does not occur anymore after the first occurrence oft2and t5does not occur anymore after the first occurrence oft4. In this example, the permutation is unique, that is,
τ=t3t1t2t5t1t2t4t2t4t2. (5.3) The condition requiring the conflict order to agree withσ is essential for the result. In the authors’ example, no permutation ofσsorted with respect to a conflict order where t2< t3satisfiesM1 τ→M2, because every nonempty occurrence sequence leading toM2
must havet2as the last transition.
The rest of this section is organized as follows. We prove (i) forS-systems. Actually, we prove a stronger result inProposition 5.10. We prove (i) for live and safe extended free-choice systems inProposition 5.12. Finally, we obtain the desired upper bound in Theorem 5.13.
5.1.S-systems. The result we wish to prove has a strong graph-theoretical flavor, because the occurrence sequences of safeS-systems correspond to paths of thes-net, as we could observe in the example above. In fact, the main idea of our proof is taken from the proof of the BEST theorem in [9] of graph theory which gives the number of Eulerian trails of a directed graph. In [2, 9], it is cited as the original reference. The following lemma follows immediately from the definitions.
Lemma5.8. Let(N,M0)be anS-system and letM1be a reachable marking. Then
s∈S
M0(s)=
s∈S
M1(s), (5.4)
whereSis the set of places ofN.
Lemma5.9. Let(N,M0)be anS-system, letM1be a reachable marking, and letM1 σ→ M2be an occurrence sequence. Let≤be a conflict order which agrees withσ and letTm
be the set of maximal transitions (with respect to≤).
LetVm⊆Tmbe the set of maximal transitions occurring inσ. Then every circuit ofN containing only transition ofVmcontains some place marked atM2.
Proposition5.10. Let(N,M0)be anS-system, letM1be a reachable marking, and letM1→M3be an occurrence sequence. Let≤be a conflict order which agrees withσ. If a prefix of≤-sorted permutation ofσ is enabled atM1, then it can be extended to a
≤-sorted permutation ofσ which is also enabled atM1.
Proof. Letτ be a prefix of a≤-sorted permutation ofσ such thatM1 τ→M3for some markingM3. It suffices to prove that ifτ is not a permutation ofσ, then M3
enables some transitiontsuch that it is again a prefix of a≤-sorted permutation ofσ. The desired≤-sorted permutation can be constructed by repeatedly extendingτ.
SinceNis ans-net, a transition is enabled if the unique place in its preset is marked.
So it suffices to prove that there exists a places, marked atM3such that #(s•,τ) <
#(s•,σ ). Then byLemma 5.4, the least (with respect to≤) transitiont∈s•satisfying
#(t,τ) <#(t,σ )is a feasible extension ofτ, that is,τ is again a prefix of a≤-sorted permutation ofσ.
Assume that no such placesexists, that is, assume that every placessatisfies either M3(s)=0 or #(s•,τ)=#(s•,σ ). (5.5) We first claim thatM3=M2. ByLemma 5.8, bothM2andM3put the same number of tokens in the places ofN; so it suffices to prove thatM2(s)≥M3(s)for every places. Letsbe a place. IfM3(s) >0, then, by assumption,
#(s•,τ)=#(s•,σ ). (5.6)
So
M2(s)=M1(s)+#(•s,τ)−#(s•,σ ) (5.7) M3 σ→M2
≥M1(s)+#(•s,τ)−#(s•,σ ) (5.8) (τ is a prefix of a permutation ofσ )
=M1(•s)+#(•s,τ)−#(s•,τ) (5.9) (by assumption)
=M3(s) (5.10)
M1 τ→M3
,
which finishes the proof of the claim.
LetTmbe the maximal transitions with respect to≤. LetUbe the set of transitions tsatisfying #(t,τ) <#(t,σ )and letUm=U∩Tm.
Sinceτis not a permutation ofσ ,uis nonempty. We show thatUmis also nonempty.
Lettbe an arbitrary transition inUand lettmbe the maximal transition of the conflict set containingt. Since≤agrees withσ andtoccurs inσ, the transitiontmalso occurs inσ. Sinceτ is a prefix of a≤-sorted permutation ofσ and sincetbelongs toU,tm
belongs toU, too. Sotm∈Um, which implies thatUmis nonempty.
We next show that
Um• ⊆•Um. (5.11)
Letsbe a place ofUm•. We prove thats∈•Um. SinceM2=M3, we have
#(•s,σ )−#(s•,σ )=#(•s,τ)−#(s•,τ). (5.12)
Sinceτis a prefix of a permutation ofσ, we get
#(t,τ)≤#(t,σ ) (5.13)
for every transitiont. Moreover, #(•s,τ) <#(•s,σ )becauses∈Um• andUm• ⊆U•. So
#(s•,τ) <#(s•,σ ), that is, some transitiont∈s•belongs toU. In particular,toccurs in some transitiont∈sthat belongs tou. In particular,tand the maximal transition ins•, saytm, both occur inσ. Asτ is a prefix of a≤-sorted permutation ofσ, we get tm∈U. Therefore sincetmis maximal, it belongs toUm. Astm∈s•, we obtains∈•Um. SinceUmis nonempty and finite, and byUm• ⊆•Um, there exists a circuitCofNwhose transitions belong toUm. LetVmbe the set of maximal transitions occurring inσ. We haveUm⊆Vm, because all transitions ofUm are maximal and occur inσ. Therefore,
all the transitions ofcbelong toVm. We can now applyLemma 5.9to conclude thatc contains some placesmarked atM2. SinceM2=M3,sis also marked atM3. Moreover, sincec contains only transitions ofUm, some transition in the post-set of s belongs toUm. SinceUm⊆U, this contradicts the assumption that every place marked atM3
satisfies
#(s•,τ)=#(s•,σ ). (5.14)
5.2. Extended free-choice systems. Theorem 5.7suggests looking at extended free- choice systems as a set of sequential systems which communicate by means of shared transitions [14]. The following lemma states that the projection of an occurrence se- quence of the systems on one of itsS-components yields a local occurrence sequence of the component.
Lemma5.11. Let(N,M0)be a system. LetM1be a reachable marking and letM1 σ
→ M2be an occurrence sequence. LetNibe anS-component ofN. LetM1i(resp.,M2i) be the restriction of the markingM1(resp.,M2) to the places ofNi. Letσidenote the sequence obtained fromσ by deletion of all transitions which do not belong toNi; thenM1i
σi
→M2i
is an occurrence sequence ofNi. Using this lemma, it is now shown thatProposition 5.10 also holds for live and safe extended free-choice systems.
Proposition5.12. Let(N,M0)be a live and safe extended free-choice system. Let M1be a reachable marking and letM1 σ→M2be an occurrence sequence. Let≤be a conflict order which agrees withσ. If a prefix of a≤-sorted permutation ofσ is enabled atM1, then it can be extended to a≤-sorted permutation ofσ which is also enabled at M1.
Proof. ByTheorem 5.7,N is covered by a set{N1,...,Nn}ofS-components with exactly one place marked. In the sequel we call theseS-components state machines of Ni. LetNibe a state machine ofN. For each marking ofNwe defineMias the restriction ofMto the set of places ofNi. For a sequence of transitionsp1,pidenotes the sequence obtained frompby the deletion of all transitions which do not belong toNi. Letτbe a proper prefix of a≤-sorted permutation ofσ such thatM1 τ→M3for some making M3. LetUbe the set of transitionstsatisfying #(t,τ) <#(t,σ ), thenuis nonempty. We prove that there exists a transitiontofu, enabled atM3such thatτtis again a prefix of a≤-sorted permutation ofσ. As inProposition 5.10, the desired permutation can then be constructed by repeatedly extendingτ.
It suffices to prove thatM3enables some transition ofU. Ifu∈Uis enabled atM3, thenNis extended free-choice and every transition in the conflict set that containsu is enabled atM3. Then byLemma 5.4, the least (with respect to≤) transitiontin this conflict set that belongs toUis a feasible extension ofτ; that is,τtis again a prefix of a≤-sorted permutation ofσ.
We proceed indirectly and assume that no transition ofU is enabled atM3. Then, since(N,M0)is a live system andM3is a reachable marking, there exists anM3 p
→M nonempty occurrence sequence such thatM enables some transitionuofU. We can
assume thatpis a minimal sequence satisfying this property, that is, no intermediate marking enables a transition ofU.
By assumption,uis not enabled atM3, soM3(s)=0 for some placesin the preset of U. LetNibe a state machine ofNcontainings. By the definition of a state machine and byLemma 5.8, only one place ofNiis marked atM3i; letrbe this place. ByLemma 5.11, M1i
σi
→M2i are occurrence sequences ofNi. Let≤ibe the restriction of≤to pairs of transition ofNi. Then≤i agrees withσibecause every conflict set ofNiis a conflict set ofN, by the definition of anS-component. Moreover,τiis a prefix of a≤i-ordered permutation ofσi, hence byProposition 5.10we have M1i
τi
→M2i for a sequenceτ such thatτiτiis a≤-sorted permutation ofσifor every transition ofNithat belongs toU. Sinceu∈U,uoccurs inτi. In particular,τiis not empty. Let the first(τi)be the first transition ofτi. Sincer is the unique place ofNimarked atM3i, we have the first(τi)∈r•. Again byLemma 5.11 M1i
σi
→M2i and the sequencepcontains some transition in•s. Since all transitions in•sbelong toNi,pcontains some transition of Ni. Sopiis nonempty. Let the first(pi)be the first transition ofpi. Again, sincer is the unique place ofNimarked atM3, we have the first(pi)∈r•.
So the first(τi)and first(pi)belong to the same conflict setr•. By the extended free-choice property, a marking enables the first(pi)if and only if it enables the first (τi). Since the first (pi)occurs in p, it becomes enabled after the occurrence of a proper prefix ofp. So first (τi) becomes enabled after the occurrence of the same proper prefix ofpas well. But the first(τi)is a transition ofu, which contradicts our hypothesis about the sequencep. This proves that some transition ofUis enabled at M3and we are done.
5.3. An upper bound on the length of shortest paths. We are finally ready to prove the following result.
Theorem 5.13. Let(N,M0)be a live and safe extended free-choice system where N=(S,T ,F) and letM2be a marking reachable fromM1. There exists an occurrence sequenceM1 τ→M2such that the length ofτis at most|T|·|T+1|·|T+2|/6.
Proof. SinceM2is reachable fromM1, there exists an occurrence sequenceM1 σ→ M2. Let≤be an arbitrary conflict order that agrees withσ. ByProposition 5.12(taking the empty sequence forτ), there is a≤-sorted permutationpofσ such thatM1 p
→M2. Letkbe the number of distinct transitions, thenk≤ |T|. We show that there exists an occurrence sequenceM1 τ→M2such that the length ofτis at mostk·(k+1)·(k+2)/6.
We proceed by induction onk. Base. Fork=0, takeτ=ε.
Step. Fork >0, letp1be the maximal prefix ofpthat contains at most one transition of each conflict setp1is biased. Letp=p1p2andM1 p1→M2 p2→M3. ByTheorem 3.4, there is an occurrence sequence M1
τ1
→ M3 such that the length of τ1 is at most k·(k+1)/2. IfM3=M2, then we are finished, because
k·(k+1)
2 ≤k·(k+1)·(k+2)
6 . (5.15)
Now assume thatM3≠M2, thenp2is nonempty. Lettbe its first transition. Sincep1
is maximal, thereforep1 contains a transitionuin the conflict set oft. Since pis a
≤-sorted permutation, u < t, and udoes not occur inp2, so the number of distinct transitions occurring inp2is at mostk−1. By the induction hypothesis, there exists an occurrence sequenceM3 τ2
→M2such that the length ofτ2is at most k·(k−1)·(k+1)
6 . (5.16)
Defineτ=τ1τ2, thenM1 τ
→M2and the length ofτ is at most k·(k+1)
2 +k·(k−1)·(k+1)
6 =k·(k+1)·(k+2)
6 . (5.17)
6. A family of systems with exponential shortest paths. It can be easily shown that a family of systems for which there exists a family no polynomial upper bound in the length of the shortest paths. All the systems of the family are live and safe.
They are even persistent; that is, a transition can only cease to be enabled by its own occurrence. The shortest path is the set{s1,s3,s5,s7,...,s4n−3,s4n−1}having increments of exponential nature in the number of transitions of the net. This can be easily proved by showing that in order to reach this marking, transitiont2n−1has to occur at least once and for every 1≤i < n, transitiont2i−1has to occur one time more than twice as often as transitiont2i+1.
7. Conclusions. We have obtained polynomial bounds for the length of the shortest paths connection of two given markings for three classes of net systems: safe conflict- free systems, safe marked graphs, and live and safe extended free-choice systems. Fur- thermore, we have shown that in the case of safe conflict-free systems and safe marked graphs, the bound is reachable and that the length of the shortest paths in safe per- sistent systems can be exponential in the number of transitions. In the proofs we have made strong use of results of Yen [19] on conflict-free systems and of graph-theoretical results on Eulerian trails. Using the first result (1.1) of this paper, it has been proved that the model checker described there has polynomial complexity in the size of the system for safe conflict-free systems. The third result (1.3) proves that the reachabil- ity problem for live and safe extended free-choice systems belongs to the classNP. Although we believe that this problem is solvable in polynomial time, membership in NP is the best upper bound obtained so far. Also, we do not know at the moment if the bound for live and safe free-choice systems is reachable. In fact, we believe that a reachable bound should be quadratic in the number of transitions.
Acknowledgements. The author thanks anonymous referees for several helpful comments and suggestions. The author is also thankful to Professor H. C. Pande, Vice- Chancellor Emeritus, Professor S. K. Mukherjee, Vice-Chancellor, and Professor N. C.
Mahanti, Professor and Head of the Department of Applied Mathematics, Birla Institute of Technology, Mesra, for encouragement and support.
References
[1] T. V. Ardenne-Ehrenfest and N. G. De Bruijn,Circuits and trees in oriented linear graphs, Simon Stevin28(1951), 203–217.
[2] E. Best and J. Desel,Partial order behaviour and structure of Petri nets, Formal Aspects Compute.2(1990), no. 2, 123–138.
[3] E. Best and J. Esparza,Model checking of persistent Petri nets, 5th Workshop Computer Science Logic, Lecture Notes in Computer Science, vol. 626, Springer-Verlag, Berlin, 1992, pp. 35–52.
[4] E. Best and P. S. Thiagarajan,Some classes of live and safe Petri nets, Concurrency and Nets, Springer, Berlin, 1987, pp. 71–94.
[5] E. Best and K. Voss,Free choice systems have home states, Acta Inform.21(1984), no. 1, 89–100.
[6] F. Commoner, A. W. Holt, S. Even, and A. Pnueli,Marked directed graphs, J. Comput. System Sci.5(1971), 511–523.
[7] J. Esparza,A solution to the covering problem for1-bounded conflict-free Petri nets using linear programming, Inform. Process. Lett.41(1992), no. 6, 313–319.
[8] ,Model checking using net unfoldings, TAPSOFT ’93: Theory and Practice of Software Development (Orsay, 1993), Lecture Notes in Comput. Sci., vol. 668, Springer, Berlin, 1993, pp. 613–628.
[9] H. Fleischner,Eulerian Graphs and Related Topics. Vol. 1, Annals of Discrete Mathematics, vol. 45, North-Holland Publishing, Amsterdam, 1990.
[10] H. J. Genrich and K. Lautenbach,Synchronisationsgraphen, Acta Informat.2(1973), 143–
161 (German).
[11] M. Hack,Analysis of production schemata by petrinets, Tech. Report 94, MIT-MAC, 1972, Corrections, 1974.
[12] R. Howell and L. Rosier,Completeness results for conflict-free vector replacement systems, J. Comput. System Sci.37(1988), no. 3, 349–366.
[13] ,Problems concerning fairness and temporal logic for conflict-free Petri nets, Theoret.
Comput. Sci.64(1989), no. 3, 305–329.
[14] L. H. Landweber and E. L. Robertson,Properties of conflict-free and persistent Petri nets, J.
Assoc. Comput. Mach.25(1978), no. 3, 352–364.
[15] K. L. Mcmillan,Using unfoldings to avoid the state explosion problem in the verification of asynchronous circuits, 4th Workshop Computer Science Logic, Springer, London, 1991, pp. 164–174.
[16] P. K. Mishra,A study of the data structure and algorithm analysis in C-programming lan- guage, M. Phil, APS University, Rewa India, 1995.
[17] P. K. Mishra and C. K. Sharma,A computational study of an efficient shortest path algorithms in C-programming language, 5th International Conference on Application of HPC in Engineering, WIT Press, Spain, 1997, pp. 85–90.
[18] P. S. Thiagarajan and K. Voss,A fresh look at free choice nets, Inform. and Control61 (1984), no. 2, 85–113.
[19] H. C. Yen,A polynomial time algorithm to decide pairwise concurrency of transitions for 1-bounded conflict-free Petri nets, Inform. Process. Lett.38(1991), no. 2, 71–76.
[20] H. C. Yen, B. Y. Wang, and M. S. Yang,A unified approach for reasoning about conflict-free Petrinets, Application and Theory of Petri Nets 1993, Lecture Notes in Comput. Sci., vol. 691, Springer, Berlin, 1993, pp. 513–531.
P. K. Mishra: Department of Applied Mathematics, Birla Institute of Technology, Mesra 835215, Ranchi, India
E-mail address:[email protected]; [email protected]
