Timed Automata

Deterministic finite automaton augmented with a finite set of

(real- valued) clocks.

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).