---
_id: '4492'
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 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.
acknowledgement: This research was supported in part by the Office of Naval Research
  Young Investigator Award N00014-95-1-0520, by the National Science Foundation CAREER
  award CCR-9501708, by the National Science Foundation Grant CCR-9504469, by the
  Air Force Office of Scientific Research Contract F49620-93-1-0056, by the Army Research
  Office MURI Grant DAAH-04-96-1-0341, by the Army Research Office Contract DAAH-04-94-G-0026,
  by the Defense Advanced Research Projects Agency Grant NAG2-892, and by the California
  PATH program.
article_processing_charge: No
article_type: original
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?
    <i>Journal of Computer and System Sciences</i>. 1998;57(1):94-124. doi:<a href="https://doi.org/10.1006/jcss.1998.1581">10.1006/jcss.1998.1581</a>
  apa: Henzinger, T. A., Kopke, P., Puri, A., &#38; Varaiya, P. (1998). What’s decidable
    about hybrid automata? <i>Journal of Computer and System Sciences</i>. Elsevier.
    <a href="https://doi.org/10.1006/jcss.1998.1581">https://doi.org/10.1006/jcss.1998.1581</a>
  chicago: Henzinger, Thomas A, Peter Kopke, Anuj Puri, and P. Varaiya. “What’s Decidable
    about Hybrid Automata?” <i>Journal of Computer and System Sciences</i>. Elsevier,
    1998. <a href="https://doi.org/10.1006/jcss.1998.1581">https://doi.org/10.1006/jcss.1998.1581</a>.
  ieee: T. A. Henzinger, P. Kopke, A. Puri, and P. Varaiya, “What’s decidable about
    hybrid automata?,” <i>Journal of Computer and System Sciences</i>, vol. 57, no.
    1. Elsevier, pp. 94–124, 1998.
  ista: 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.
  mla: Henzinger, Thomas A., et al. “What’s Decidable about Hybrid Automata?” <i>Journal
    of Computer and System Sciences</i>, vol. 57, no. 1, Elsevier, 1998, pp. 94–124,
    doi:<a href="https://doi.org/10.1006/jcss.1998.1581">10.1006/jcss.1998.1581</a>.
  short: T.A. Henzinger, P. Kopke, A. Puri, P. Varaiya, Journal of Computer and System
    Sciences 57 (1998) 94–124.
date_created: 2018-12-11T12:09:08Z
date_published: 1998-01-01T00:00:00Z
date_updated: 2022-08-23T14:29:15Z
day: '01'
doi: 10.1006/jcss.1998.1581
extern: '1'
intvolume: '        57'
issue: '1'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://www.sciencedirect.com/science/article/pii/S0022000098915811
month: '01'
oa: 1
oa_version: Published Version
page: 94 - 124
publication: Journal of Computer and System Sciences
publication_identifier:
  isbn:
  - 0022-0000
publication_status: published
publisher: Elsevier
publist_id: '237'
quality_controlled: '1'
status: public
title: What's decidable about hybrid automata?
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 57
year: '1998'
...