428
S. Wimmer and J. von Mutius
1 Timed Automata and Model Checking
Transition Systems We take a very simple view of transition systems: they are
simply a relation → of type
a ⇒
a ⇒ bool for a type of states
a. We write
a →
∗ b to denote that b can be reached from a via a sequence of →-transitions.
Timed Automata To make the paper self-contained, this paragraph briefly describes timed automata and is mostly reproduced from Wimmer and Lammich
[29]. For a thorough introduction see the tutorial paper of Bengtsson and Yi [4].
Compared to standard finite automata, timed automata introduce a notion
of clocks. Figure 1 depicts an example of a timed automaton. We will assume
that clocks are of type nat. A clock valuation u is a function of type nat ⇒ real .
Locations and transitions are guarded by clock constraints, which have to be
l 1
l 2
c 1 ≤ 1 ∧ c 2 ≤ 100
l 3
c 1 > 0, a 1 , c 2 := 0
a 3 , c 1 := c 2 := 0
a 2 , c 1 := 0
c 1 > 100, a 4
Fig. 1: Example of a timed automaton with two clocks.
fulfilled to stay in a location or to take a transition. Clock constraints are
conjunctions of constraints of the form c ∼ d for a clock c, an integer d, and
∼ ∈ {<, ≤, =, ≥, >}. We write u |= cc if the clock constraint cc holds for the
clock valuation u. We define a timed automaton A as a pair (T , I) where I is
a mapping from locations to clock constraints (also named invariants); and T
is a set of transitions written as A l −→
g,a,r l
where l and l
are start and
successor location, g is the guard of the transition, a is an action label, and r is
a list of clocks that will be reset to zero when the transition is taken. States of
timed automata are pairs of a location and a clock valuation. The operational
semantics defines two kinds of steps (given as their HOL descriptions):
– Delay: (l, u) →
d (l, u ⊕ d) if d ≥ 0 and u ⊕ d |= I l;
– Action: (l, u) → a (l
, [r := 0]u)
if A l −→
g,a,r l
, u |= g, and [r := 0]u |= I l
;
where u ⊕ d = (λc. u c + d) offsets all clocks by d in the valuation u, and
[r := 0]u = (λc. if c ∈ r then 0 else u c) resets all clocks in r to 0 in valuation u.
For any (timed) automaton A, we consider the transition system
(l, u) → A (l
, u
) = (∃d ≥ 0. ∃a u
. (l, u) →
d (l, u
) ∧ (l, u
) → a (l
, u
)) .
S. Wimmer and J. von Mutius
1 Timed Automata and Model Checking
Transition Systems We take a very simple view of transition systems: they are
simply a relation → of type
a ⇒
a ⇒ bool for a type of states
a. We write
a →
∗ b to denote that b can be reached from a via a sequence of →-transitions.
Timed Automata To make the paper self-contained, this paragraph briefly describes timed automata and is mostly reproduced from Wimmer and Lammich
[29]. For a thorough introduction see the tutorial paper of Bengtsson and Yi [4].
Compared to standard finite automata, timed automata introduce a notion
of clocks. Figure 1 depicts an example of a timed automaton. We will assume
that clocks are of type nat. A clock valuation u is a function of type nat ⇒ real .
Locations and transitions are guarded by clock constraints, which have to be
l 1
l 2
c 1 ≤ 1 ∧ c 2 ≤ 100
l 3
c 1 > 0, a 1 , c 2 := 0
a 3 , c 1 := c 2 := 0
a 2 , c 1 := 0
c 1 > 100, a 4
Fig. 1: Example of a timed automaton with two clocks.
fulfilled to stay in a location or to take a transition. Clock constraints are
conjunctions of constraints of the form c ∼ d for a clock c, an integer d, and
∼ ∈ {<, ≤, =, ≥, >}. We write u |= cc if the clock constraint cc holds for the
clock valuation u. We define a timed automaton A as a pair (T , I) where I is
a mapping from locations to clock constraints (also named invariants); and T
is a set of transitions written as A l −→
g,a,r l
where l and l
are start and
successor location, g is the guard of the transition, a is an action label, and r is
a list of clocks that will be reset to zero when the transition is taken. States of
timed automata are pairs of a location and a clock valuation. The operational
semantics defines two kinds of steps (given as their HOL descriptions):
– Delay: (l, u) →
d (l, u ⊕ d) if d ≥ 0 and u ⊕ d |= I l;
– Action: (l, u) → a (l
, [r := 0]u)
if A l −→
g,a,r l
, u |= g, and [r := 0]u |= I l
;
where u ⊕ d = (λc. u c + d) offsets all clocks by d in the valuation u, and
[r := 0]u = (λc. if c ∈ r then 0 else u c) resets all clocks in r to 0 in valuation u.
For any (timed) automaton A, we consider the transition system
(l, u) → A (l
, u
) = (∃d ≥ 0. ∃a u
. (l, u) →
d (l, u
) ∧ (l, u
) → a (l
, u
)) .