*
Thomas A. Henzinger,
Rupak Majumdar, and Jean-Francois Raskin*

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.

**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 mu-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
mu-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 omega-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 mu-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.

*ACM Transactions on Computational Logic* 6:1-32, 2005.
A preliminary version appeared in the
*Proceedings of the
17th International Conference on Theoretical Aspects of Computer Science*
(STACS),
Lecture Notes in Computer Science 1770,
Springer, 2000, pp. 13-34.

Download inofficial, sometimes updated PostScript / PDF document. © 2000 Springer, 2005 ACM.