Clock Transition Systems

Abstract

The objective of the paper is to introduce a new model capable of modeling both Time Petri Nets (TPNs) and Networks of Timed Automata (NTA). We called it Clock Transition System (CTS). This new model incorporates the advantages of the structure of Petri nets, while introducing explicitly the concept of clocks. Transitions in the network can be guarded by an expression on the clocks and reset a subset of them as in timed automata. The urgency may be introduced by a separate description of invariants. We show that CTS allow to express TPNs (even when unbounded) and NTA. For those two classical models, we identify subclasses of CTSs equivalent by isomorphism of their operational semantics and provide (syntactic) translations. The classical state-space computation developed for NTA and then adapted to TPNs can easily be de ned for general CTSs. Armed with these merits, the CTS model seems a good candidate to serve as an intermediate theoretical and practical model to factor out the upcoming developments in the TPNs and the NTA scienti c communities.

Keywords

• Real-time systems
• Timed models
• Timed Automata
• Time Petri nets

-

Mastering the development of correct distributed real-time systems remains a priority in light of clear scienti c issues they represent. One necessary lane in our opinion is the use of mathematically based models.

Low Level timed models. [ 10 ] introduce the abstract notion of timed transition systems allowing to give the formal semantics of a real time system as a set of timed execution sequences. They incorporate time into classical transition systems by assuming that all discrete transitions happen instantaneously while real time constraints restrict the times at which discrete transition may occur. [ 13 ] de ned timed transition systems (TTS) as a basic semantical model for real time systems which is a labelled transition system with two type of labels: atomics actions and delay actions (i.e. positive reals) representing discrete and continuous changes of real-time systems. ? This work was partially funded by the ANR national research program ImpRo (ANR-2010-BLAN-0317).

To avoid delay actions, [ 2, 3 ] advocate an alternative proposal, namely, to designate certain program variables as clock variables. It leads to higher level of speci cation, explicitly referring to clocks, which are just another kind of system variables. Thus, [ 9 ] extend labeled transition systems with clocks and consider both discrete or dense time domain. Similarly, [ 12 ] propose a computational model for real-time systems called Clocked Transition Systems. This model represent time by a set of timers (clocks) which increase whenever time progress, but can be set to arbitrary values by system (program) transitions. A Clocked Transition System is also equiped of discrete variables of any type. Assertions associated with transitions allow the updates of variables and assertions over system variables specify a global restriction of the time progress. TPNs and TA. For the class of critical systems that we aim, in which the speci cation of permissible behavior requires a description of ne temporal constraints, and for which veri cation must be performed by e cient tools, the scienti c community has notably focused for many years on two timed models: Time Petri nets (TPNs for short) [ 16, 4 ] and timed automata (TA for short) or networks of timed automata (NTA for short) [ 1 ], and their di erent extensions. These models respectively time extend Petri nets and nite automata. The paper [ 17 ] provides an overview of the theoretical known results about the relationships among these models.

Each class of model has its advantages and disadvantages. TPNs are particularly well suited for having a compact representation of concurrent behaviors with causal dependencies induced by complex synchronization between activities. The time constraints are described on transitions by intervals of ring. The mixture of concurrency and global time induces non local constraints, which are sometimes di cult to control from the designer point of view.

Timed automata better clarify how time should change. The designer's model introduces a set of temporal variables (clocks) used to form expressions guarding transitions. Transitions may reset clocks. The urgency is expressed by de ning invariants on states, forcing the progress if possible. Somehow, this model is less abstract than TPNs, but is sometimes easier to build. The introduction of concurrency is achieved by connecting synchronously a set of components. The interest is the modular construction of models. The disadvantage is that it induces a kind of premature architectural decision. Another quirk of the explicit management of clocks is the ability to block the time if you are not careful. Intermediate models for TPNs and NTA. The two main tools for TPNs and NTA are respectively TINA [ 5 ] and UPPAAL [ 14 ]. These tools use both intermediate model allowing to manipulate variables and computable functions extending the modeling concision, but in a rather restrictive way. In particular, TINA's intermediate model manipulates only interval representation for timing. It enables state class based analysis but is less general than explicit clocks used in NTA. UPPAAL manipulates bounded variables which can not represent general TPNs (which are Turing powerful). Moreover the UPPAAL synchronization mechanism, featuring only point-to-point and broadcast synchronizations, is less rich than that of TPNs.

Our contribution. A whole set of theories, methods and tools of analysis has been developed separately for TPNs and NTA. Yet we know that these models are very close, but nevertheless have subtle di erences that have prevented until now to actually factorize research and development of associated technologies. The objective of the paper is to introduce an intermediate model capable of modeling both TPNs and NTA. This intermediate model is inspired from Clocked Transition Systems [ 12 ] but with only integer variables and with high level functions, its semantics is a Timed Transition Systems [ 13 ] and we called it Clock Transition System (CTS for short). Clock Transition System is designed to incorporate the advantages of the structure of Petri nets, while introducing explicitly the concept of clocks. Transitions in the network can be guarded by an expression on the clocks and reset a subset of them as in timed automata. The urgency may be introduced by a separate description of invariants. These are associated with a marking of the Clock Transition System, which plays the same role as the state in a timed automaton. Armed with these merits, the Clock Transition System models seems a good candidate to serve as an intermediate model to factor out the upcoming theoretical and practical developments in the TPNs and the NTA scienti c communities.

Outline of the paper. We rst introduce in Section 2 the Clock Transition System model giving its syntax and its operational sequential semantics as usual. We then show in Sections 3 and 4 how TPNs and NTA can be easily represented by a Clock Transition System. Finally, Section 5 discusses the model and the techniques for its analysis. Proofs for the theorems can be found in [ 15 ]. 2 2.1

De nitions

Basic Notations and De nitions N is the set of natural numbers and Z is the set of integers. B = ftrue; falseg is the set of booleans. For a nite set E, we denote its size by jEj and by 2E the set of all its subsets. For any two sets E and F , we denote by EF the set of mappings from F into E.

Let R (resp. Q) be the set of real (resp. rational) numbers. R 0 (resp. Q 0 is the set of non-negative real (resp. rational) numbers. Let X be a nite set of clocks. A valuation v of X is a mapping from X into R 0. We denote by 0 the null valuation such that 8x 2 X; 0(x) = 0. For a valuation v and R X, we write v[R 0] the valuation such that 8x 2 R; v[R 0](x) = 0 and 8x 62 R; v[R 0](x) = v(x). Finally, for d 2 R 0, v + d is the valuation such that 8x 2 X; (v + d)(x) = v(x) + d. Similarly a valuation on a set of integer variables V is a mapping from V to N.

We denote by C(X) the set of constraints generated by the grammar ::= truejx kjx < kj: j ^ , where x is a clock in X, k 2 Q 0, : is the logical negation and ^ is the logical conjunction. We denote by B(X) the subset of C(X) without the use of negation. We say that a valuation v satis es a simple constraint if the expression obtained by replacing all clocks x by their valuation v(x) logically evaluates to true. We then write v j= .

For two nite sets A and B, F (A; B) denotes the set of computable functions from A to B. continuity: (q !d q0) ) (8d0

d; 9q00; q d!0 q00).

De nition 1 (Timed Transition System). A timed transition system (TTS) over the alphabet A is a tuple S = (Q; q0; A; !) where Q is a set of states, q0 2 Q is the initial state, A is a nite set of actions disjoint from R 0e, ! Q (A [ R 0) Q is a set of edges. If (q; e; q0) 2 !, we also write q ! q0. Moreover, TTS should satisfy the classical time-related conditions where d; d0 2 R 0: i) time determinism: (q !d q0) ^ (q !d q00) ) (q0 = q00), ii) time additivity: (q !d q0) ^ (q0 d!0 q00) ) (q d+d!0 q00), iii) null delay: 8q : q !0 q, and iv) time

Let S = (Q; q0; A; !) be a TTS. Let ! be the re exive and transitive closure of !. We denote Reach(q0) = fq 2 Qjq0 ! qg, the set of reachable states in S.

De nition 2 (Isomorphism). Let S1 = (Q1; q01 ; A; !1) and S2 = (Q2; q02 ; A; !2) be two TTSs. S1 and S2 are isomorphic (we write S1 = S2) whenever there is a bijection f : Reach(q01 ) ! Reach(q02 ) such that 8q; 8q0 2 Reach(q01 ) we have: q a2!A1 q0 i f (q) !a2 f (q0) and q d2R !01 q0 i f (q) !d2 f (q0). De nition 3 (Equivalence up to isomorphism). Let two models A and A0 whose semantics are expressed as TTSs SA and SA0 . A and A0 are equivalent up to isomorphism, which we denote A = A0, i SA = SA0 . 2.2

Clock Transition Systems De nition 4 (Clock Transition System). A (labeled) Clock Transition System is a tuple hV; T; Pre; Post; m0; A; ; X; Guard; Resets; Invi such that: { V is a nite non-empty set of integer variables; { T is a nite non-empty set of transitions; { Pre : T ! F (NV ; B) gives a discrete guard for each transition; { Post : T ! F (NV ; NV ) gives a discrete assignment for each transition; { m0 is the initial valuation of V ; { A is a nite non-empty alphabet; { : T ! A is a labeling function of the transitions; { X is a nite set of clocks; { Guard : T ! C(X) gives a time guard for each transition; { Resets : T ! 2F(NV ;B) X de nes a conditional reset of clocks on transitions; { Inv F (NV ; B) B(X) de nes a nite set of invariants

The semantics of the CTS T = hV; T; Pre; Post; m0; A; ; X; Guard; Resets; Invi is de ned by the timed transition system ST = (NV RX0; (m0; 0); A; !) such that: { (m; v) a2!A (m0; v0) i there exists t 2 T such that:

Pre(t)(m) is true;

(t) = a; m0 = Post(t)(m); v j= Guard(t); v0 = v fxj(f; x) 2 Resets(t) and f (m)g 8(f; J ) 2 Inv, f (m0) implies v0 j= J . 0 ; { (m; v) d2R !0 (m; v + d) i 8(f; J ) 2 Inv, f (m) ) 80 < d0 d; v + d0 j= J .

T is said to be k-bounded if for any (m; v) reachable from (m0; 0) in ST , we have 8p 2 P; m(p) k. T is said to be bounded if there exists k such that T is k-bounded.

State space and main properties. Clock Transition System allows only explicit clocks and integer variables. We can then easily extend the classical zone abstraction used in the tool Uppaal [ 14 ]. For bounded CTS this abstraction gives a nite representation of the in nite state-space and many analysis techniques can be constructed to decide safety, reachability, liveness, etc. We then obtain the following theorems.

Theorem 1. k-boundedness is decidable for CTS.

Theorem 2. Reachability is decidable for bounded CTS.

Example. To actually illustrate how we can design a CTS, consider the following small example in Table 1.

It represents a system of ow control between a producer and a consumer. The producer produces a set of objects every two time units. The number of items produced in each burst is determined by a counter V1 which can be controlled by the receiver. The receiver stores the objects in a container V2 which is emptied at a rate of one object every time unit. It also knows two constants and ( < ) de ning response thresholds. Below a volume of stock , the receiver causes the increment of V1 to gradually accelerate the activity of the sender. Above the threshold , V1 is divided by two to reduce sharply the activity of the sender (risk of over ow). The acceleration and deceleration commands require between one to three units of time to be taken into account. Fig. 1 shows a possible timed execution of the system.

V1 time { P is a nite non-empty set of places; { T is a nite non-empty set of transitions; { Pre : P T ! N is the backward incidence function; { Post : P T ! N is the forward incidence function; { m0 : P ! N is the initial marking of the net; { A is nite non-empty alphabet; { : T ! A is a labeling function of the transitions.

A marking of N is an application from P to N. Let m be a marking of N . Then, for any place p 2 P , we say that p contains m(p) tokens. For any transition t we denote by t the set of places p such that Pre(p; t) 6= 0 and by t the set of places p such that Post(p; t) 6= 0.

A transition t 2 T is said to be enabled by the marking m if 8p 2 t; m(p) Pre(p; t). This is denoted by t 2 en(m). The operational semantics of the Petri Net N = hP; T; Pre; Post; m0i is de ned by the transition system SN = (NjP j; m0; A; !) such that: m !a m0 i there exists t 2 en(m) such that (t) = a and 8p 2 P; m0(p) = m(p) Pre(p; t) + Post(p; t).

We then say that m0 is obtained from m by ring the enabled transition t.

Petri nets can be extended with timing information in many ways. We focus here on Time Petri Nets [ 16 ] in which time intervals are attached to transitions, de ning the durations during which they will be enabled.

We note I the set of rational intervals fx 2 Rja 1 x 2 b; a 2 Q 0; b 2 Q 0; 1; 22 f<; gg [ fx 2 Qja x < +1; a 2 Q 0; 2 f<; gg.

For any interval I, we denote by I# the smallest left-closed interval with lower bound 0 that contains I.

De nition 6 (Time Petri Net). A time Petri net (TPN) is a tuple T = hN ; Isi where: { N = hP; T; Pre; Post; m0; A; i is a Petri Net; { Is : T ! I assigns a static time interval to each transition.

Fig. 2. A Time Petri Net.

For each transition t there is an associated clock xt. We consider valuations on the set of clocks fxtjt 2 T g and we will slightly abuse the notations by writing v(t) instead of v(xt).

Let m be a marking of the net and t a transition in en(m). Let m0 be the marking obtained from m by ring t. Let m00 be the intermediate marking de ned by 8p; m00(p) = m(p) Pre(p; t). A transition t0 is newly enabled by the ring of t from m, and we note t 2 new(m; t) if t0 2 en(m0) n en(m00) [ ftg

The operational semantics of the TPN T = hN ; Isi is de ned by the time transition system ST = (NP RT 0; (m0; 0); A; !) such that: { (m; v) a2!A (m0; v0) i there exists t 2 en(m) such that:

(t) = a; 8p 2 P; m0(p) = m(p) Pre(p; t) + Post(p; t); v(t) 2 Is(t); v0 = v[new(m; t) 0]. { (m; v) d2R !0 (m; v + d) i 8t0 2 en(m); 80 < d0 d; (v + d0)(t0) 2 Is#(t0).

Boundedness of (time) Petri nets is de ned exactly as for CTSs.

We now prove that possibly unbounded TPNs form a subclass of CTSs. First, the following theorem holds: Theorem 3. Every TPN N can be translated into a CTS T (N ) s.t. N = T (N ).

To illustrate the encoding, consider the TPN in Fig. 2. Its equivalent in CTS is given in Table 2. We now de ne a syntactic subclass of CTSs that is equivalent to TPNs: De nition 7. The syntactic subclass CTS-TPN of CTS is de ned by the following restrictions: { 8t 2 T; 8p 2 V , there exists k(p; t) 2 N; k0(p; t) 2 Z s.t.: k0(p; t) k(p; t); Pre(t) = Vp2P p k(p; t);

Post(t) is a list of assignments 8p; p := p + k0(p; t);

For a valuation m, we de ne m0t by 8p 2 P; m0t(p) = m(p) k(p; t) + k0(p; t) and m0t0 by 8p 2 P; m0t0(p) = m(p) k(p; t).

Then Resets(t) = f(gt0 ; xt0 )jt0 2 T g and gt0 (m) holds i t = t0 or (Pre(t0)(m0t) and not Pre(t0)(m0t0)); { 8t 2 T , Guard(t) refers to at most one clock xt and xt = xt0 implies t = t0; { Inv = f(Pre(t); Jt)jt 2 T g (note that Jt may be true); { 8t 2 T , Jt refers only to xt and is not equal to xt < 0. Furthermore, if Jt = xt k or Jt = xt < k, then the set of valuations satisfying Guard(t) ^ xt = a is non-empty; { 8t 2 T , if Jt = true then Guard(t) has no nite upper bound.

Theorem 4. Every CTS-TPN T can be translated into a TPN N (T ) such that T = N (T ).

Corollary 1. The class CTS-TPN is equivalent to the class of TPNs up to isomorphism of TTS. 4

Networks of Timed Automata and Clock Transition

Systems

Timed Automata [ 1 ] are used to model systems which combine discrete and continuous evolutions.

De nition 8 (Timed Automaton). A Timed Automaton (TA) is a tuple A = hL; `0; E; A; ; X; Guard; Resets; Invi where: { L is a nite non-empty set of locations; { `0 2 L is the initial location; { E L L is a nite set of directed edges; { A is nite non-empty alphabet; { : E ! A is the edge labelling function; { Xis a nite set of positive real-valued clocks; { Guard : E ! C(X) gives a guard for each edge; { Resets : E ! 2X gives a set of clocks to reset for each edge; { Inv : L ! B(X) de nes a set of invariants; De nition 9 (Semantics of TA). The semantics of a timed automaton A = hL; `0; E; A; ; X; Guard; Resets; Invi is a timed transition system SA = (Q; q0; A; !) with Q = L (R 0)X , q0 = (l0; 0) is the initial state and ! consists of the discrete and continuous transition relations:

9e = (l; l0) 2 E such that: { (l; v) a2!A (l0; v0) i

(e) = a; v j= Guard(e); v0 = v[Resets(e) v0 j= Inv(l0) { (l; v) d2R !0 (l; v + d) i 8d0 0 < d0 d; v + d0 j= Inv(l) A run of a timed automaton A is a path in SA starting in q0.

It is convenient to describe a system as a parallel composition of timed automata. To this end, we use the classical composition notion based on a synchronization function a la Arnold-Nivat.

De nition 10 (Networks of Timed Automata). Let A1, . . . , An be n timed automata with Ai = hLi; `0i ; Ei; A; i; X; Guardi; Resetsi; Invii. A synchronization function f is a partial function from (A [ f g)n to A where is a special symbol used when an automaton is not involved in a step of the global system. A Network of Timed Automata (A1j : : : jAn)f is the parallel composition of the Ai's w.r.t. f .

The con gurations of (A1j : : : jAn)f are pairs (~l; v) with ~l = (l1; : : : ; ln) 2 L1 : : : Ln, the ith component li 2 Li of ~l is denoted by ~l[i], v is a valuation on the set of clocks X and v(x) is the value of the clock x 2 X. The network can do a discrete transition if all the components agree to and time can progress in the network also if all the components agree to. This is formalized by the following de nition: De nition 11 (Semantics of NTA). Let A1; : : : ; An be n timed automata with Ai = hLi; `0i ; Ei; A; i; X; Guardi; Resetsi; Invii, SA1 ; : : : ; SAn their semantics with SnAi = (Qi; q0i ; A; !i). Let f be a (partial) synchronization function (A [ f g) ! A. The semantics of (A1j : : : jAn)f is a timed transition system S = (Q; q0; A; !) with Q = L1 : : : Ln (R 0)X , q0 is the initial state ((`01 ; : : : ; `0n ); 0) and ! is de ned by: { (~l; v) b2!A (~l0; v0) i

Let R =

S

Resetsi((~l[i]; ~l0[i])). Then v0 = v[R 0], i2[1::n];(~l[i];l~0[i])2Ei every Ai agrees on synchronization i.e. there exists (a1; : : : ; an) 2 (A [ f g)n s.t. f (a1; : : : ; an) = b and for any i 2 [1::n] we have:

If ai = , then ~l0[i] = ~l[i], If ai 2 A, then (~l[i]; v) v0(x) = vi0(x)

a!ii (~l0[i]; vi0). Note that 8x 2 XnResets, i.e. (~l[i]; v) !di (~l[i]; v + d) { (~l; v) d2R !0 (~l; v + d) i for all i 2 [1::n], every Ai agrees on time elapsing

Now we prove that NTA form a subclass of CTSs and are indeed equivalent to bounded CTSs.

Theorem 5. Every NTA A can be translated into a CTS T (A) s.t. A = T (A).

To illustrate the encoding, consider the NTA in Fig. 3. Its equivalent in CTS is given in Table 3.

l1 b : x = 0 a : [x] x

1 l2 b : [x] y

1 l3 c : y = 1; [y] b l4

Theorem 6. Every bounded CTS T can be translated into a TA A(T ) s.t. T = A(T ).

Corollary 2. The class of bounded CTSs is equivalent to the class of TA up to isomorphism of TTS.

Discussion

As we have seen in the previous section, the expressive power and conciseness of Clock Transition Systems are two of their best assets. Furtermore, since both TA and TPNs can easily be transformed in CTS, one can imagine a modelling work ow in which sequential components are modelled as TA, components featuring complex synchronization are modelled as TPNs, and complex dynamics are directly discretized in the form of CTS. This mixed modelling can ultimately be transformed in CTS for the analysis.

We can lift most of the analysis techniques developed for (time) Petri nets and (timed) automata to CTS. For instance: { For unbounded untimed CTSs, given adequate restrictions on the discrete guard and assignment functions (such as those in the subclass CTS-TPN), we can compute a coverability graph [ 11 ]. { For bounded CTSs (with time), we can easily extend the region abstraction [ 1 ] or the zone abstraction used in the tool Uppaal [ 14 ]. These abstractions give a nite representation of the in nite state-space. From these basic abstractions many analysis techniques can be constructed to decide safety, reachability, liveness, etc. { For potentially unbounded CTSs (with time), the techniques based on these abstractions become semi-algorithms. A few interesting problems are still decidable though, e.g. k-boundedness and even safety control of the unbounded CTS to automatically make it bounded using the technique of [ 7 ]. It should also be possible to apply supervision techniques like in [ 8 ].

Finally, new techniques developed directly for CTSs can be immediately applied to both TPNs and TA, thus reducing the duplication of e orts. 6

Conclusion and perspectives

We de ned the new model of clock transition systems. It blends concepts from both time Petri nets and networks of timed automata. That means that CTS is a good intermediate model to develop tools, while factoring software developments. We showed that (in terms of isomorphism of TTS formal semantics): { TPNs and TA may be encoded using CTSs; { The syntactic subclass CTS-TPNs forms exactly the set of TPNs; { Bounded CTSs form exactly the set of Timed Automata; { Computation of a symbolic state-space is possible for CTSs and in particular allows model-checking.

The other contribution is that CTSs ultimately appear to be a powerful and concise formalism for describing timed models. One could also imagine a possible mixture of NTA, TPNs and CTSs to model complex timed behaviors, all of them being ultimately transcribed into CTSs, analyzed by a unique engine.

The outlook is therefore to start from this model for our next developments in the tool Romeo [ 6 ]. In particular, we will equip this model with a concurrent semantics to build timed unfoldings.

References

1. Rajeev Alur and David L. Dill . A theory of timed automata . Theoretical Computer Science , 126 ( 2 ): 183 { 235 , 1994 .

2. Rajeev Alur and Thomas A. Henzinger . Real-time system = discrete system + clock variables. In Theories and Experiences for Real-Time System Development , AMAST Series in Computing, volume 2 , 1994 .

3. Rajeev Alur and Thomas A. Henzinger . Real-time system = discrete system + clock variables . Software Tools for Technology Transfer , 1 : 86 { 109 , 1997 .

4. B. Berthomieu and M. Diaz . Modeling and veri cation of time dependent systems using time Petri nets . IEEE trans. on Soft. Eng. , 17 ( 3 ): 259 { 273 , 1991 .

5. B. Berthomieu , P. - O. Ribet , and F. Vernadat . The tool TINA { construction of abstract state spaces for Petri nets and time Petri nets . International Journal of Production Research , 42 ( 4 ), July 2004 .

6. Guillaume Gardey , Didier Lime, Morgan Magnin, and Olivier (H.) Roux . Romeo: A tool for analyzing time Petri nets . In Proceedings of CAV'05 , volume 3576 of LNCS , Edinburgh, Scotland, UK , July 2005 . Springer.

7. Guillaume Gardey , Olivier (F.) Roux , and Olivier (H.) Roux . Safety control synthesis for time Petri nets . In 8th International Workshop on Discrete Event Systems (WODES'06) , pages 222 { 228 , Ann Arbor , USA, July 2006 . IEEE Computer Society Press.

8. Bartosz Grabiec , Louis-Marie Traonouez , Claude Jard, Didier Lime, and Olivier H. Roux . Diagnosis using unfoldings of parametric time Petri nets . In Proceedings of FORMATS'10 , volume 6246 of LNCS , pages 137 { 151 , Austria , September 2010 . Springer.

9. Thomas A. Henzinger , Peter W. Kopke , and Howard Wong-Toi. The expressive power of clocks . In Proceedings of the 22nd International Colloquium on Automata, Languages, and Programming (ICALP) , volume 944 of LNCS , pages 417 { 428 , 1995 .

10. Thomas A. Henzinger , Zohar Manna, and Amir Pnueli . Temporal proof methodologies for timed transitions systems . Information and Computation , 112 ( 2 ): 273 { 337 , 1994 .

11. Richard M. Karp and Raymond E. Miller . Parallel program schemata . Journal of Computer and System Sciences , 3 ( 2 ): 147 { 195 , 1969 .

12. Yonit Kesten , Zohar Manna, and Amir Pnueli . Verifying clocked transition systems . In Hybrid Systems , volume 1066 of LNCS , pages 13 { 40 , 1996 .

13. K. G. Larsen , P. Pettersson , and W. Yi . Model-checking for real-time systems . In Horst Reichel (Ed.), editor, Proceedings of the 10th International Conference on Fundamentals of Computation Theory , pages 62 { 88 , Dresden , Germany, August 1995 . LNCS 965.

14. Kim G. Larsen , Paul Pettersson, and Wang Yi . Uppaal in a nutshell . International Journal on Software Tools for Technology Transfer , 1 ( 1 {2): 134 { 152 , Oct 1997 . http://www.uppaal.com/.

15. Didier Lime , Olivier H. Roux , and Claude Jard . Clock transition systems . Technical report , Institut de Recherche en Communications et Cyberntique de Nantes (IRCCyN), 2012 . Available on HAL as hal- 00725792 .

16. P. M. Merlin . A study of the recoverability of computing systems . PhD thesis , Dep. of Information and Computer Science, University of California, Irvine, CA, 1974 .

17. J. Srba . Comparing the expressiveness of timed automata and timed extensions of Petri nets . In Proceedings of FORMATS'08 , volume 5215 of LNCS , pages 15 { 32 . Springer, 2008 .