Abstract
State-space explosion is a fundamental obstacle in the 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 reduction 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.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
References
R. Alur and T.A. Henzinger, “Reactive modules,” in Proceedings of the 11th Annual Symposium on Logic in Computer Science, IEEE Computer Society Press, Silver Spring, MD, 1996, pp. 207–218.
J.R. Burch, E.M. Clarke, and D.E. Long, “Symbolic model checking with partitioned transition relations,” in DAC 91: Design Automation Conference, 1991, pp. 403–407.
J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and L.J. Hwang, “Symbolic model checking: 1020 states and beyond,” Information and Computation, Vol. 98, No. 2, pp. 142–170, 1992.
R.K. Brayton, G.D. Hachtel, A.L. Sangiovanni-Vincentelli, F. Somenzi, A. Aziz, S.-T. Cheng, S. Edwards, S. Khatri, Y. Kukimoto, A. Pardo, S. Qadeer, R.K. Ranjan, S. Sarwary, T.R. Shiple, G.M. Swamy, and T. Villa, “VIS:Asystem for verification and synthesis,” in R. Alur and T.A. Henzinger (Eds.), CAV 96: Computer Aided Verification. Lecture Notes in Computer Science, Vol. 1102, Springer-Verlag, Berlin, 1996, pp. 428–432.
C.-T. Chou and D.A. Peled, “Formal verification of a partial-order reduction technique for model checking,” in TACAS 96: Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, Vol. 1055, Springer-Verlag, Berlin, 1996, pp. 241–257.
D. Dolev, M. Klawe, and M. Rodeh, “An O (n log n) unidirectional distributed algorithm for extrema finding in a circle,” Journal of Algorithms, Vol. 3, 1982, pp. 245–260.
P. Godefroid, Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem. Lecture Notes in Computer Science, Vol. 1032, Springer-Verlag, Berlin, 1996.
P. Godefroid and P. Wolper, “A partial approach to model checking,” Information and Computation, Vol. 110, No. 2, pp. 305–326, 1994.
G.J. Holzmann and D.A. Peled, “An improvement in formal verification,” in Proc. of the 7th International Conference on Formal Description Techniques, Chapman & Hall, London, 1994, pp. 197–211.
T. Kam, T. Villa, R.K. Brayton, and A.L. Sangiovanni-Vincentelli, Multi-valued decision diagrams: theory and applications. International Journal on Multiple-Valued Logic, Vol. 4, No. 1/2, pp. 9–62, 1998.
A. Mazurkiewicz, “Basic notions of trace theory,” in J.W. de Bakker, W.-P. de Roever, and G. Rozenberg (Eds.), Linear Time, Branching Time, and Partial Order in Logics and Models for Concurrency. Lecture Notes in Computer Science, Vol. 354, Springer-Verlag, Berlin, 1989, pp. 285–363.
K.L. McMillan, Symbolic Model Checking: An Approach to the State-Explosion Problem. Kluwer Academic Publishers, Dordrecht, 1993.
D. Peled, “All from one, one for all: On model checking using representatives,” in C. Courcoubetis (Ed.), CAV 93: Computer Aided Verification. Lecture Notes in Computer Science, Vol. 697, Springer-Verlag, Berlin, 1993, pp. 409–423.
R.K. Ranjan, A. Aziz, B. Plessier, C. Pixley, and R.K. Brayton, “Efficient formal design verification: Data structures + algorithms,” in Workshop Notes of the International Workshop on Logic Synthesis, 1995.
Thomas R. Shiple, Ramin Hojati, Alberto L. Sangiovanni-Vincentelli, and Robert K. Brayton, “Heuristic minimization of BDDs using don't cares,” in DAC 94: Design Automation Conference, 1994, pp. 225–231.
A. Valmari, “Astubborn attack on state explosion,” in R.P. Kurshan and E.M. Clarke (Eds.), CAV 90: Computer Aided Verification. Lecture Notes in Computer Science, Vol. 531, Springer-Verlag, Berlin, 1990, pp. 25–42.
Author information
Authors and Affiliations
Rights and permissions
About this article
Cite this article
Alur, R., Brayton, R., Henzinger, T. et al. Partial-Order Reduction in Symbolic State-Space Exploration. Formal Methods in System Design 18, 97–116 (2001). https://doi.org/10.1023/A:1008767206905
Issue Date:
DOI: https://doi.org/10.1023/A:1008767206905