# Timed Automata

**Timed automata** are simple continuous-time hybrid systems where the passage
of time triggers events. The mode refinements are **clocks**, which are first-order
differential equations as follows:

for all *t* ∈
*T _{k},
ds*(

*t*)/

*dt*=

*a,*

where *a* is the rate of the clock and *T _{k}*
⊂

*Time*is the subset of time where the system is in mode

*k*.

Consider the **tick generator** example below:

This generates a *tick* output at times 1, 3, 4, 6, 7, 9, 10, .... It
spends one time unit in *mode 1*, then transitions to *mode 2*, where
it spends two time units, and then transitions back to *mode 1*. So at
any time *t *the state of *tickGenerator* is the pair (*mode*(*t*),
*s*(*t*)). The actions on the transitions set *s* to zero.

Notice that there are no inputs. None are needed because, conceptually, this machine is reacting continually, at all times.