Timed Automata

In the context of automata theory, a timed automata is a finite state machine extended with a finite set of real-valued clock, which is used to model the behavior of the system components over time.

The transitions are labeled with a guard which determines the condition on the clocks in order to change the state; a word $w$ that has to be read, and a set of clocks to reset when transitioning.

The state of a timed automata is a pair composed by a location node $\ell$ and a clock assignment.

The automata below accepts the alphabet $\{a,b\}$, and:

• The transition from $q_0$ to $q_1$ happens when the letter $a$ is read, and it resets the clock $x$ (indicated by the clock reset $\{x\}$);
• The self-loop in $q_0$ happens when we the letter $b$ is read, and it doesn’t change the state of the clocks.
• The transition from $q_1$ to $q_0$ happens when the letter $b$ is read and when the clock constraint $x<1$ is satisfied. It doesn’t change the state of the clocks.
• The self-loop in $q_1$ happens when we the letter $a$ is read, and it doesn’t change the state of the clocks. The timed automata we just described recognizes words over the alphabet $\{a,b\}$ where each occurrence of $a$ is followed by an occurrence of $b$ after less than a time unit (because the clock condition $x<1$).

---

tag: automata