This paper deals with model checking of timed systems modeled by Time Petri nets (TPN). We propose a new finite graph, called Timed Aggregate Graph (TAG), abstracting the behavior of bounded TPNs with strong time semantics. The main feature of this abstract representation compared to existing approaches is the encoding of the time information. This is done in a pure way within each node of the TAG allowing to compute the minimum and maximum elapsed time in every path of the graph. The TAG preserves runs and reachable states of the corresponding TPN and allows for on-the-fly verification of reachability properties. We illustrate in this paper how the TAG can be used to check some usual timed reachability properties and we supply an algorithm for extracting an explicit timed trace (involving the elapsed time before each fired transition) from an abstract run of the TAG. The TAG-based approach is implemented and compared to two well known TPNs analysis approaches.
Time Petri nets are one of the most used formal models for the specification
and the verification of systems involving explicit timing constraints, such as
communication protocols, circuits, or real-time systems. The main extensions of
Petri nets with time are time Petri nets [
For real-time systems, dense time model (where time is considered in the
domain R 0) is the unique possible option, raising the problem of handling
an infinite number of states. In fact, the set of reachable states of the TPN is
generally infinite due to the infinite number of time successors a given state could
have. Two main approaches are used to treat this state space: region graphs [
In this work, we propose a new finite graph, called Timed Aggregate Graph
(TAG), abstracting the behavior of bounded TPNs with strong time semantics.
A preliminary version of this work has been published in [
This paper is organized as follows: In Section 2, some preliminaries about
TPNs and the corresponding semantics are recalled. In Section 3, we define the
Timed Aggregate Graph (TAG) associated with a TPN and we discuss the main
preservation results of the TAG-based approach. In Section 4, we show how the
verification of some usual reachability properties can be accomplished
on-thefly by exploring the TAG. Section 5 relates our work to existing approaches. In
Section 6, we discuss the experimental results obtained with our implementation
compared to two well-known tools, namely Romeo [
A TPN is a P/T Petri net [
Definition 1. A TPN is a tuple N = hP, T, Pre, Post , Ii where: – hP, T, Pre, Post i is a P/T Petri net – I : T ! N ⇥ (N [ { +1} ) is the time interval function such that: I(t) = (tmin, tmax), with tmin tmax, where tmin (resp. tmax) is the earliest (resp. latest) firing time of transition t.
A marking of a TPN is a function m : P ! N where m(p), for a place p, denotes
the number of tokens in p. A marked TPN is a pair N = hN1, m0i where N1 is
a TPN and m0 is a corresponding initial marking. A transition t is enabled by
a marking m iff m Pre(t) and Enable(m) = {t 2 T : m Pre(t)} denotes the
set of enabled transitions in m. If a transition ti is enabled by a marking m, then
" (m, ti) denotes the set of newly enabled transitions [
The semantics of TPNs can be given in terms of Timed Transition Systems
(TTS) [
Definition 2 (Semantics of a TPN). Let N = hP, T, Pre, Post , I, m0i be a marked TPN. The semantics of N is a TTS SN = hQ, s0, !i where: 1. Q is a (possibly infinite) set of states 2. s0 = (m0, V0) is the initial state such that: 8 t 2 T, V0(t) =
? ⇢ 0 if t 2 Enable(m0) otherwise 3. ! ✓
Q ⇥ (T [ R 0) ⇥ Q is the discrete and continuous transition relations: (a) the discrete transition relation:
8 t 2 T : (m, V !) t (m0, V 0) iff: (b) the continuous transition relation: 8 d 2 R 0, (m, V !) d (m0, V 0) iff: >>><>8 ttm2inE naVbl(et() m) t^mma8<x0 0= m if t0 2 "(m, t) >>>> 8 t0 2 T : V 0(t0) = V (t0) if t0 2 #(m, t) : otherwise : ?
Pre(t) + Post (t) >8 8 t 2 Enable(m), V (t) + d tmax >>>< m0 = m
8 t 2 T : >>>>: V 0(t) = ⇢ V (t) + d if t 2 Enable(m);
V (t) otherwise.
The above definition requires some comments. First, a state change occurs either by the firing of transitions or by time elapsing: The firing of a transition may change the current marking while the time elapsing may make some new transitions fireable. Second, the delay transitions respect the STS semantics: an enabled transition must fire within its firing interval unless it is disabled by the firing an other transition.
Given a TPN N and the corresponding TTS SN , a path ⇡ = s0! ↵ 1 s1! ↵ 2 . . . , where ↵ i 2 (T [ R 0), is a run of SN iff (si, ↵ i, si+1) 2! for each i = 0, 1, . . . . The length of a run ⇡ can be infinite and is denoted by | ⇡ |. The possibly infinite set of runs of SN is denoted [SN ]. Without loss of generality, we assume that for each non empty run ⇡ = s0! ↵ 1 s1! ↵ 2 . . . of a STS corresponding to a TPN, there do not exist two successive labels ↵ i and ↵ i+1 belonging both to R 0. Then, ⇡ can be written, involving the reachable markings of N , as ⇡ = m0(!d1,t1)m1(!d2,t2) . . . where di is the time elapsed at marking mi 1 before firing ti. In order to associate a run ⇡ of SN with a run of N , denoted P(⇡ ), we define the following projection function, where ⇧ denotes the concatenation operator between paths and ⇡ i, for i = 0, 1 . . . , denotes the suffix of ⇡ starting at state si.
P(⇡ ) = 8 s0.m ><>> s0.m(!0,↵ 1) ⇧ P(⇡ 1) if ↵ 1 2 T
if | ⇡ |= 0 >>:> ss00..mm!(↵↵!11,↵ ⇧2P)⇧(P⇡1()⇡ 2) iiff ↵↵ 11 22 RR 00^^ || ⇡⇡ ||= 21 3 3.1
Timed Aggregate Graph In this subsection, we propose to abstract the reachability state space of a TPN using a new graph called Timed Aggregate Graph (TAG) where nodes are called aggregates and are grouping sets of states of a TTS. The key idea behind TAGs is the way the time information is encoded inside aggregates. In addition to the marking characterizing an aggregate, the time information is composed of two parts: – The first part of the time information characterizing an aggregate is a dynamically updated interval, namely (↵ t, t), associated with each enabled transition t. This interval gives the earliest and the latest firing times of any enabled transition starting from the corresponding aggregate. Either the corresponding transition is fireable at the current aggregate and the system must remain within the aggregate at least ↵ t time units and at most t time units (as long as the other enabled transitions remain fireable) before firing t, or t is not possible from the current aggregate (e.g. because of some diagonal constraint), and the system must move to an other aggregate by firing other transitions until t becomes fireable. In the latter case, the system must consume at least ↵ t, and can consume at most t to make t fireable in the future. – The second part of the time information characterizing an aggregate is a matrix, namely M eet, allowing to dynamically maintain the relative differences between the firing times of enabled transitions (diagonal constraints). Given two enabled transitions t1 and t2, M eet(t1, t2) is an interval representing the earliest and the latest firing times of t1 the last time both t1 and t2 were enabled (through the paths leading to the aggregate).
Before we formally define the TAG and illustrate how the attributes of an aggregate are computed dynamically, let us first formally define aggregates. Definition 3 (Timed Aggregate). Let N = hP, T, P re, P ost, Ii be a TPN. A timed aggregate associated with N is a tuple a = (m, E, M eet), where: – m is a marking – E = {ht, ↵ t, ti | t 2 Enable(m), ↵ t 2 N ^ t 2 N [ { +1}} is a set of enabled transitions each asssociated with two time values. – Meet is a matrix s.t. 8 t, t0 2 Enable(m), M eet(t, t0) = h↵, i where ↵ (resp.
) represents the earliest (resp. latest) firing time of t the last time t and t0 are both enabled before reaching the aggregate a.
As for the states of a TTS, the attributes of an aggregate a are denoted by a.m, a.E and a.M eet. Moreover, a.M eet(t, t0).↵ (resp. a.M eet(t, t0). ) is denoted by a.↵ tm(t,t0) (resp. a. tm(t,t0)), or simply ↵ tm(t,t0) (resp. tm(t,t0)) when the corresponding aggregate is clear from the context. We use also ↵ m(t,t0) (resp.
m(t,t0)) to denote ↵ tm(t,t0) (resp. tm(t,t0)) when the involved transition t is clear from the context.
The E attribute of an aggregate a allows to compute the minimum and the maximum time the system can elapse when its current state is within a. The following predicates ( and ) compute these information for a given aggregate. Definition 4 (Minimum and maximum stay times). Let a = hm, Ei be an aggregate, the minimum and maximum time the system can stay at a are denoted by (a) and (a) respectively, and are defined by the two following predicates: – (a) = minht,↵ t, ti2 E (↵ t) – (a) = maxht,↵ t, ti2 E ( t) The minimum (resp. maximum) stay time (a) (res. (a)) of an aggregate a allows to encapsulate the continuous transition relation within a.
Given an aggregate a = hm, Ei and an enabled transition t (i.e., ht, ↵ t, ti 2 E), two primordial issues must be achieved to define the semantics of the TAG: (1) is t fireable from a?, and (2) if it is the case, how do we obtain the successor aggregate by firing t from a. In the following, we answer these issues. Definition 5. Let a = hm, E, M eeti be an aggregate and let ht, ↵ t, ti 2 E. m(t0,t) t0 Then, t is fireable at a, denoted by a t , iff 8h t0, ↵ t0 , t0 i 2 E, ↵ tm(t,t0) A transition t is fireable at an aggregate a iff there is no transition t0, that is enabled by a, whose latest firing time was strictly smaller than the earliest firing time of t the last time both transitions were enabled.
Now that the firability condition is formally defined, the following definition computes the successor aggregate obtained by the firing of a given transition. In this definition, the notion of newly (and oldly) enabled transitions is extended to aggregates as follows: " (a, t) =" (a.m, t) and # (a, t) =# (a.m, t) for each transition t enabled by a.m Definition 6. Let a = hm, E, M eeti be an aggregate and let ht, ↵ t, ti 2 E.
Assume that t is fireable at a (following Definition 5). The aggregate a0 = hm0, E0, M eet0i obtained by firing t from a, denoted by a t a0, is obtained as follows: 1. m0 = m Pre(t) + Post (t) 2. E0 = E10 [ E20, where: • E10 = S • E20 = St02" (a,t){ht0, t0min, t0maxi}
t02# (a,t){ht0, ↵ t00 , t00 i} where: – ↵ t00 = ↵ t0 SCR(a, t0), where SCR(a, t0) = – t00 = t0 • 8 (ht1, ↵ 1, 1i, ht2, ↵ 2, 2i) 2 E0 ⇥ E0
M ax(0, (↵ tm(t,t0) ( tm0 (t0,t) t0 )) M ax(0, (M int002 Enable(a)(M in( m(t0,t00), m(t00,t0)) (↵ tm0 (t0,t00) ↵ t0 )) M eet0(t1, t2) = <8 [t1min , t1max ] if t1 2" (a, t)
[↵ 1, 1] if t1 2#(a, t) ^ t2 2" (a, t) : M eet(t1, t2) if t1 2#(a, t) ^ t2 2#(a, t).
The computation of a successor a0 of an aggregate a by the firing of a transition t is guided by the following intuition: If #(a, t) 6= ; , then the more the system can remain at a, the less it can remain at a0 and vice versa. Otherwise, the time elapsed within a0 is independent from the time elapsed within a. Thus, given a transition t0 enabled by a0, two cases are considered: if t0 is newly enabled, then its earliest and latest firing times are statically obtained by t0min and t0max respectively. Otherwise, the more one can remain at a, the less will be the necessary wait time at a0 before firing t0. The function SCR (Still Can Remain) allows to compute the maximum remaining time at a under the hypothesis that, since t0 became enabled, it remains the maximum time at each encountered aggregate before reaching a (note that this is different from (a)). Thus SCR(a, t0) is obtained by the following reasoning: given a transition t00 that is enabled by a, it is clear that since the last time t0 and t00 became both enabled, the maximum elapsed time can not be greater than M in( m(t0,t00), m(t00,t0)) (because of the STS semantics which is used in this paper). The maximum time the system can remain at a is then obtained by subtracting from this quantity the time that is already spent during the path leading to a (i.e., (↵ tm0 (t0,t00) ↵ t0 )). By analyzing all the transitions enabled by a the function SCR takes the minimum values in order to not violate the STS semantics rule. Similarly, the latest firing time of t0 corresponds to the situation where, between the last time t and t0 were both enabled and the current aggregate a, each fired transition is fired as soon as possible. Each time a transition is fired, its earliest firing time is subtracted from the latest firing time of the old transitions. However, if the quantity of time that must be subtracted from the latest firing time of t0 has already been subtracted in between, then the latest firing time of t0 at a0 is the same latest firing time of t0 at the aggregate a.
Concerning the M eet attribute, given two transitions t1 and t2 that are enabled at a0, the value of M eet(t1, t2) is simply obtained by considering the membership of these transitions to " (a, t) and to #(a, t). Finally, by considering that 1 1 = 0, the previous definition allows to handle transitions having an unbounded latest firing time.
p1 p2 p1 p2 p1 p2 p3 t1[1; 2] t2[1; 1] t1[0; 1] t2[2; 3]
t1[1; 1] t2[2; 2] t3[1; 1] p1
p2 t1[1; 2] t2[2; 1 ]
Fig. 1. Four TPN Examples
Now, we are ready to formally define the TAG associated with a marked TPN N . It is a labeled transition system where nodes are timed aggregates. It has an initial aggregate, a set of actions (the set of transitions of N ) and a transition relation. The initial aggregate is easily computed by considering static information of the TPN while the transition relation is directly obtained by Definition 5 and Definition 6.
Definition 7 (Timed Aggregate Graph). Let N = hP, T, Pre, Post , I, m0i be a TPN. The TAG associated with N is a tuple G = hA, T, a0, i where: 1. A is a set of timed aggregates; 2. a0 = hm0, h0i is the initial timed aggregate s.t.: (a) m0 is the initial marking of N . (b) E0 = {ht, tmin, tmaxi | t 2 Enable(m0 )} (c) 8 t, t 2 Enable(a), M eet(t, t0) = [tmin, tmax] 3. ✓ A ⇥ T ⇥ A is the transition relation such that: 8 a 2 A, 8 t 2 T , (a, t, a0) 2 iff a t a0
Since each transition having an unbounded static latest firing time will always maintain the same latest firing time at each aggregate where it is enabled, one can prove that the number of aggregates of a TAG is bounded when the corresponding TPN is bounded. Indeed, given a reachable marking m, the number of different aggregates having m as marking can be bounded by the number of possible values of its attributes. This number is finite because of the following facts: (1) if the number of the transitions that are enabled by m is e, there are 2|e| possible subsets of old transitions; (2) for a given subset of old transitions o, the number of possible arrangements of the old transitions regarding the enabling time is at most equal to | o |! (the 2n elements corresponding to the orderings where two or more old transitions became enabled at the same time are not considered); (3) given an arrangement t1 t2 · · · t|o|, the number of possible values of ↵ tm1(t1,t2) is at most equel to Pit=1m0in (t1max i + 1). Similarly, the possible values of ↵ tm2(t2,t3) is equal to Pit=2m0in (t2max i + 1), etc. Thus, the number of the possible different values of the matrix M eet, for this particular arrangement, is obtained by ⇧ j|o=|2 Pit=j01min (tj 1max i + 1); (4) for each enabled transition t (with tmax 6= 1 ), there are at most Pit=mi0n (tmax i + 1) different intervals that can represent the earliest and latest firing times associated with t in a given aggregate (i.e., ↵ t and t). When tmax = 1 , the number of possible time intervals associated with t is tmin + 1.
Figure 2 illustrates the TAGs corresponding to the TPNs of Figure 1. In the three first TAGs, the marking associated with each aggregate is omitted (it is the same as the initial one). The second column of the tables gives the dynamic earliest and latest firing times of the enabled transitions (i.e., t1, t2 and t3 respectively). For sake of readability of the figures, the M eet attribute is omitted.
Although the four models of Figure 1 are quite simple, they are representative enough to explain the TAG construction. Indeed, in the first one the transitions intervals overlap, while the case of disjoint intervals is considered through the second and the third models. Finally, the fourth model illustrates the case of an unbounded latest firing time. More significant examples are considered in Section 6.
aggregate E aaaaa32410 {{{{{hhhhh10011,,,,,22122iiiii,,,,,hhhhh01101,,,,,11101iiiii}}}}} a5 {h0,0i,h1,1i} aggraaaaaaaaae436521870gate {{{{{{{{{hhhhhhhhh010101101,,,,,,,,,010101101iiiiiiiii,,,,,,,,}hhhhhhhh,20202012hE,,,,,,,,120202012,iiiiiiii1,,,,,,,,ihhhhhhhh,11010011h,,,,,,,,111010011,iiiiiiii1}}}}}}}}i t2a5 a9 {h1,1i,h1,1i,h0,0i} t1 a1 a0 a3 In this section, we establish the main result of our approach: The TAG is an exact representation of the reachability state space of a TPN. In fact, for each path in the TPN (resp. in the corresponding TAG) it is possible to find a path in the TAG (resp. TPN) involving the same sequence of transitions and where the time elapsed within a given state is between the minimum and the maximum stay time of the corresponding aggregate. 1 . . . n+1, 9 ⇡ = a0! t1 a1! . . .! tn an s.t. 8 i = 0 . . . n, di+1 and 8 i = 1 . . . n, di ↵ i 1ti .
Theorem 1. Let N be a TPN and let G = hA, T, a0, i be the TAG associated with N . Then 8 ⇡ = m0(!d1,t1)m1(!d2,t2) . . . (!dn,tn)mn!dn+1, with di 2 R 0, for i = (ai), mi = ai.m Proof. Let ⇡ = m0(!d1,t1)m1(!d2,t2) . . . (!dn,tn)mn!dn+1 be a path of N , with di 2 R 0, for i = 1 . . . n + 1. Given a path a0! a1 . . . , we denote by ↵ it (res. it ), for i = 0 . . . , the dynamic earliest firing time (resp. latest firing time) of a transition t enabled by an aggregate ai.
Let us prove by induction on the length of ⇡ the existence of a path ⇡ in the TAG satisfying the conditions of Theorem 1.
– | ⇡ |= 0: Obvious since m0 = a0.m (by construction) and since d1 is less or equal to mint2 Enable(m0) tmax which is exactly the value of (a0). – | ⇡ |= 1 i.e., ⇡ = m0(!d1,t1)m1! d2 . It is clear that ↵ 0t1 d1 (a0). The fact that t1 is fireable at m0 implies that it is at a0 (8 t 2 Enable(m0), t1min tmax) and its firing leads to the aggregate a1 satisfying a1.m = m1. Let us assume that d2 > (a1) and let tm be the transition that is enabled at a1 and which has the smallest latest firing time i.e., 1tm = (a1). If tm is newly enabled at a1 then d2 should clearly be greater or equal to (a1). If tm 2#(a0, t1) then 1tm = tmmax t1min . Since d1 t1min , then tmmax t1min tmmax d1. The fact that d2 > 1tm would imply that d1 + d2 > tmmax which is contradictory with the STS semantics. Thus d2 (a1). – Assume that for any path ⇡ s.t. | ⇡ | n, there exists a path in the TAG with the same trace and satisfying the above conditions. Let ⇡ = m0(!d1,t1)m1(!d2,t2) . . . (!dn,tn)mn(dn!+1,tn+1)mn+1!dn+2 be a path of length n + 1. Let ⇡ = a0! t1 a1! t2 . . .! tn an be the path in the TAG associated with the n-length prefix of ⇡ (by the induction hypothesis). Then dn+1 (an). Let us demonstrate that dn+1 ↵ nn+1 : It is clear that this is the case when tn+1 2" (an, tn+1. If tn+1 2#(an, tn+1, let LastN ewi(t) be the function that returns the greatest integer, smaller than (or equal to) i, such that t 2" (al 1, tl). If such a value does not exist, then t became enabled, for the last time, at the initial aggregate a0 and the function returns 0. Let k = LastN ewi(tn+1), then ↵ nn+1 = tn+1min Pin=k1 SCR(ai, tn+1). The STS semantics implies that Pin=k1 SCR(ai, tn+1) Pin=k1 di+1 Thus tn+1min Pin=k1 SCR(ai, tn+1) tn+1min Pin=k1 di+1, and dn+1 > ↵ ntn+1 would means that Pin=k di+1 < tn+1min which would prevent the firing of tn+1 at mn. Thus, dn+1 ↵ ntn+1 . Let us show now that tn+1 is fireable at an. Assume the opposite, this would imply that there exists a transition t enabled by an such that ↵ m(tn+1,t) > m(t,tn+1). Let LastN ewn(tn+1) = l, LastN ewn(t) = k, and let us consider the three following cases: 1. l = k, then m(t,tn+1) = tmax and ↵ m(tn+1,t) = tnmin and the fact that tnmin > tmax would prevent tn+1 from being fireable at mn which is not the case. Thus, tn+1 is fireable at an as well. 2. l < k. In this case, ↵ m(tn+1,t) = tn+1min Pjk=l1 SCR(aj, tn+1) and m(t,tn+1) = tmax. Again, the STS semantics implies that Pik=l1 SCR(ai, tn+1) Pik=l1 di+1. Thus, tn+1min Pik=l1 SCR(ai, tn+1) tn+1min Pik=l1 di+1, and ↵ m(tn+1,t) > tmax would means that Pik=l di+1 < tn+1min which would prevent the firing of tn+1 at mn. Thus, ↵ m(tn+1,t) and tn+1 is necessarily fireable at an. 3. l > k. In this case, ↵ m(tn+1,t) = tn+1min and m(t,tn+1) = tmax Pli=1k M ax(0, (↵ m(ti+1,t) ( m(t,ti+1) it )). Knowing that Pli=1k M ax(0, (↵ m(ti+1,t) ( m(t,ti+1) it )) Pli=1k di+1 (otherwise, the time spent between k and some i l is smaller than ↵ m(ti,t), which is contradictory with the recurrence hypothesis), tmax Pli=1k M ax(0, (↵ m(ti+1,t) ( m(t,ti+1) Pli=1k di+1. Thus, if tn+1min > m(t,tn+1) it )) tmax then tn+1min > tmax Pli=1k di+1 which prevent the firing of tn+1 at mn (before firing t) which is not true. Thus, tn+1 is fireable at an.
Let us now demonstrate that dn+2 (an+1). Assume the opposite, and let tm be the transition enabled by an+1 which has the smallest latest firing time i.e. n+1tm = (an+1). It is clear that if tm 2" (an, tn+1) then dn+2 (an+1). Otherwise,Pifntm 2# (an, tn+1) and i=k M ax(0, (↵ m(ti+1,tm) k = LastN ewn+1(tm) then Pn+in1=tkmM=atxm(m0,a(x↵ m(ti+1,tm), then Again, since Pin=k di+1 n+1tm tmmax Pn n+1tm would imply that dn+2 + Pin=i=kkddi+i+11>,atnmdmtahxewfhacicththisatnodtn+al1lo>wed by the STS semantics. m(t,tn+1) Thus, dn+2
(an+1).
Theorem 2. Let N be a TPN and let G = hA, T, a0, i be the TAG associated with N . Then, for any path ⇡ = a0! t1 a1! . . .! tn an in the TAG, there exists a run ⇡ = m0(!d1,t1)m1! . . . (!dn,tn)mn in N , s.t. 8 i = 0 . . . n, mi = ai.m, 8 i = 1 . . . n, ↵ i 1ti ) di (ai 1), and 8 d 2 R 0, mn! d , d (an) Proof. Let ⇡ = a0! t1 a1! . . .! tn an. We denote by ↵ it (res. it ) the dynamic earliest firing time (resp. the dynamic latest firing time) of a transition t at aggregate ai, for i 2 {0, . . . , n 1}. Let us demonstrate that the path ⇡ = m0(!d1,t1)m1! . . . (!dn,tn)mn obtained by the following algorithm satisfies the requirement. The function LastN ewi(t) returns the greatest integer l, smaller than i, such that t 2" (al 1, tl). If such a value does not exist, then t became enabled, for the last time, at the initial aggregate a0 and the function returns 0. We propose to proceed by construction and built a path ⇡ satisfying the Theorem 2. We use the following algorithm to compute a set of delays di, for i = 1 . . . n and prove that the a0.m(!d1,t1)a1.m! . . . (!dn,tn)an.m is a run of the TPN associated with the TAG.
Input: an abstract path ⇡ = a0! t1 a1! . . .! tn an Output: a concrete path ⇡ = m0(!d1,t1)m1! . . . (!dn,tn)mn begin 1 8 i = 1 . . . n 2 di ↵ i 1ti 3 8 i = n 1 . . . 1 4 k = LastN ewi(ti+1) 5 If (Pij=1k dj+1 < ti+1min ) 6 7 8 k j < i dj+1 = M ax(dj+1, ↵ jti+1
↵ j+1ti+1 ) and Pij=1k(↵ jt ↵ j+1t ) ti+1max for any transition t 2#(ai 1, ti). Now, the elapsed time since the last time ti+1 became enabled can exceed ti+1max . This can occur if, in order to ensure the firing of some transition tj (for j > i + 1) this time has been increased by the algorithm (lines 5 7). Thus, one has to decrease this time while maintaining the firability of the transition tj . This is ensured by lines 8 10. The last condition that could prevent ti+1 from being fireable at ai. is that condition (2) is violated: the time elapsed between the moment some transition t, enabled before, ti+1, and the moment ti+1 became enabled is bigger than tmax ti+1min . This can happen when the firing of some transition tj , with j > i + 1, involved the increase of this quantity of time. This case is treated at lines 11 15, by fixing this problem while maintaining the future firability of tj .
Thus, the algorithm ensures the construction of a run of the TPN associated with the TAG that has the same trace. It is clear that the values of di, for i = 1 . . . n, respects the conditions of Theorem 2. Now, Theorem 1 ensures that if mn! d , for some d 2 R 0, then d (an). Finally, given d 2 R 0 s.t., d (an), the algorithm used to build ⇡ implies that the involved markings are reached as soon as possible. By construction of the TAG, (an) is the maximum time the system can stay at mn.
Using the above results one can use the TAG associated with a TPN in order to analyse both event and state based properties. In particular, we can check whether a given marking (resp. transition) is reachable (resp. is fireable) before (or after) some time. 4
Our ultimate goal is to be able, by browsing the TAG associated with a TPN, to check timed reachability properties. For instance, we might be interested in checking whether some state-based property ' is satisfied within a time interval [d, D), with d 2 N and D 2 (N [ {1} ), starting from the initial marking. The following usual reachability properties belong to this category. 1. 9 ⌃ [d;D]' : There exists a path starting from the initial state, consuming between d and D time units and leading to a state that satisfies '. 2. 8 ⇤[d;D]' : For all paths starting from the initial state, all the states, that are reached after d and before D time units, satisfy '. 3. 8 ⌃ [d;D]' : For all paths starting from the initial state, there exists a state in the path, reached after d and before D time units that satisfies '. 4. 9 ⇤[d;D]' : There exists a path from the initial state where all the states, that are reached after d and before D time units, satisfy '.
For the verification of time properties, an abstraction-based approach should allow the computation of the minimum and maximum elapsed time over any path. In the following, we establish that the TAG allows such a computation. Definition 8. Let N be a TPN and let G = hA, T, a0, i be the corresponding TAG. Let ⇡ = a0! t1 a1! . . .! tn an be a path in G. For each aggregate ai (for i = 0 . . . n), M inAT⇡ (ai) (resp. M axAT⇡ (ai)) denotes the minimum (resp. maximum) elapsed time between a0 and ai. In particular, M inAT (a0) := 0 and M axAT (a0) := (a0).
Proposition 1. Let N be a TPN and let G = hA, T, a0, i be the corresponding TAG. Let ⇡ = a0! t1 a1! . . .! tn an be a path in G. We denote by ↵ it (resp.
it ) the dynamic earliest (resp. latest) firing time of a transition t at aggregate ai, for i = 1 . . . n. Then, 8 i = 1 . . . n, the following holds: – M inAT⇡ (ai) = M inAT⇡ (ai 1) + ↵ i 1ti – M axAT⇡ (ai) = M axAT (ai 1) + M int2 Enable(ai)SCR(ai, t) aaaaa aaaaa aaaaa aaaaa aaaaa aaaaa aaaaa aaaaa aaaaa Region1 MaxAT < d Region2 MaxAT d MinAT D |= ' ? d
D
Region3 temps MinAT > D
Using the previous proposition, one can browse the TAG graph and compute the minimum and maximum bounds of the elapsed time of the current path on-the-fly. If a path of the TAG is considered as a counterexample for some time reachability property, one can use the algorithm given in the proof of Theorem 2 in order to build a concrete counterexample. Here we do not give the detailed algorithms for checking reachability properties on-the-fly, but we give the main intuition. The TAG is represented as a tree which is partitioned into three regions (see. Figure 3). The first region (Region1) contains the aggregates that are reachable strictly before d time units. The second region (Region2) contains the aggregates that are reachable between d and D time units and the last region contains the aggregates that are reachable strictly after D time units. In case D = 1 Region3 is empty. By doing so, the verification algorithms behave as follows: only aggregates belonging to Region2 are analyzed with respect to '. Region1 must be explored in order to compute the maximal and minimum access time of the traversed aggregates, but Region3 is never explored. In fact, as soon as an aggregate is proved to belong to Region3 the exploration of the current path is stopped. Furthermore, one has to check for a particular kind of Zeno behavior: if a cycle involving only aggregates whose minimal and maximal access times are equal, then the exploration of the current branch is stopped.
For instance checking the formula number 1 is reduced to the search of an aggregate a in Region2 that satisfies '. As soon as such an aggregate is reached the checking algorithm stops the exploration and returns true. When, all the aggregates of Region2 are explored (none satisfies ') the checking algorithm returns false. Dually, the formula number 2 is proved to be unsatisfied as soon as an aggregate in Region2 that do not satisfy ' is reached. When all the aggregates of Region2 are explored (each satisfies ') the checking algorithm returns true.
Checking formulae number 3 and 4 is slightly more complicated. In fact, checking formula number 3 is reduced to check if, along any path in Region2, there exists at least one aggregate satisfying '. As soon as a path in Region2 is completely explored without encountering an aggregate satisfying ', the exploration is stopped and the checking algorithm returns false. Otherwise, it returns true. Finally, checking formula 4 is reduced to check that there exists a path in Region2 such that all the aggregates belonging to this path satisfy '. This formula is proved to be true as soon as such a path is found. Otherwise, when all the paths of Region2 are explored (none satisfies the desired property), the checking algorithm returns false. 5
This section reviews the most known techniques, proposed in the literature, that abstract and analyse the state space of real-time systems described by means of TPN. Abstraction techniques aim at constructing, by removing some irrelevant details, a contraction of the state space of the model, which preserves properties of interest. The existing abstraction approaches mainly differ in the states agglomeration criteria, the characterization of states and state classes (interval states or clock states), the kind of preserved properties.
The States Class Graph (SCG) [
The Zones Based Graph (ZBG) [
Unlike the TAG, in all existing approaches, the time information does not appear explicitly in nodes which leads to additional and costly calculations such as: the manipulation of DBM to encode the zones (for zones based approaches) and the classes (for state-class based approaches), the approximations to counter the problem of unbounded transitions, conversion of graphs to timed automata (using UPPAAL) to model check properties (etc). In our work the time information is encoded within the aggregates allowing to check time properties just by browsing the graph, which has a significant impact on the construction complexity. The encoding of the timing information in the aggregates is such that the minimum and maximum elapsed time in every path of the TAG can be computed. 6
The efficiency of the verification of timed reachability properties is closely linked with the size of the explored structure to achieve this verification. Thus, it was important to first check that the TAG is a suitable/reduced abstraction before performing verification on it. Our approach for building TAG-TPN was implemented in a prototype tool (written in C++), and used for experiments in order to validate the size of the graphs generated by the approach (note that the prototype was not optimized for time efficiency yet, therefore no timing figures are given in this section). All results reported in this section have been obtained on a Mac-os with 2 gigahertz Intel with 8 gigabytes of RAM. The implemented prototype allowed us to have first comparison with existing approaches with respect to the size of obtained graphs. This section is dedicated to report, compare and discuss the experimental results obtained with three approaches: SCG, ZBG and TAG-TPN. Notice that we used the ROMEO tool to build both SCGs and ZBGs. The built versions preserve Linear-time Temporal Logic (LTL) properties. We tested our approach on several TPN models and we report here the obtained results for three well known examples of parametric TPN models.
The considered models are: (1) a TPN representing a composition of
producer/consumer models by fusion of a single buffer (of size 5) [
Table1 reports the results obtained with the SCG, the ZBG and the TAGTPN approaches, in terms of graph size number of nodes/number of edges).
SCG (with Tina) (nodes / arcs) 34 / 56 748 / 2460 4604 / 21891 14086 / 83375 31657 / 217423 61162 / 471254 107236 / 907 708 4 / 4 18 / 29 65 / 146 220 / 623 727 / 2536 2378 / 9154 7737 / 24744 25080 / 102242
The obtained preliminary results show that the size of the TAG is comparable to the size of the graphs obtained with the ZBG and the SCG approaches. The TAG achieves better performances than both SCG and ZBG for the train crossing example, while it is slightly worse for the Fischer’s protocol and performs similarly to SCG but worse than ZBG for the producer/consumer example.
This is an encouraging result because of the following reasons: The TAG allows for checking timed properties while the SCG approach do not. Also, it can be used for the verification of event-based timed properties while the ZBG approach do not. An other difference consists in the fact that the verification of timed properties can be achieved directly on the TAG, without any synchronisation with an additional automaton (representing the formula to be checked), nor any prior step of translation to timed automata. Moreover, using the algorithm given in the proof of Theorem 2, and in the prospect of using the TAG in order to check timed properties, one can exhibit (e.g., from a counterexample abstract path in the TAG) an explicit run involving the time spent at each reached marking. Finally, we claim that the TAG is a suitable abstraction for further reductions, especially the partial order reduction which is based on the exploitation of the independency between the TPN transitions. The third example of Figure 2 is a typical illustration of the gain one could have by applying such a reduction. 7
We proposed a new symbolic graph for the abstraction of the TPN state space. The proposed graph, called TAG, produces a finite representation of the bounded TPN behavior and allows for analyzing of timed reachability properties. Unlike, the existing approaches, our abstraction can be directly useful to check timed logic properties. We think that our approach is more understandable than the SCG and the ZBG approaches (the two main approaches for TPNs analysis since three decades) and easily implementable. Another feature of our approach is that each path of the TAG can be matched with a concrete path of the TPN model where the elapsed time at each encountered state is exhibited.
Our ultimate goal is to use the TAG traversal algorithm for the verification of timed reachability properties expressed in the TCTL logic. Several issues have to be explored in the future: We first have to improve our implementation so that time consumption criterion can be taken into account in our comparison to existing tools. We should also, carry out additional experimentations (using more significant use cases) to better understand the limits of our approach and to better compare the TAG technique to the existing approaches. Second, we believe that partial order reduction techniques can be used to reduce the size of the TAG while preserving time properties but without necessarily preserving all the paths of the underlying TPN. Finally, two challenging perspectives can be considered in the future: (1) the design and the implementation of model checking algorithms for verification of TCTL formulae, and (2), the extension of our approach to timed automata.