Clock Transition Systems D. Lime1 and O.H. Roux1 and C. Jard2? 1 LUNAM Université, École Centrale de Nantes, IRCCyN UMR CNRS 6597, Nantes, France 2 ENS Cachan & INRIA, IRISA, Rennes, France Université européenne de Bretagne Abstract. The objective of the paper is to introduce a new model ca- pable 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 de- scription of invariants. We show that CTS allow to express TPNs (even when unbounded) and NTA. For those two classical models, we iden- tify 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 defined for general CTSs. Armed with these merits, the CTS model seems a good candidate to serve as an intermediate theoretical and prac- tical model to factor out the upcoming developments in the TPNs and the NTA scientific communities. Keywords: Real-time systems; Timed models; Timed Automata; Time Petri nets; 1 Introduction Mastering the development of correct distributed real-time systems remains a priority in light of clear scientific 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 tran- sition 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] defined 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 specification, 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 rep- resent 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 specification of permissible behavior requires a description of fine temporal con- straints, and for which verification must be performed by efficient tools, the scientific 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 different extensions. These models respectively time extend Petri nets and finite 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 partic- ularly well suited for having a compact representation of concurrent behaviors with causal dependencies induced by complex synchronization between activi- ties. The time constraints are described on transitions by intervals of firing. The mixture of concurrency and global time induces non local constraints, which are sometimes difficult 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 defining 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 gen- eral 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 mod- els are very close, but nevertheless have subtle differences that have prevented until now to actually factorize research and development of associated technolo- gies. 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 scientific communities. Outline of the paper. We first 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 Definitions 2.1 Basic Notations and Definitions N is the set of natural numbers and Z is the set of integers. B = {true, false} is the set of booleans. For a finite set E, we denote its size by |E| and by 2E the set of all its subsets. For any two sets E and F , we denote by E F 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 finite 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 ∀x ∈ X, 0(x) = 0. For a valuation v and R ⊆ X, we write v[R ← 0] the valuation such that ∀x ∈ R, v[R ← 0](x) = 0 and ∀x 6∈ R, v[R ← 0](x) = v(x). Finally, for d ∈ R≥0 , v + d is the valuation such that ∀x ∈ 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 φ ::= true|x ≤ k|x < k|¬φ|φ ∧ φ, where x is a clock in X, k ∈ 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 satisfies 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 |= γ. For two finite sets A and B, F(A, B) denotes the set of computable functions from A to B. Definition 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 ∈ Q is the initial state, A is a finite set of actions disjoint from R≥0 , →⊆ e Q × (A ∪ R≥0 ) × Q is a set of edges. If (q, e, q 0 ) ∈−→, we also write q −−→ q 0 . Moreover, TTS should satisfy the classical time-related conditions where d, d0 ∈ d d R≥0 : i) time determinism: (q −→ q 0 ) ∧ (q − → q 00 ) ⇒ (q 0 = q 00 ), ii) time additivity: d d0 d+d0 0 → q 0 ) ∧ (q 0 −→ q 00 ) ⇒ (q −−−→ q 00 ), iii) null delay: ∀q : q − (q − → q, and iv) time d d0 → q 0 ) ⇒ (∀d0 ≤ d, ∃q 00 , q −→ q 00 ). continuity: (q − Let S = (Q, q0 , A, →) be a TTS. Let →∗ be the reflexive and transitive closure of →. We denote Reach(q0 ) = {q ∈ Q|q0 →∗ q}, the set of reachable states in S. Definition 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 ∀q, ∀q 0 ∈ Reach(q01 ) we a∈A a d∈R≥0 d have: q −−−→1 q 0 iff f (q) − →2 f (q 0 ) and q −−−−→1 q 0 iff f (q) − →2 f (q 0 ). Definition 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 , iff SA ∼ = SA0 . 2.2 Clock Transition Systems Definition 4 (Clock Transition System). A (labeled) Clock Transition Sys- tem is a tuple hV, T, Pre, Post, m0 , A, λ, X, Guard, Resets, Invi such that: – V is a finite non-empty set of integer variables; – T is a finite 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 finite non-empty alphabet; – λ : T → A is a labeling function of the transitions; – X is a finite set of clocks; – Guard : T → C(X) gives a time guard for each transition; V – Resets : T → 2F (N ,B)×X defines a conditional reset of clocks on transitions; – Inv ⊆ F(NV , B) × B(X) defines a finite set of invariants The semantics of the CTS T = hV, T, Pre, Post, m0 , A, λ, X, Guard, Resets, Invi is defined by the timed transition system ST = (NV × RX ≥0 , (m0 , 0), A, →) such that: a∈A – (m, v) −−−→ (m0 , v 0 ) iff there exists t ∈ T such that: • Pre(t)(m) is true; • λ(t) = a; • m0 = Post(t)(m); • v |= Guard(t); • v 0 = v {x|(f, x) ∈ Resets(t) and f (m)} ← 0 ;   • ∀(f, J) ∈ Inv, f (m0 ) implies v 0 |= J. d∈R≥0 – (m, v) −−−−→ (m, v + d) iff ∀(f, J) ∈ Inv, f (m) ⇒ ∀0 < d0 ≤ d, v + d0 |= J. T is said to be k-bounded if for any (m, v) reachable from (m0 , 0) in ST , we have ∀p ∈ 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 ex- plicit 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 finite representation of the infinite 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. V = {V1 , V2 }, T = {t1 , t2 , t3 , t4 }, X = {x1 , x2 } Pre(t1 ) = (V1 > 0), Post(t1 ) = (V2 := V1 + V2 ) Pre(t2 ) = (V2 > 0), Post(t2 ) = (V2 := V2 − 1) Guard(t1 ) = (x1 = 2), Guard(t2 ) = (x1 = 1) Pre(t3 ) = (V2 < α), Post(t3 ) = (V1 := V1 + 1) Guard(t3 ) = Guard(t4 ) = (1 ≤ x2 ≤ 3) Pre(t4 ) = (V1 > 1) ∧ (V2 > β) Resets(t1 ) = Resets(t2 ) = {(true, x1 )} Post(t4 ) = (V1 := V1 div 2), m0 = (1, 0) Resets(t3 ) = Resets(t4 ) = {(true, x2 )} Inv = {((V1 > 0), x1 ≤ 2), ((V2 > 0), x1 ≤ 1), ((V2 < α)∨((V1 > 1)∧(V2 > β)), x2 ≤ 3)} Table 1. A small CTS (control flow). It represents a system of flow 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 β (α < β) defining 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 overflow). 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. V2 V1 time Fig. 1. A possible execution of the CTS example of Table 1. 3 Time Petri Nets and Clock Transition Systems Definition 5 (Petri Net). A (labeled) Petri Net N is a tuple hP, T, Pre, Post, m0 , A, λi such that: – P is a finite non-empty set of places; – T is a finite 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 finite 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 ∈ 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 ∈ T is said to be enabled by the marking m if ∀p ∈ •t, m(p) ≥ Pre(p, t). This is denoted by t ∈ en(m). The operational semantics of the Petri Net N = hP, T, Pre, Post, m0 i is defined by the transition system SN = (N|P | , m0 , a A, →) such that: m − → m0 iff there exists t ∈ en(m) such that λ(t) = a and ∀p ∈ P, m0 (p) = m(p) − Pre(p, t) + Post(p, t). We then say that m0 is obtained from m by firing 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, defining the durations during which they will be enabled. We note I the set of rational intervals {x ∈ R|a ∼1 x ∼2 b, a ∈ Q≥0 , b ∈ Q≥0 , ∼1 , ∼2 ∈ {<, ≤}} ∪ {x ∈ Q|a ∼ x < +∞, a ∈ Q≥0 , ∼∈ {<, ≤}}. For any interval I, we denote by I ↓ the smallest left-closed interval with lower bound 0 that contains I. Definition 6 (Time Petri Net). A time Petri net (TPN) is a tuple T = hN , Is i where: – N = hP, T, Pre, Post, m0 , A, λi is a Petri Net; – Is : T → I assigns a static time interval to each transition. p1 p2 t1 [0, ∞[ t0 [0, 0] t2 [1, 2] p3 p4 p5 t3 [2, 2] Fig. 2. A Time Petri Net. For each transition t there is an associated clock xt . We consider valuations on the set of clocks {xt |t ∈ T } 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 firing t. Let m00 be the intermediate marking defined by ∀p, m00 (p) = m(p) − Pre(p, t). A transition t0 is newly enabled by the firing of t from m, and we note t ∈ new(m, t) if t0 ∈ en(m0 ) \ en(m00 ) ∪ {t} The operational semantics of the TPN T = hN , Is i is defined by the time transition system ST = (NP × RT≥0 , (m0 , 0), A, →) such that: a∈A – (m, v) −−−→ (m0 , v 0 ) iff there exists t ∈ en(m) such that: • λ(t) = a; • ∀p ∈ P, m0 (p) = m(p) − Pre(p, t) + Post(p, t); • v(t) ∈ Is (t); • v 0 = v[new(m, t) ← 0]. d∈R≥0 – (m, v) −−−−→ (m, v + d) iff ∀t0 ∈ en(m), ∀0 < d0 ≤ d, (v + d0 )(t0 ) ∈ Is↓ (t0 ). Boundedness of (time) Petri nets is defined 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 define a syntactic subclass of CTSs that is equivalent to TPNs: Definition 7. The syntactic subclass CTS-TPN of CTS is defined by the fol- lowing restrictions: – ∀t ∈ T, ∀p ∈ V , there exists k(p, t) ∈ N, k 0 (p, t) ∈ Z s.t.: • k 0 (p, t) ≥V−k(p, t); • Pre(t) = p∈P p ≥ k(p, t); • Post(t) is a list of assignments ∀p, p := p + k 0 (p, t); V = {p1 , p2 , p3 , p4 , p5 }, T = {t0 , t1 , t2 , t3 } m0 = (1, 1, 0, 0, 0), X = T Guard(t0 ) = (t0 = 0), Guard(t1 ) = (t1 ≥ 0) Guard(t2 ) = (1 ≤ t2 ≤ 2), Guard(t3 ) = (t3 = 2) Pre(t0 ) = (p3 ≥ 1) ∧ (p4 ≥ 1) Resets(t0 ) = {((p1 = 0), t1 ), ((p2 = 0), t2 )} Pre(t1 ) = (p1 ≥ 1), Pre(t2 ) = (p2 ≥ 1) Resets(t1 ) = {((p3 = 0), t0 ), ((p3 = 0), t3 )} Pre(t3 ) = (p3 ≥ 1) Resets(t2 ) = {((p4 = 0), t0 )}, Resets(t3 ) = ∅ Post(t1 ) = (p1 := p1 − 1, p3 := p3 + 1) Post(t2 ) = (p2 := p2 − 1, p4 := p4 + 1) Post(t3 ) = (p3 := p3 − 1, p5 := p5 + 1) Post(t0 ) = (p1 := p1 + 1, p2 := p2 + 1, p3 := p3 − 1, p4 := p4 − 1) Inv = {(Pre(t0 ), (t0 = 0)), (Pre(t1 ), true), (Pre(t2 ), (t2 ≤ 2)), (Pre(t3 ), (t3 ≤ 2))} Table 2. CTS coding the TPN of Fig. 2. • For a valuation m, we define m0t by ∀p ∈ P, m0t (p) = m(p) − k(p, t) + k 0 (p, t) and m00t by ∀p ∈ P, m00t (p) = m(p) − k(p, t). Then Resets(t) = {(gt0 , xt0 )|t0 ∈ T } and gt0 (m) holds iff t = t0 or (Pre(t0 )(m0t ) and not Pre(t0 )(m00t )); – ∀t ∈ T , Guard(t) refers to at most one clock xt and xt = xt0 implies t = t0 ; – Inv = {(Pre(t), Jt )|t ∈ T } (note that Jt may be true); – ∀t ∈ 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; – ∀t ∈ T , if Jt = true then Guard(t) has no finite 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. Definition 8 (Timed Automaton). A Timed Automaton (TA) is a tuple A = hL, `0 , E, A, λ, X, Guard, Resets, Invi where: – L is a finite non-empty set of locations; – `0 ∈ L is the initial location; – E ⊆ L × L is a finite set of directed edges; – A is finite non-empty alphabet; – λ : E → A is the edge labelling function; – Xis a finite 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) defines a set of invariants; Definition 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: a∈A – (l, v) −−−→ (l0 , v 0 ) iff ∃e = (l, l0 ) ∈ E such that: • λ(e) = a; • v |= Guard(e); • v 0 = v[Resets(e) ← 0]; • v 0 |= Inv(l0 ) d∈R≥0 – (l, v) −−−−→ (l, v + d) iff ∀d0 0 < d0 ≤ d, v + d0 |= 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 au- tomata. To this end, we use the classical composition notion based on a synchro- nization function à la Arnold-Nivat. Definition 10 (Networks of Timed Automata). Let A1 , . . . , An be n timed automata with Ai = hLi , `0i , Ei , A, λi , X, Guardi , Resetsi , Invi i. A synchroniza- tion function f is a partial function from (A ∪ {•})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 (A1 | . . . |An )f is the parallel composition of the Ai ’s w.r.t. f . The configurations of (A1 | . . . |An )f are pairs (~l, v) with ~l = (l1 , . . . , ln ) ∈ L1 × . . . × Ln , the ith component li ∈ 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 ∈ 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 definition: Definition 11 (Semantics of NTA). Let A1 , . . . , An be n timed automata with Ai = hLi , `0i , Ei , A, λi , X, Guardi , Resetsi , Invi i, SA1 , . . . , SAn their seman- tics with SAi = (Qi , q0i , A, →i ). Let f be a (partial) synchronization function (A ∪ {•})n → A. The semantics of (A1 | . . . |An )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 defined by: b∈A – (~l, v) −−−→ (~l0 , v 0 ) iff Resetsi ((~l[i], ~l0 [i])). Then v 0 = v[R ← 0], S • Let R = i∈[1..n],(~l[i],l~0 [i])∈Ei • every Ai agrees on synchronization i.e. there exists (a1 , . . . , an ) ∈ (A ∪ {•})n s.t. f (a1 , . . . , an ) = b and for any i ∈ [1..n] we have: ∗ If ai = •, then ~l0 [i] = ~l[i], ai ∗ If ai ∈ A, then (~l[i], v) −→ ~0 0 i (l [i], vi ). Note that ∀x ∈ X\Resets, 0 0 v (x) = vi (x) d∈R≥0 ~ – (l, v) −−−−→ (~l, v + d) iff for all i ∈ [1..n], every Ai agrees on time elapsing d i.e. (~l[i], v) − →i (~l[i], v + d) 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. b:x=0 x≤1 y≤1 b l1 l2 l3 l4 a : [x] b : [x] c : y = 1, [y] Fig. 3. A network of two timed automata with two clocks x and y. Locations are denoted in circles, and invariants boxed above them. Transitions are labeled by their action (a, b or c), the guard on clocks and resets (bracketed). V = {p1 , p2 } m0 = (l1 , l3 ) T = {A, B1 , B2 , C} X = {x, y} λ(A) = a, λ(B1 ) = λ(B2 ) = b, λ(C) = c Guard((A) = Guard(B1 ) = true Pre(A) = (p1 = l1 ), Post(a) = (p1 := l2 ) Guard(B2 ) = (x = 0) Pre(B1 ) = ((p1 , p2 ) = (l2 , l3 )) Guard(C) = (y = 1) Post(B1 ) = ((p1 , p2 ) := (l2 , l4 )) Resets(A) = Resets(B1 ) = {(true, x)} Pre(B2 ) = ((p1 , p2 ) = (l2 , l3 )) Resets(B2 ) = ∅ Post(B2 ) = ((p1 , p2 ) := (l1 , l4 )) Resets(C) = {(true, y)} Pre(C) = (p2 = l3 ), Post(C) = (p2 := l3 ) Inv = {((p1 = l1 ), true), ((p1 = l2 ), (x ≤ 1)), ((p2 = l3 ), (y ≤ 1)), ((p2 = l4 ), true)} Table 3. CTS coding the NTA of Fig. 3. 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. 5 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 workflow in which sequential components are modelled as TA, components fea- turing 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 finite representation of the infinite 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 de- cidable 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 ap- plied to both TPNs and TA, thus reducing the duplication of efforts. 6 Conclusion and perspectives We defined 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 verification 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. Roméo: 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 syn- thesis for time Petri nets. In 8th International Workshop on Discrete Event Sys- tems (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 methodolo- gies 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. Inter- national 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. Tech- nical 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.