---
res:
bibo_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.@eng
bibo_authorlist:
- foaf_Person:
foaf_givenName: Thomas A
foaf_name: Thomas Henzinger
foaf_surname: Henzinger
foaf_workInfoHomepage: http://www.librecat.org/personId=40876CD8-F248-11E8-B48F-1D18A9856A87
orcid: 0000−0002−2985−7724
- foaf_Person:
foaf_givenName: Peter
foaf_name: Kopke, Peter W
foaf_surname: Kopke
- foaf_Person:
foaf_givenName: Anuj
foaf_name: Puri, Anuj
foaf_surname: Puri
- foaf_Person:
foaf_givenName: P.
foaf_name: Varaiya,P.
foaf_surname: Varaiya
bibo_doi: 10.1145/225058.225162
dct_date: 1995^xs_gYear
dct_publisher: ACM@
dct_title: What's decidable about hybrid automata?@
...