## Partial-Order Reduction in Symbolic State-Space Exploration

*Rajeev Alur, Robert K. Brayton,
Thomas A. Henzinger,
Shaz Qadeer, and Sriram K. Rajamani*

State-space explosion is a fundamental obstacle in formal verification of
designs and protocols.
Several techniques for combating this problem have emerged in the past few
years, among which two are significant:
*partial-order reductions* and *symbolic state-space search*.
In asynchronous systems, interleavings of independent concurrent events are
equivalent, and only a representative interleaving needs to be explored to
verify local properties.
Partial-order methods exploit this redundancy and visit only a subset of the
reachable states.
Symbolic techniques, on the other hand, capture the transition relation of a
system and the set of reachable states as boolean functions.
In many cases, these functions can be represented compactly using binary
decision diagrams (BDDs).
Traditionally, the two techniques have been practiced by two different
schools--partial-order methods with enumerative depth-first search for the
analysis of asynchronous network protocols, and symbolic breadth-first search
for the analysis of synchronous hardware designs.
We combine both approaches and develop a method for using partial-order
reduction techniques in symbolic BDD-based invariant checking.
We present theoretical results to prove the correctness of the method, and
experimental results to demonstrate its efficacy.

*Formal Methods in System Design* 18:97-116, 2001.
A preliminary version appeared in the
*Proceedings of the
Ninth International Conference on Computer-Aided Verification*
(CAV),
Lecture Notes in Computer Science 1254,
Springer, 1997, pp. 340-351.

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