Timed formalisms: 6 - Timed Automata
Deterministic finite automaton augmented with a finite set of
The states of the automaton are called vertices and the
transitions (arcs, edges) are called switches.
Switches (edges) are instantaneous.
Time can elapse in locations.
A clock can be reset to zero simultaneously with any switch.
The reading of a clock equals the time elapsed since the last
time it was reset (time is global).