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.