---
_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: *Proceedings of the 17th Annual Symposium on Theoretical Aspects of Computer
Science*. Vol 1770. Springer; 2000:13-34. doi:10.1007/3-540-46541-3_2'
apa: 'Henzinger, T. A., & Majumdar, R. (2000). A classification of symbolic
transition systems. In *Proceedings of the 17th Annual Symposium on Theoretical
Aspects of Computer Science* (Vol. 1770, pp. 13–34). Lille, France: Springer.
https://doi.org/10.1007/3-540-46541-3_2'
chicago: Henzinger, Thomas A, and Ritankar Majumdar. “A Classification of Symbolic
Transition Systems.” In *Proceedings of the 17th Annual Symposium on Theoretical
Aspects of Computer Science*, 1770:13–34. Springer, 2000. https://doi.org/10.1007/3-540-46541-3_2.
ieee: T. A. Henzinger and R. Majumdar, “A classification of symbolic transition
systems,” in *Proceedings of the 17th Annual Symposium on Theoretical Aspects
of Computer Science*, 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.” *Proceedings of the 17th Annual Symposium on Theoretical
Aspects of Computer Science*, vol. 1770, Springer, 2000, pp. 13–34, doi:10.1007/3-540-46541-3_2.
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'
...