=Paper=
{{Paper
|id=None
|storemode=property
|title=Clock Transition Systems
|pdfUrl=https://ceur-ws.org/Vol-928/0227.pdf
|volume=Vol-928
|dblpUrl=https://dblp.org/rec/conf/csp/LimeRJ12
}}
==Clock Transition Systems==
https://ceur-ws.org/Vol-928/0227.pdf
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.