A Glimpse of Timed Automata

Terms

Timed Automaton Intuitively, an automaton with clocks, the transitions from state to state are constrained by time. Formally, $A = (L, L^0, \Sigma, X, I, E)$, respectively the set of locations (states), the set of initial locations, labels, clocks, invariants, the set of edges (transitions) $$E = \{ (s, a, \varphi, \lambda, s') | s,s' \in L, a \in \Sigma, \varphi \text{:clock constraints}, \lambda \subseteq X \}$$

Clock a stopwatch in this context, i.e. clocks are to measure the elapsed time, it can be reset.

Guard Boolean comparison between the clock and some integer value, serves as a constraint for the switch from one location to another

Action the label of transition, used to synchronize actions among several timed automata

Reset set the clock to time 0 and meanwhile the clock starts ticking again

Invariant a time constraint residing inside the state which must be respected when staying within such state, otherwise, it must move out.

Deadlock cases are, there are no more allowed moves (due to bad design of automata).

Example

We quote an automaton from this slide ^[1],

Figure 1. An Example Timed Automaton

• $s_i$'s are state labels
• two clocks present $x$, $y$
• after action $a$, it can only stay in $s_1$ for no more than $1$ time unit
• action $d$ can occur only when clock $y$ reads more than $2$ (due to the guard $y>2$)

References

1. R. Sebastiani, Timed and Hybrid Systems: Formal Modeling and Verification, slides of Formal Methods course, 2012