### 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]},

- $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

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

## No comments:

## Post a Comment