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
(#>
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 (#>
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:
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. (#>