A Classification of Symbolic Transition Systems


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.