---
_id: '4502'
abstract:
- lang: eng
  text: "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.\r\n\r\nOn
    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.\r\n\r\nOn 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."
acknowledgement: "We thank Howard Wong-Toi for a careful reading.\r\n"
article_processing_charge: No
author:
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
- first_name: Peter
  full_name: Kopke, Peter
  last_name: Kopke
- first_name: Anuj
  full_name: Puri, Anuj
  last_name: Puri
- first_name: P.
  full_name: Varaiya, P.
  last_name: Varaiya
citation:
  ama: 'Henzinger TA, Kopke P, Puri A, Varaiya P. What’s decidable about hybrid automata?
    In: <i>Proceedings of the 27th Annual ACM Symposium on Theory of Computing</i>.
    ACM; 1995:373-382. doi:<a href="https://doi.org/10.1145/225058.225162">10.1145/225058.225162</a>'
  apa: 'Henzinger, T. A., Kopke, P., Puri, A., &#38; Varaiya, P. (1995). What’s decidable
    about hybrid automata? In <i>Proceedings of the 27th annual ACM symposium on Theory
    of computing</i> (pp. 373–382). Las Vegas, NV, United States of America: ACM.
    <a href="https://doi.org/10.1145/225058.225162">https://doi.org/10.1145/225058.225162</a>'
  chicago: Henzinger, Thomas A, Peter Kopke, Anuj Puri, and P. Varaiya. “What’s Decidable
    about Hybrid Automata?” In <i>Proceedings of the 27th Annual ACM Symposium on
    Theory of Computing</i>, 373–82. ACM, 1995. <a href="https://doi.org/10.1145/225058.225162">https://doi.org/10.1145/225058.225162</a>.
  ieee: T. A. Henzinger, P. Kopke, A. Puri, and P. Varaiya, “What’s decidable about
    hybrid automata?,” in <i>Proceedings of the 27th annual ACM symposium on Theory
    of computing</i>, Las Vegas, NV, United States of America, 1995, pp. 373–382.
  ista: '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.'
  mla: Henzinger, Thomas A., et al. “What’s Decidable about Hybrid Automata?” <i>Proceedings
    of the 27th Annual ACM Symposium on Theory of Computing</i>, ACM, 1995, pp. 373–82,
    doi:<a href="https://doi.org/10.1145/225058.225162">10.1145/225058.225162</a>.
  short: T.A. Henzinger, P. Kopke, A. Puri, P. Varaiya, in:, Proceedings of the 27th
    Annual ACM Symposium on Theory of Computing, ACM, 1995, pp. 373–382.
conference:
  end_date: 1995-06-01
  location: Las Vegas, NV, United States of America
  name: 'STOC: Symposium on the Theory of Computing'
  start_date: 1995-05-29
date_created: 2018-12-11T12:09:11Z
date_published: 1995-01-01T00:00:00Z
date_updated: 2022-06-09T14:40:29Z
day: '01'
doi: 10.1145/225058.225162
extern: '1'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://dl.acm.org/doi/10.1145/225058.225162
month: '01'
oa: 1
oa_version: Published Version
page: 373 - 382
publication: Proceedings of the 27th annual ACM symposium on Theory of computing
publication_identifier:
  isbn:
  - '9780897917186'
publication_status: published
publisher: ACM
publist_id: '228'
quality_controlled: '1'
status: public
title: What's decidable about hybrid automata?
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
year: '1995'
...