Up to Topics
Previous
NextTimed 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 ∈ Tk, ds(t)/dt = a,
where a is the rate of the clock and Tk ⊂ 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.