Timed Automata
Traditionally, finite automata have no mechanism to represent the
time taken between actions. However, in many specifications, we
need to model time. For instance, we may want to specify a
minimum and maximum delay between turning on a switch and its
effect being observed. In 1992, Alur and Dill introduced a model
of timed automata in which real-valued clocks are incorporated
into the state-transition structure of traditional automata in
such a way that some useful questions about the automata remain
computable. In this talk, we will introduce the Alur-Dill model
of timed automata and look at some technical issues involved in
analyzing these models.