What's decidable about hybrid automata?

T.A. Henzinger, P. Kopke, A. Puri, P. Varaiya, Journal of Computer and System Sciences 57 (1998) 94–124.

Download
No fulltext has been uploaded. References only!

Journal Article | Published
Author
; ; ;
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 a boundary between decidability and undecidability for the reachability problem of 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 independent 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ω-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
1998-01-01
Journal Title
Journal of Computer and System Sciences
Volume
57
Issue
1
Page
94 - 124
IST-REx-ID

Cite this

Henzinger TA, Kopke P, Puri A, Varaiya P. What’s decidable about hybrid automata? Journal of Computer and System Sciences. 1998;57(1):94-124. doi:10.1006/jcss.1998.1581
Henzinger, T. A., Kopke, P., Puri, A., & Varaiya, P. (1998). What’s decidable about hybrid automata? Journal of Computer and System Sciences, 57(1), 94–124. https://doi.org/10.1006/jcss.1998.1581
Henzinger, Thomas A, Peter Kopke, Anuj Puri, and P. Varaiya. “What’s Decidable about Hybrid Automata?” Journal of Computer and System Sciences 57, no. 1 (1998): 94–124. https://doi.org/10.1006/jcss.1998.1581.
T. A. Henzinger, P. Kopke, A. Puri, and P. Varaiya, “What’s decidable about hybrid automata?,” Journal of Computer and System Sciences, vol. 57, no. 1, pp. 94–124, 1998.
Henzinger TA, Kopke P, Puri A, Varaiya P. 1998. What’s decidable about hybrid automata? Journal of Computer and System Sciences. 57(1), 94–124.
Henzinger, Thomas A., et al. “What’s Decidable about Hybrid Automata?” Journal of Computer and System Sciences, vol. 57, no. 1, Elsevier, 1998, pp. 94–124, doi:10.1006/jcss.1998.1581.

Export

Marked Publications

Open Data IST Research Explorer

Search this title in

Google Scholar