Symbolic Exploration of Transition Hierarchies

Rajeev Alur, Thomas A. Henzinger, and Sriram K. Rajamani

In formal design verification, successful model checking is typically preceded by a laborious manual process of constructing design abstractions. We present a methodology for partially--and in some cases, fully--bypassing the abstraction process. For this purpose, we provide to the designer abstraction operators which, if used judiciously in the description of a design, structure the corresponding state space hierarchically. This structure can then be exploited by verification tools, and makes possible the automatic and exhaustive exploration of state spaces that would otherwise be out of scope for existing model checkers.

Specifically, we present the following contributions:

Proceedings of the Fourth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Lecture Notes in Computer Science 1384, Springer, 1998, pp. 330-344.

Download inofficial, sometimes updated PostScript / PDF document. © 1998 Springer.