Timed Automata

Timed automata are finite state machines extended with real-valued clock variables that enable the modeling and verification of systems with quantitative timing constraints. Developed by Alur and Dill in the early 1990s, timed automata provided the first decidable framework for verifying real-time properties — properties that specify not merely what a system must do, but when it must do it. The decidability result is non-trivial: the continuous state space of clock variables would normally produce infinite state spaces, but the region construction — partitioning clock space into finitely many equivalence classes — restores decidability.

Timed automata are the formal foundation of real-time systems verification, implemented in tools like UPPAAL and Kronos. They can express deadlines, timeouts, and periodic behavior in a way that pure finite-state models cannot. The limitation is that timed automata assume perfect clocks and instantaneous transitions — assumptions that real hardware violates. The gap between the model and the machine is the frontier of current research in formal verification and hybrid systems.