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:
A temporal abstraction operator that aggregates transitions and hides
Mathematically, our abstraction operator is a function that maps a flat
transition system into a two-level hierarchy where each atomic upper-level
transition expands into an entire lower-level transition system.
For example, an arithmetic operation may expand into a sequence of bit
A BDD-based algorithm for the symbolic exploration of multi-level
hierarchies of transition systems.
The algorithm traverses a level-n transition by expanding the
corresponding level-(n-1) transition system on-the-fly.
The level-n successors of a state are determined by computing a
level-(n-1) reach set, which is then immediately released from memory.
In this fashion, we can exhaustively explore hierarchically structured
state spaces whose flat counterparts cause memory overflows.
We experimentally demonstrate the efficiency of our method with three
examples---a multiplier, a cache coherence protocol, and a multiprocessor
In the first two examples, we obtain significant improvements in run
times and peak BDD
sizes over traditional state-space search.
The third example cannot be model checked at all using conventional
methods (without manual abstractions), but can be analyzed fully
automatically using transition hierarchies.
In Proceedings of the Fourth International Workshop
on Tools and Algorithms for the Construction and
Analysis of Systems (TACAS'98), LNCS 1384, pp. 330-344, 1998.