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 partiallyand in some cases, fullybypassing
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
intermediate steps.
Mathematically, our abstraction operator is a function that maps a flat
transition system into a twolevel hierarchy where each atomic upperlevel
transition expands into an entire lowerlevel transition system.
For example, an arithmetic operation may expand into a sequence of bit
operations.

A BDDbased algorithm for the symbolic exploration of multilevel
hierarchies of transition systems.
The algorithm traverses a leveln transition by expanding the
corresponding level(n1) transition system onthefly.
The leveln successors of a state are determined by computing a
level(n1) 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
examplesa multiplier, a cache coherence protocol, and a multiprocessor
system.
In the first two examples, we obtain significant improvements in run
times and peak BDD sizes over traditional statespace 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.
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. 330344.
Download inofficial, sometimes updated
PostScript /
PDF document.
© 1998 Springer.