Hybrid Automata

Origin. Rajeev Alur, Costas Courcoubetis, Thomas Henzinger, and Pei-Hsin Ho, "Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems" (Hybrid Systems, LNCS 736, 1993, 209–229), defined the model; the nine-author sequel with Nicolas Halbwachs, Xavier Nicollin, Alfredo Olivero, Joseph Sifakis, and Sergio Yovine, "The algorithmic analysis of hybrid systems" (Theoretical Computer Science 138, 1995, 3–34), fixed the linear class and its symbolic analysis. Thomas Henzinger, "The theory of hybrid automata" (LICS 1996, 278–292), is the consolidated statement. The decidability frontier is Thomas Henzinger, Peter Kopke, Anuj Puri, and Pravin Varaiya, "What's decidable about hybrid automata?" (STOC 1995, 373–382; Journal of Computer and System Sciences 57, 1998, 94–124), and its o-minimal side is Gerardo Lafferriere, George Pappas, and Shankar Sastry, "O-minimal hybrid systems" (Mathematics of Control, Signals, and Systems 13, 2000, 1–21).

Models. A machine, admitted the way Timed Automata is: as the semantic object the verification questions are asked of. A hybrid automaton is a finite control graph over real-valued variables: each mode carries a flow condition — a differential inclusion the variables obey while control stays in the mode — and an invariant bounding how long it may stay; each edge carries a guard and a reset. A state is a mode paired with a point of ℝⁿ, a run alternates continuous flows with discrete jumps, and the intended model is embedded control, where a program switches the differential equations of a plant. Reachability is the central problem — safety verification is its complement — and it is undecidable in general; the content of the theory is the exact position of the decidable boundary, which lies barely above timed automata.

Formalism.

Hybrid automaton (Alur–Courcoubetis–Henzinger–Ho 1993; Henzinger 1996): H = (X, V, E, init, inv, flow, jump): variables, modes, edges, and conditions attached to modes and edges. flow(v): a constraint on X ∪ Ẋ — the differential inclusion governing trajectories in mode v. inv(v): the region control may occupy in v; init(v): where runs may start. jump(e): a guard on the variables and a reset relating their values before and after the edge. Run: alternating flow steps (a trajectory satisfying flow(v) inside inv(v)) and jump steps (an edge whose guard holds, reset applied); jumps take no time. Reachability: whether a run from init reaches a given state.

The classes, by what flows and jumps may say: Timed automaton: ẋ = 1 for every variable; guards compare variables with constants; resets to 0. Stopwatch automaton: ẋ ∈ {0, 1} — clocks that pause. Rectangular automaton: ẋ ∈ [l, u] per variable; init, inv, guards, and resets all products of intervals. Initialized: whenever an edge changes a variable's flow interval, it resets that variable. Linear hybrid automaton: all conditions linear constraints; flow conditions mention Ẋ only, so each mode allows a polyhedron of slopes. O-minimal hybrid system: flows, guards, and resets definable in an o-minimal structure; every edge resets the whole continuous state (see O-Minimality).

The frontier (Henzinger–Kopke–Puri–Varaiya, STOC 1995; JCSS 1998): Initialized rectangular automata: reachability PSPACE-complete, by a translation into timed automata that preserves ω-languages. Uninitialized rectangular, or non-rectangular: undecidable. One stopwatch added to a timed automaton: reachability undecidable, by encoding two-counter machines. The same boundary, recorded from the timed side, in Timed Automata.

O-minimal decidability (Lafferriere–Pappas–Sastry 2000): Every o-minimal hybrid system admits a finite bisimulation. The quotient is computable when the o-minimal theory is decidable: semialgebraic data via real closed fields; data needing exp waits on the decidability of Th(ℝ_exp), which is open (see O-Minimality). Two routes to a finite abstraction (Alur–Henzinger–Lafferriere–Pappas 2000): constrain the dynamics, as in timed and rectangular automata, or admit o-minimal dynamics and make every jump forget the continuous state.

Symbolic analysis (Alur et al. 1995; Alur–Henzinger–Ho, IEEE TSE 22, 1996): For linear hybrid automata, post maps polyhedra to polyhedra and is computable. Iterating post from init is a semi-algorithm: every answer is correct, and termination is not guaranteed — reachability stays undecidable. HyTech implements the iteration (Henzinger–Ho–Wong-Toi 1997), with linear hybrid automata as input and polyhedra as the data structure.

Symbols.

Symbol	Unicode	Name	Meaning
ẋ	—	Dotted variable	The time derivative of x, the subject of flow conditions
ℝ	U+211D	Double-struck R / Reals	The variables range over ℝ; a state is a mode with a point of ℝⁿ
∈	U+2208	Element of	Differential inclusion, ẋ ∈ [l, u]
ω	U+03C9	Omega (small)	The ω-languages preserved by the HKPV translation
X	—	Variable set	The finitely many real-valued variables
V, E	—	Modes and edges	The control graph
flow, inv	—	Flow and invariant	The per-mode conditions
init, jump	—	Initial and jump conditions	The start states and the per-edge guard with reset
[l, u]	—	Slope interval	The admissible derivatives of a rectangular variable
post	—	Successor operator	Maps a region to the states reachable in one flow or jump
H	—	Hybrid automaton	The structure (X, V, E, init, inv, flow, jump)

Metatheory. Henzinger, Kopke, Puri, and Varaiya (1995, journal 1998) proved reachability for initialized rectangular automata PSPACE-complete, by translating the automaton into a timed automaton that preserves its ω-language, with hardness inherited from timed automata; and they proved the hypotheses minimal: dropping initialization makes reachability undecidable, as does a non-rectangular constraint, as does one stopwatch added to a timed automaton — the two-counter encodings recorded in Timed Automata. General undecidability follows a fortiori, so every analysis of the full model is a semi-algorithm or an approximation. Lafferriere, Pappas, and Sastry (2000) proved that every o-minimal hybrid system admits a finite bisimulation, so a finite quotient preserves the temporal-logic properties (Alur, Henzinger, Lafferriere, and Pappas, Proceedings of the IEEE 88, 2000, 971–984), and reachability is decidable whenever the o-minimal theory is — for semialgebraic systems by Tarski's decision procedure for real closed fields. For linear hybrid automata, the 1995 Theoretical Computer Science paper gave the computable post operator and the model-checking semi-algorithms the tools run.

Applies to. Verification of embedded controllers and of plants switched by programs. Timing and mode-switching models of plants and protocols, written as linear hybrid automata. The decidable envelopes of real-time verification: timed and initialized rectangular analysis (Timed Automata), semialgebraic o-minimal systems. Duration properties of real-time behaviour, checked against the automaton (Duration Calculus). Reachability computation for switched continuous systems.

Limitations. Reachability is undecidable, and the undecidability begins one stopwatch above timed automata, so the decidable classes are thin. Initialization — resetting a variable whenever its law changes — is exactly what severs the memory between modes that the two-counter encodings need; the o-minimal route severs it completely, resetting everything at every jump, so no variable carries its value across a mode change. The symbolic analysis of linear hybrid automata terminates on no general class, and a run of the iteration that has not stopped carries no information. Rectangular flows bound derivatives by constants, so real dynamics enter only through abstraction: a nonlinear plant must be over-approximated before the theory applies, and the verdict is about the abstraction. The semantics admits Zeno runs — infinitely many jumps in bounded time — and excluding them is a side condition the modeller imposes. Decidability of the o-minimal class is conditional on the decidability of the underlying theory, which for the exponential field is open.