Next: Home states Up: Efficient qualitative analysis Previous: Boundedness


Liveness of the (C)PN need not carry over to the timed net [7][6][5]. Formulating restrictions on the incorporation of timing aspects for general QPNs is difficult, but we can establish such conditions, if we restrict the structure of the CPN to EFC-nets for which liveness can be determined very efficiently by examinating the deadlock/trap-property [12].

For liveness of an EFC-QPN, whose underlying CPN is live, obviously immediate and timed transitions must not be in conflict. Furthermore we have to ensure that all tokens in a queueing place have the opportunity of being served independently of each other. Otherwise also very simple QPNs need not be live. Fig. 7 depicts such a situation. is a timed queueing place, whose queue service tokens according to a 'last come first served preemptive resume' scheduling discipline. Since firing of immediate transitions has priority on scheduling in timed queueing places, a token being served at immediately returns to this place thus preempting service of the other token. So either token or will never leave this queue. The following conditions exclude such situations.

Part (10) of condition EQUAL-Service together with (#>) guarantees that already served tokens are not rescheduled. Before establishing the main result of this subsection we need the following

Proof: Assume there is a timeless trap, i.e.
The set is a closed subset of states being reachable from . Since is finite, is non-empty.

First of all we will show, that there is a state in in which an immediate transition is enabled, i.e. . Assume the contrary. From liveness of the CPN and (#>) it follows that . Choose an arbitrary state .

If there is no with , an immediate transition is enabled, because of our initial assumption that a timeless trap exists.
Otherwise there exists with and since satisfies condition EQUAL-Service the process will eventually reach a state where . This argumentation can be applied successively to all with . Thus a state will be reached where . In analogy to (1st) the enabling of an immediate transition is guaranteed.

Since is a closed subset of states all these immediate transitions are live with regard to . Let be the set of such live immediate transitions with regard to colours and the corresponding complementary set. is non-empty, because of .

Boundedness and liveness of the CPN yield that the unfolded CPN consists of P/T-nets which are by themselves strongly connected (cf. [9]). Note that unfolding of a CPN might result in several isolated P/T-nets. E.g. unfolding the CPN given in Fig. 7 yields two (strongly connected) P/T-nets. Define the set of input places of enabled transitions in with regard to the corresponding colours and .

Due to strongly connectedness one of the following two cases must hold:


ad a)
The definition of implies the existence of . Condition EQUAL-Conflict together with the EFC-net structure ensures that for and also transition is enabled with regard to whenever is enabled with regard to . Thus contradicting .
ad b)
Since tokens of colour are not removed by firing of an immediate transition for some . For and , tokens of colour will pile up at place . Since all queueing places keep track of the token count according to (#>) the QPN is not bounded contradicting the boundedness of the underlying CPN (cf. Theorem 3). =0

Proof: For abbreviation some of the definitions given in the proof of Lemma 1 will be used here.

Assume the QPN is not live. According to Theorem 3 is finite. Choose an arbitrary strongly connected subset with . This is always possible, since the is assumed to be not live. Note that might also comprises tangible states in this context.

The EFC-net structure yields and is not marked with any token of colour in all states of , i.e. :

Otherwise, because conditions EQUAL-Service and EQUAL-Conflict are satisfied, will eventually be enabled according to colour , since the QPN has no timeless trap (cf. Lemma 1). Thus . Extending the -operator to CPNs via unfolding we get and implying . Since all queues keep track of the token number (cf. (#>)), represents an unmarked deadlock of the CPN contradicting its liveness (cf. Theorem 4). =0pt=0

Next: Home states Up: Efficient qualitative analysis Previous: Boundedness

Tue Jan 9 09:36:45 MET 1996