Timed Automata

Origin. Rajeev Alur and David Dill, "Automata for modeling real-time systems" (ICALP 1990), in journal form "A theory of timed automata" (Theoretical Computer Science 126, 1994, 183–235): finite automata over infinite words augmented with real-valued clocks, guards comparing clocks to constants, and resets. The companion logic is TCTL: Rajeev Alur, Costas Courcoubetis, and David Dill, "Model-checking in dense real-time" (Information and Computation 104, 1993, 2–34). David Dill, "Timing assumptions and verification of finite-state concurrent systems" (CAV 1989), supplied the zone and difference-bound-matrix machinery the implementations run on.

Models. A machine, admitted here the way Büchi automata are: as the semantic apparatus of a logic family rather than a logic. MITL formulas compile into timed automata, TCTL is checked over them, and the decidability results of real-time logic are results about the automaton. A model of behaviour is a timed word — events paired with nondecreasing, diverging real timestamps; a configuration is a location together with a clock valuation; time elapses in the valuation, and transitions test guards and reset clocks. The state space is uncountable, and the theory's central result is that a finite quotient of it — the regions — decides reachability.

Formalism.

Timed automaton: A = (Σ, S, S₀, C, E): alphabet, locations, start locations, clocks, edges. Edge (s, s′, a, λ, φ): reads a, resets the clocks in λ to 0, enabled when the constraint φ holds. Clock constraints: Boolean combinations of x ≤ c and c ≤ x, with c rational — integral after scaling. Timed word: (σ₀, τ₀)(σ₁, τ₁)…, timestamps τᵢ nondecreasing and divergent. Timed Büchi automaton: a Büchi condition on the locations; timed Muller likewise.

Region equivalence (Alur–Dill 1994): ν ≈ ν′ iff the valuations agree on the integer parts of all clocks up to the largest constant, and on the ordering of the fractional parts. Finitely many classes: exponential in the number of clocks and in the encoding of the constants. Region automaton: the quotient is a finite automaton accepting Untime(L(A)).

Decidability (Alur–Dill 1994): Emptiness and reachability: PSPACE-complete. Universality and timed language inclusion: undecidable for nondeterministic automata — Π¹₁-hard. Closure: union and intersection yes, complement no. Deterministic timed Muller automata: a proper subclass closed under all Boolean operations.

One clock (Ouaknine–Worrell 2004): L(B) ⊆ L(A) is decidable when A has at most one clock, by a well-quasi-order argument. Undecidable again over infinite timed words. One-clock alternating timed automata decide MTL over finite timed words — the connection worked out in Metric Temporal Logic.

TCTL (Alur–Courcoubetis–Dill 1993): φ ::= p | ¬φ | φ ∧ φ | ∃φ U∼c φ | ∀φ U∼c φ, with ∼ one of <, ≤, =, ≥, >. CTL with time bounds on the path quantifiers, interpreted over the dense computation trees of a timed automaton. Model checking: PSPACE-complete, already with one clock. Satisfiability: Π¹₁-hard — validity is not recursively enumerable, so no complete finitary axiomatization exists.

Zones (Dill 1989): Zone: a conjunction of constraints x ∼ c and x − y ∼ c — a convex polyhedron. Difference bound matrix: the zone as a weighted graph; canonical form by all-pairs shortest paths; intersection, time elapse, reset, inclusion, emptiness all on the matrix. Forward reachability on zones with extrapolation is the algorithm of practice; UPPAAL is where it is practised.

The boundary (Henzinger–Kopke–Puri–Varaiya, STOC 1995; JCSS 1998): All clocks advance at rate 1. Let one clock stop and resume — a stopwatch — and reachability is undecidable, by encoding two-counter machines. Initialized rectangular hybrid automata: still PSPACE. Uninitialized, or non-rectangular: undecidable.

Symbols.

Metatheory. Alur and Dill (1994) proved emptiness PSPACE-complete by the region construction, with hardness by reduction from linear bounded automata, and proved universality and timed language inclusion Π¹₁-hard, so nondeterministic timed automata are not closed under complement and specifications cannot in general be automata. Alur, Courcoubetis, and Dill (1993) proved TCTL model checking PSPACE-complete and TCTL satisfiability Π¹₁-hard over dense time. Henzinger, Kopke, Puri, and Varaiya (1995, journal 1998) drew the boundary of the model itself: one stopwatch added to a timed automaton makes reachability undecidable, and initialized rectangular automata are the decidable envelope, at PSPACE. Ouaknine and Worrell (2004) closed the inclusion gap from below: one-clock inclusion is decidable over finite timed words, undecidable over infinite ones, and the one-clock alternating machinery yields the decidability of MTL over finite timed words recorded in Metric Temporal Logic. On the logic side the compilation of MITL into timed automata (Alur, Feder, Henzinger 1996) places MITL satisfiability in EXPSPACE; each of these bounds is obtained through the region construction.

Applies to. Model checking of real-time systems; UPPAAL. Decision procedures for MITL and the decidable MTL fragments. TCTL verification of embedded controllers. Timing analysis of circuits and protocols. Schedulability analysis.

Limitations. No complementation and undecidable inclusion: a specification cannot be an arbitrary timed automaton checked by product and emptiness, which is the Büchi-automata workflow, so specifications must be deterministic, one-clock, or arrive through a decidable logic. The region graph is exponential in the number of clocks and in the size of the constants, the PSPACE lower bound says this is not an artifact, and zones improve the practice while the worst case stands. Guards compare clocks with rational constants only; the clean decidability ends at the model's own edge, since a single stopwatch, or uninitialized rate changes, encode two-counter machines. The one-clock decidability of inclusion does not survive the passage to infinite words. And the model idealizes: clocks are exact reals and transitions instantaneous.

© 2026 Lingenic LLC