What's decidable about hybrid automata?

Henzinger TA, Kopke P, Puri A, Varaiya P. 1995. What’s decidable about hybrid automata? Proceedings of the 27th annual ACM symposium on Theory of computing. STOC: Symposium on the Theory of Computing, 373–382.


Conference Paper | Published | English
Author
Henzinger, Thomas AISTA ; Kopke, Peter; Puri, Anuj; Varaiya, P.
Abstract
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.
Publishing Year
Date Published
1995-01-01
Proceedings Title
Proceedings of the 27th annual ACM symposium on Theory of computing
Acknowledgement
We thank Howard Wong-Toi for a careful reading.
Page
373 - 382
Conference
STOC: Symposium on the Theory of Computing
Conference Location
Las Vegas, NV, United States of America
Conference Date
1995-05-29 – 1995-06-01
IST-REx-ID

Cite this

Henzinger TA, Kopke P, Puri A, Varaiya P. What’s decidable about hybrid automata? In: Proceedings of the 27th Annual ACM Symposium on Theory of Computing. ACM; 1995:373-382. doi:10.1145/225058.225162
Henzinger, T. A., Kopke, P., Puri, A., & Varaiya, P. (1995). What’s decidable about hybrid automata? In Proceedings of the 27th annual ACM symposium on Theory of computing (pp. 373–382). Las Vegas, NV, United States of America: ACM. https://doi.org/10.1145/225058.225162
Henzinger, Thomas A, Peter Kopke, Anuj Puri, and P. Varaiya. “What’s Decidable about Hybrid Automata?” In Proceedings of the 27th Annual ACM Symposium on Theory of Computing, 373–82. ACM, 1995. https://doi.org/10.1145/225058.225162.
T. A. Henzinger, P. Kopke, A. Puri, and P. Varaiya, “What’s decidable about hybrid automata?,” in Proceedings of the 27th annual ACM symposium on Theory of computing, Las Vegas, NV, United States of America, 1995, pp. 373–382.
Henzinger TA, Kopke P, Puri A, Varaiya P. 1995. What’s decidable about hybrid automata? Proceedings of the 27th annual ACM symposium on Theory of computing. STOC: Symposium on the Theory of Computing, 373–382.
Henzinger, Thomas A., et al. “What’s Decidable about Hybrid Automata?” Proceedings of the 27th Annual ACM Symposium on Theory of Computing, ACM, 1995, pp. 373–82, doi:10.1145/225058.225162.
All files available under the following license(s):
Copyright Statement:
This Item is protected by copyright and/or related rights. [...]

Link(s) to Main File(s)
Access Level
OA Open Access

Export

Marked Publications

Open Data ISTA Research Explorer

Search this title in

Google Scholar
ISBN Search