---
_id: '4454'
abstract:
- lang: eng
  text: We define five increasingly comprehensive classes of infinite-state systems,
    called STS1--STS5, whose state spaces have finitary structure. For four of these
    classes, we provide examples from hybrid systems.STS1 These are the systems with
    finite bisimilarity quotients. They can be analyzed symbolically by iteratively
    applying predecessor and Boolean operations on state sets, starting from a finite
    number of observable state sets. Any such iteration is guaranteed to terminate
    in that only a finite number of state sets can be generated. This enables model
    checking of the μ-calculus.STS2 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.STS3 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 all ω-regular properties,
    including linear temporal logic.STS4 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.STS5 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 is a weaker
    termination condition than above). This enables model checking of reachability
    properties.
author:
- first_name: Thomas A
  full_name: Thomas Henzinger
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
- first_name: Ritankar
  full_name: Majumdar, Ritankar S
  last_name: Majumdar
- first_name: Jean
  full_name: Raskin, Jean-François
  last_name: Raskin
citation:
  ama: Henzinger TA, Majumdar R, Raskin J. A classification of symbolic transition
    systems. <i>ACM Transactions on Computational Logic (TOCL)</i>. 2005;6(1):1-32.
    doi:<a href="https://doi.org/10.1145/1042038.1042039">10.1145/1042038.1042039</a>
  apa: Henzinger, T. A., Majumdar, R., &#38; Raskin, J. (2005). A classification of
    symbolic transition systems. <i>ACM Transactions on Computational Logic (TOCL)</i>.
    ACM. <a href="https://doi.org/10.1145/1042038.1042039">https://doi.org/10.1145/1042038.1042039</a>
  chicago: Henzinger, Thomas A, Ritankar Majumdar, and Jean Raskin. “A Classification
    of Symbolic Transition Systems.” <i>ACM Transactions on Computational Logic (TOCL)</i>.
    ACM, 2005. <a href="https://doi.org/10.1145/1042038.1042039">https://doi.org/10.1145/1042038.1042039</a>.
  ieee: T. A. Henzinger, R. Majumdar, and J. Raskin, “A classification of symbolic
    transition systems,” <i>ACM Transactions on Computational Logic (TOCL)</i>, vol.
    6, no. 1. ACM, pp. 1–32, 2005.
  ista: Henzinger TA, Majumdar R, Raskin J. 2005. A classification of symbolic transition
    systems. ACM Transactions on Computational Logic (TOCL). 6(1), 1–32.
  mla: Henzinger, Thomas A., et al. “A Classification of Symbolic Transition Systems.”
    <i>ACM Transactions on Computational Logic (TOCL)</i>, vol. 6, no. 1, ACM, 2005,
    pp. 1–32, doi:<a href="https://doi.org/10.1145/1042038.1042039">10.1145/1042038.1042039</a>.
  short: T.A. Henzinger, R. Majumdar, J. Raskin, ACM Transactions on Computational
    Logic (TOCL) 6 (2005) 1–32.
date_created: 2018-12-11T12:08:56Z
date_published: 2005-01-01T00:00:00Z
date_updated: 2021-01-12T07:57:05Z
day: '01'
doi: 10.1145/1042038.1042039
extern: 1
fulldoi: https://doi.org/10.1145/1042038.1042039
intvolume: '         6'
issue: '1'
month: '01'
page: 1 - 32
publication: ACM Transactions on Computational Logic (TOCL)
publication_status: published
publisher: ACM
publist_id: '272'
quality_controlled: 0
status: public
title: A classification of symbolic transition systems
type: journal_article
volume: 6
year: '2005'
...