Advertisement

Partial-order reduction in symbolic state space exploration

  • R. Alur
  • R. K. Brayton
  • T. A. Henzinger
  • S. Qadeer
  • S. K. Rajamani
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1254)

Abstract

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.

Keywords

Boolean Function Transition Relation Binary Decision Diagram Reachability Analysis Symbolic Model Check 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

References

  1. [BCL91]
    J.R. Burch, E.M. Clarke, and D.E. Long. Symbolic Model Checking with Partitioned Transition Relations. In Proc. of the 28th Design Automation Conference, pages 403–407,1991.Google Scholar
  2. [BCMD92]
    J.R. Burch, E.M. Clarke, K.L. McMillan, and D.L. Dill. Symbolic Model Checking: 1020 States and Beyond. Information and Computation, 98:142–170, 1992.Google Scholar
  3. [BHSV+96]
    R.K.Brayton,G.D.Hachtel,A. 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. Swamy, and T. Villa. VIS: A System for Verification and Synthesis. In Proc. of the 8th International Conference on Computer-Aided Verification, vol. 1102 of Lecture Notes in Computer Science, pages 428–432. Springer, 1996.Google Scholar
  4. [CP96]
    C.-T. Chou and D.A. Peled. Formal Verification of a Partial-Order Reduction Technique for Model Checking. In Proc. of the Second International Workshop on Tools and Algorithms for the Construction and Analysis of Systems, vol. 1055 of Lecture Notes in Computer Science, pages 241–257. Springer, 1996.Google Scholar
  5. [Dil89]
    D.L. Dill. Trace Theory for Automatic Hierarchical Verification of Speed-Independent Circuits. MIT Press, 1989.Google Scholar
  6. [DKR82]
    D. Dolev, M. Klawe, and M. Rodeh. An O(n log n) Unidirectional Distributed Algorithm for Extrema Finding in a Circle. Journal of Algorithms, 3:245–260, 1982.Google Scholar
  7. [God96]
    P. Godefroid. Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem, vol. 1032 of Lecture Notes in Computer Science. Springer, 1996.Google Scholar
  8. [GW94]
    P. Godefroid and P. Wolper. A Partial Approach to Model Checking. Information and Computation, 110:305–326, 1994.Google Scholar
  9. [HP94]
    G.J. Holzmann and D.A. Peled. An Improvement in Formal Verification. In Proc. of the 7th International Conference on Formal Description Techniques, pages 197–211. Chapman & Hall, 1994.Google Scholar
  10. [Maz88]
    A. Mazurkiewicz. Basic Notions of Trace Theory. In Workshop on Linear Time, Branching Time, and Partial Order in Logics and Models for Concurrency, vol. 354 of Lecture Notes in Computer Science, pages 285–363. Springer, 1988.Google Scholar
  11. [McM93]
    K.L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.Google Scholar
  12. [Pel93]
    D.A. Peled. All from One, One for All: On Model Checking Using Representatives. In Proc. of the 5th International Conference on Computer-Aided Verification, vol. 697 of Lecture Notes in Computer Science, pages 409–423. Springer, 1993.Google Scholar
  13. [RAP+95]
    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.Google Scholar
  14. [Val91]
    A. Valmari. Stubborn Sets for Reduced State Space Generation. In Advances in Petri Nets, vol. 483 of Lecture Notes in Computer Science, pages 491–515. Springer, 1991.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1997

Authors and Affiliations

  • R. Alur
    • 1
  • R. K. Brayton
    • 1
  • T. A. Henzinger
    • 1
  • S. Qadeer
    • 1
  • S. K. Rajamani
    • 1
  1. 1.EECS DepartmentUniversity of CaliforniaBerkeleyUSA

Personalised recommendations