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 (#>
.
Choose an arbitrary state 
.
with
, an immediate transition is enabled, because
of our initial assumption that a timeless trap 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.
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:
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 
.
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
(#>
=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