---
res:
bibo_abstract:
- 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.@eng
bibo_authorlist:
- foaf_Person:
foaf_givenName: Thomas A
foaf_name: Thomas Henzinger
foaf_surname: Henzinger
foaf_workInfoHomepage: http://www.librecat.org/personId=40876CD8-F248-11E8-B48F-1D18A9856A87
orcid: 0000−0002−2985−7724
- foaf_Person:
foaf_givenName: Ritankar
foaf_name: Majumdar, Ritankar S
foaf_surname: Majumdar
- foaf_Person:
foaf_givenName: Jean
foaf_name: Raskin, Jean-François
foaf_surname: Raskin
bibo_doi: 10.1145/1042038.1042039
bibo_issue: '1'
bibo_volume: 6
dct_date: 2005^xs_gYear
dct_publisher: ACM@
dct_title: A classification of symbolic transition systems@
...