---
_id: '4439'
abstract:
- lang: eng
  text: "We define five increasingly comprehensive classes of infinite-state systems,
    called STS1–5, whose state spaces have finitary structure. For four of these classes,
    we provide examples from hybrid systems.\r\nSTS1 These are the systems with finite
    bisimilarity quotients. They can be analyzed symbolically by (1) iterating the
    predecessor and boolean operations starting from a finite set of observable state
    sets, and (2) terminating when no new state sets are generated. This enables model
    checking of the μ-calculus.\r\nSTS2 These are the systems with finite similarity
    quotients. They can be analyzed symbolically by iterating the predecessor and
    positive boolean operations. This enables model checking of the existential and
    universal fragments of the μ-calculus.\r\nSTS3 These are the systems with finite
    trace-equivalence quotients. They can be analyzed symbolically by iterating the
    predecessor operation and a restricted form of positive boolean operations (intersection
    is restricted to intersection with observables). This enables model checking of
    linear temporal logic.\r\nSTS4 These are the systems with finite distance-equivalence
    quotients (two states are equivalent if for every distance d, the same observables
    can be reached in d transitions). The systems in this class can be analyzed symbolically
    by iterating the predecessor operation and terminating when no new state sets
    are generated. This enables model checking of the existential conjunction-free
    and universal disjunction-free fragments of the μ-calculus.\r\nSTS5 These are
    the systems with finite bounded-reachability quotients (two states are equivalent
    if for every distance d, the same observables can be reached in d or fewer transitions).
    The systems in this class can be analyzed symbolically by iterating the predecessor
    operation and terminating when no new states are encountered. This enables model
    checking of reachability properties."
acknowledgement: This research was supported in part by the DARPA (NASA) grant NAG2-1214,
  the DARPA (Wright-Patterson AFB) grant F33615-C-98-3614, the MARCO grant 98-DT-660,
  the ARO MURI grant DAAH-04-96-1-0341, and the NSF CAREER award CCR-9501708.
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: Ritankar
  full_name: Majumdar, Ritankar
  last_name: Majumdar
citation:
  ama: 'Henzinger TA, Majumdar R. A classification of symbolic transition systems.
    In: <i>Proceedings of the 17th Annual Symposium on Theoretical Aspects of Computer
    Science</i>. Vol 1770. Springer; 2000:13-34. doi:<a href="https://doi.org/10.1007/3-540-46541-3_2">10.1007/3-540-46541-3_2</a>'
  apa: 'Henzinger, T. A., &#38; Majumdar, R. (2000). A classification of symbolic
    transition systems. In <i>Proceedings of the 17th Annual Symposium on Theoretical
    Aspects of Computer Science</i> (Vol. 1770, pp. 13–34). Lille, France: Springer.
    <a href="https://doi.org/10.1007/3-540-46541-3_2">https://doi.org/10.1007/3-540-46541-3_2</a>'
  chicago: Henzinger, Thomas A, and Ritankar Majumdar. “A Classification of Symbolic
    Transition Systems.” In <i>Proceedings of the 17th Annual Symposium on Theoretical
    Aspects of Computer Science</i>, 1770:13–34. Springer, 2000. <a href="https://doi.org/10.1007/3-540-46541-3_2">https://doi.org/10.1007/3-540-46541-3_2</a>.
  ieee: T. A. Henzinger and R. Majumdar, “A classification of symbolic transition
    systems,” in <i>Proceedings of the 17th Annual Symposium on Theoretical Aspects
    of Computer Science</i>, Lille, France, 2000, vol. 1770, pp. 13–34.
  ista: 'Henzinger TA, Majumdar R. 2000. A classification of symbolic transition systems.
    Proceedings of the 17th Annual Symposium on Theoretical Aspects of Computer Science.
    STACS: Theoretical Aspects of Computer Science, LNCS, vol. 1770, 13–34.'
  mla: Henzinger, Thomas A., and Ritankar Majumdar. “A Classification of Symbolic
    Transition Systems.” <i>Proceedings of the 17th Annual Symposium on Theoretical
    Aspects of Computer Science</i>, vol. 1770, Springer, 2000, pp. 13–34, doi:<a
    href="https://doi.org/10.1007/3-540-46541-3_2">10.1007/3-540-46541-3_2</a>.
  short: T.A. Henzinger, R. Majumdar, in:, Proceedings of the 17th Annual Symposium
    on Theoretical Aspects of Computer Science, Springer, 2000, pp. 13–34.
conference:
  end_date: 2000-02-19
  location: Lille, France
  name: 'STACS: Theoretical Aspects of Computer Science'
  start_date: 2000-02-17
date_created: 2018-12-11T12:08:51Z
date_published: 2000-01-01T00:00:00Z
date_updated: 2023-04-18T13:02:39Z
day: '01'
doi: 10.1007/3-540-46541-3_2
extern: '1'
intvolume: '      1770'
language:
- iso: eng
month: '01'
oa_version: None
page: 13 - 34
publication: Proceedings of the 17th Annual Symposium on Theoretical Aspects of Computer
  Science
publication_identifier:
  isbn:
  - '9783540671411'
publication_status: published
publisher: Springer
publist_id: '292'
quality_controlled: '1'
scopus_import: '1'
status: public
title: A classification of symbolic transition systems
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 1770
year: '2000'
...