Automatic abstraction techniques for propositional μ-calculus model checking

  • Abelardo Pardo
  • Gary D. Hachtel
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1254)


An abstraction/refinement paradigm for the full propositional μ-calculus is presented. No distinction is made between universal or existential fragments. Necessary conditions for conservative verification are provided, along with a fully automatic symbolic model checking abstraction algorithm. The algorithm begins with conservative verification of an initial abstraction. If the conclusion is negative, it derives a “goal set” of states which require further resolution. It then successively refines, with respect to this goal set, the approximations made in the subformulas, until the given formula is verified or computational resources are exhausted.


Model Check Boolean Function Binary Decision Diagram Kripke Structure 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.


  1. 1.
    F. Balarin and A. L. Sangiovanni-Vincentelli. An iterative approach to language containment. In C. Courcoubetis, editor, Fifth Conference on Computer Aided Verification (CAV '93). Springer-Verlag, Berlin, 1993. LNCS 697.Google Scholar
  2. 2.
    R. K. Brayton et al. VIS: A system for verification and synthesis. In T. Henzinger and R. Alur, editors, Eigth Conference on Computer Aided Verification (CAV'96), pages 428–432. Springer-Verlag, Rutgers University, 1996. LNCS 1102.Google Scholar
  3. 3.
    R. E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, C-35(8):677–691, Aug. 1986.Google Scholar
  4. 4.
    J. R. Burch, E. M. Clarke, and D. E. Long. Representing circuits more efficiently in symbolic model checking. In Proceedings of the Design Automation Conference, pages 403–407, San Francisco, CA, June 1991.Google Scholar
  5. 5.
    J. R. Burch, E. M. Clarke, K. L. McMillan, and D. L. Dill. Sequential circuit verification using symbolic model checking. In Proceedings of the Design Automation Conference, pages 46–51, June 1990.Google Scholar
  6. 6.
    H. Cho, G. D. Hachtel, E. Macii, B. Plessier, and F. Somenzi. Algorithms for approximate FSM traversal based on state space decomposition. In Proceedings of the Design Automation Conference, pages 25–30, Dallas, TX, June 1993.Google Scholar
  7. 7.
    P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by constructions or approximation of fixpoints. In Proceedings of the ACM Symposium on the Principles of Programming Languages, pages 238–250, 1977.Google Scholar
  8. 8.
    M. Dam. CTL* and ECTL* as fragments of the modal μ-calculus. Theoretical Computer Science, 126: 77–97, 1994.Google Scholar
  9. 9.
    E. A. Emerson and C.-L. Lei. Efficient model checking in fragments of the propositional mu-calculus. In Proceedings of the First Annual Symposium of Logic in Computer Science, pages 267–278, June 1986.Google Scholar
  10. 10.
    D. Geist and I. Beer. Efficient model checking by automated ordering of transition relation parititons. In D. L. Dill, editor, Sixth Conference on Computer Aided Verification (CAV'94), pages 299–310, Berlin, 1994. Springer-Verlag. LNCS 818.Google Scholar
  11. 11.
    P. Kelb, D. Dams, and R. Gerth. Practical symbolic model checking of the full μ-calculus using compositional abstractions. Technical Report 95-31, Department of Computing Science, Eindhoven University of Technology, 1995.Google Scholar
  12. 12.
    D. Kozen. Results on the propositional μ-calculus. Theoretical Computer Science, 27:333–354, 1983.Google Scholar
  13. 13.
    R. P. Kurshan. Computer-Aided Verification of Coordinating Processes. Princeton University Press, Princeton, NJ, 1994.Google Scholar
  14. 14.
    W. Lee, A. Pardo, J. Jang, G. Hachtel, and F. Somenzi. Tearing based abstraction for CTL model checking. In Proceedings of the IEEE International Conference on Computer Aided Design, pages 76–81, 1996.Google Scholar
  15. 15.
    D. E. Long. Model Checking, Abstraction, and Compositional Verification. PhD thesis, Carnegie-Mellon University, July 1993.Google Scholar
  16. 16.
    K. L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, Boston, MA, 1994.Google Scholar
  17. 17.
    C. Pixley, S.-W. Jeong, and G. D. Hachtel. Exact calculation of synchronization sequences based on binary decision diagrams. In Proceedings of the Design Automation Conference, pages 620–623, Anaheim, CA, June 1992.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1997

Authors and Affiliations

  • Abelardo Pardo
    • 1
  • Gary D. Hachtel
    • 1
  1. 1.University of ColoradoBoulderUSA

Personalised recommendations