The Theory of Hybrid Automata

2 min read

An invited survey of the theory of hybrid automata, the standard model for a digital controller driving an analogue plant. Control modes are graph vertices, each with a flow condition (a differential equation or inclusion) and an invariant; control switches are edges with jump conditions that reset continuous variables. Henzinger collects which verification questions can be decided for which subclasses, and how symbolic state-space computation works when the state space is uncountable.

Findings

  • The running example is a thermostat: in mode Off the temperature follows x’ = -0.1x, in mode On x’ = 5 − 0.1x, starting at 20 degrees, with switches guarded by thresholds such as x < 19.
  • Rectangular automata (each derivative ranges over a fixed interval that does not change with the mode, and variables are decoupled) are the decidability frontier. A drifting clock fits: its rate lies in [1 − ε, 1 + ε]. Their time-abstract traces are regular, emptiness is in PSPACE and time-abstract trace inclusion is decidable in EXPSPACE.
  • Step past that line and reachability becomes undecidable: letting flow bounds change with the mode, relating different variables, or adding a single stopwatch to clocks is enough.
  • For linear hybrid automata, symbolic reachability with linear predicates is still possible, as a procedure that may not terminate.

Limits

  • Exact verification works for very simple dynamics. A quadrotor or a vessel in waves is far outside the decidable classes, so practice relies on over-approximation and reachability tools.
  • A theory survey with no case study of a real controller. I read the 1996 Berkeley technical report version, which matches the LICS paper.

Relevance

Every claim that a robot controller “provably stays safe” rests on a hybrid model like this one, and the undecidability results explain why most robot safety arguments end up as runtime checks instead (Simplex, SOTER). It follows timed automata; see safe control and runtime monitoring.