---
_id: '4443'
abstract:
- lang: eng
  text: "Three natural equivalence relations on the infinite state space of a hybrid
    automaton are language equivalence, simulation equivalence, and bisimulation equivalence.
    When one of these equivalence relations has a finite quotient, certain model checking
    and controller synthesis problems are decidable. When bounds on the number of
    equivalence classes are obtained, bounds on the running times of model checking
    and synthesis algorithms follow as corollaries.\r\nWe characterize the time-abstract
    versions of these equivalence relations on the state spaces of rectangular hybrid
    automata (RHA), in which each continuous variable is a clock with bounded drift.
    These automata are useful for modeling communications protocols with drifting
    local clocks, and for the conservative approximation of more complex hybrid systems.
    Of our two main results, one has positive implications for automatic verification,
    and the other has negative implications. On the positive side, we find that the
    (finite) language equivalence quotient for RHA is coarser than was previously
    known by a multiplicative exponential factor. On the negative side, we show that
    simulation equivalence for RHA is equality (which obviously has an infinite quotient).\r\nOur
    main positive result is established by analyzing a subclass of timed automata,
    called one-sided timed automata (OTA), for which the language equivalence quotient
    is coarser than for the class of all timed automata. An exact characterization
    of language equivalence for OTA requires a distinction between synchronous and
    asynchronous definitions of (bi)simulation: if time actions are silent, then the
    induced quotient for OTA is coarser than if time actions (but not their durations)
    are visible."
acknowledgement: This research was supported in part by ONR Young Investigator award
  N00014-95-1-0520, by NSF CAREER award CCR-9501708, by NSF grant CCR-9504469, by
  Air Force Office of Scientific Research contract F49620-93-1-0056, by ARPA grant
  NAG2-892, and by the U.S. Army Research Office through the Mathematical Sciences
  Institute of Cornell University, Contract Number DAAL03-91-C-0027.
alternative_title:
- LNCS
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
citation:
  ama: 'Henzinger TA, Kopke P. State equivalences for rectangular hybrid automata.
    In: <i>7th International Conference on Concurrency Theory</i>. Vol 1119. Schloss
    Dagstuhl - Leibniz-Zentrum für Informatik; 1996:530-545. doi:<a href="https://doi.org/10.1007/3-540-61604-7_74">10.1007/3-540-61604-7_74</a>'
  apa: 'Henzinger, T. A., &#38; Kopke, P. (1996). State equivalences for rectangular
    hybrid automata. In <i>7th International Conference on Concurrency Theory</i>
    (Vol. 1119, pp. 530–545). Pisa, Italy: Schloss Dagstuhl - Leibniz-Zentrum für
    Informatik. <a href="https://doi.org/10.1007/3-540-61604-7_74">https://doi.org/10.1007/3-540-61604-7_74</a>'
  chicago: Henzinger, Thomas A, and Peter Kopke. “State Equivalences for Rectangular
    Hybrid Automata.” In <i>7th International Conference on Concurrency Theory</i>,
    1119:530–45. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 1996. <a href="https://doi.org/10.1007/3-540-61604-7_74">https://doi.org/10.1007/3-540-61604-7_74</a>.
  ieee: T. A. Henzinger and P. Kopke, “State equivalences for rectangular hybrid automata,”
    in <i>7th International Conference on Concurrency Theory</i>, Pisa, Italy, 1996,
    vol. 1119, pp. 530–545.
  ista: 'Henzinger TA, Kopke P. 1996. State equivalences for rectangular hybrid automata.
    7th International Conference on Concurrency Theory. CONCUR: Concurrency Theory,
    LNCS, vol. 1119, 530–545.'
  mla: Henzinger, Thomas A., and Peter Kopke. “State Equivalences for Rectangular
    Hybrid Automata.” <i>7th International Conference on Concurrency Theory</i>, vol.
    1119, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 1996, pp. 530–45, doi:<a
    href="https://doi.org/10.1007/3-540-61604-7_74">10.1007/3-540-61604-7_74</a>.
  short: T.A. Henzinger, P. Kopke, in:, 7th International Conference on Concurrency
    Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 1996, pp. 530–545.
conference:
  end_date: 1996-08-29
  location: Pisa, Italy
  name: 'CONCUR: Concurrency Theory'
  start_date: 1996-08-26
date_created: 2018-12-11T12:08:52Z
date_published: 1996-01-01T00:00:00Z
date_updated: 2022-07-06T08:43:23Z
day: '01'
doi: 10.1007/3-540-61604-7_74
extern: '1'
intvolume: '      1119'
language:
- iso: eng
main_file_link:
- url: https://link.springer.com/chapter/10.1007/3-540-61604-7_74
month: '01'
oa_version: None
page: 530 - 545
publication: 7th International Conference on Concurrency Theory
publication_identifier:
  isbn:
  - '9783540616047'
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '288'
quality_controlled: '1'
status: public
title: State equivalences for rectangular hybrid automata
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 1119
year: '1996'
...