A Theory of Timed Automata

2 min read

Alur and Dill add real-valued clocks to finite automata. Each clock measures time since it was last reset, and each transition can carry a guard on clock values (for example “take this edge only if x < 2”). The automaton reads timed words, sequences of events stamped with real times. The main result is the region construction: the infinite clock space can be cut into finitely many equivalence classes, so checking whether a timed automaton accepts anything is decidable, in PSPACE.

Findings

  • Nondeterministic timed automata are closed under union and intersection but not under complement. Deterministic timed Muller automata are closed under all Boolean operations.
  • Emptiness is decidable (PSPACE). Universality and language inclusion are undecidable for the nondeterministic case and PSPACE-complete for the deterministic one.
  • The verification example is a railroad crossing with train, gate and controller components. The train signals at least 2 minutes before entering and the gate closes within 1 minute of “lower”. Two properties are checked: the gate is closed whenever the train is inside the crossing (safety), and the gate is never closed for more than 10 minutes at a stretch (real-time liveness). The authors point out that the safety property, though untimed, fails if the timing requirements are dropped.
  • The paper lists follow-on results: decision procedures for MITL and model checking for TCTL both reduce to this construction.

Limits

  • Clocks all run at rate 1. Anything with richer continuous dynamics needs hybrid automata, where decidability is mostly lost.
  • Undecidable inclusion means you cannot, in general, check a nondeterministic timed model against a nondeterministic timed specification. The paper’s verification procedure therefore takes the specification as a deterministic timed automaton.
  • I read the abstract, introduction, verification section and the summary of later results, and skipped the proofs.

Relevance

Timeouts in robot safety logic are timed automata in all but name, and UPPAAL-style checks of them rest on this paper. It is the model behind timed specifications in Luckcuck et al.’s survey and behind timed monitors like TLTL. See runtime monitoring and robust robotics.