## What's Decidable about Hybrid Automata?

*
Thomas A. Henzinger,
Peter W. Kopke, Anuj Puri, and Pravin Varaiya*

Hybrid automata model systems with both digital and analog components, such
as embedded control programs.
Many verification tasks for such programs can be expressed as reachability
problems for hybrid automata.
By improving on previous decidability and undecidability results, we identify
the precise boundary between decidability and undecidability of the
reachability problem for hybrid automata.

On the positive side, we give an (optimal) PSPACE reachability algorithm for
the case of initialized rectangular automata, where all analog variables
follow trajectories within piecewise-linear envelopes and are reinitialized
whenever the envelope changes.
Our algorithm is based on the construction of a timed automaton that contains
all reachability information about a given initialized rectangular automaton.
The translation has practical significance for verification, because it
guarantees the termination of symbolic procedures for the reachability
analysis of initialized rectangular automata.
The translation also preserves the omega-languages of initialized rectangular
automata with bounded nondeterminism.

On the negative side, we show that several slight generalizations of
initialized rectangular automata lead to an undecidable reachability problem.
In particular, we prove that the reachability problem is undecidable for
timed automata augmented with a single stopwatch.

*Journal of Computer and System Sciences* 57:94-124, 1998.
A preliminary version appeared in the
*Proceedings of the
27th Annual Symposium on Theory of Computing*
(STOC), ACM Press, 1995, pp. 373-382.

Download inofficial, sometimes updated
PostScript /
PDF document.
© 1995 ACM,
1998 Elsevier.