BDD-Based Decision Procedures for \( \mathcal{K} \)

  • Guoqiang Pan
  • Ulrike Sattler
  • Moshe Y. Vardi
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2392)


We describe BDD-based decision procedures for \( \mathcal{K} \). Our approach is inspired by the automata-theoretic approach, but we avoid explicit automata construction. Our algorithms compute the fixpoint of a set of types, which are sets of formulas satisfying some consistency conditions. We use BDDs to represent and manipulate such sets. Experimental results show that our algorithms are competitive with contemporary methods using benchmarks from TANCS 98 and TANCS 2000.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    H. R. Andersen. An introduction to binary decision diagrams. Technical report, Department of Information Technology, Technical University of Denmark, 1998.Google Scholar
  2. 2.
    C. Areces, R. Gennari, J. Heguiabehere, and M. de Rijke. Tree-based heuristics in modal theorem proving. In Proceedings of the ECAI’2000, 2000.Google Scholar
  3. 3.
    F. Baader and S. Tobies. The inverse method implements the automata approach for modal satisfiability. In Proc. of IJCAR-01, volume 2083 of LNCS. Springer Verlag, 2001.Google Scholar
  4. 4.
    I. Beer, S. Ben-David, D. Geist, R. Gewirtzman, and M. Yoeli. Methodology and system for practical formal verification of reactive hardware. In Proc. of CAV-94, volume 818 of LNCS, pages 182–193, 1994.Google Scholar
  5. 5.
    P. Blackburn, M. D. Rijke, Y. Venema, and M. D. Rijke. Modal logic. Cambridge University Press, 2001.Google Scholar
  6. 6.
    R. E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, Vol. C-35(8):677–691, August 1986.Google Scholar
  7. 7.
    J. Burch, E. Clarke, K. McMillan, D. Dill, and L. J. Hwang. Symbolic model checking: 1020 states and beyond. Infomation and Computation, 98(2):142–170, 1992.zbMATHCrossRefMathSciNetGoogle Scholar
  8. 8.
    J. R. Burch, E. M. Clarke, and D. E. Long. Symbolic model checking with partitioned transition relations. In Int. Conf. on VLSI, pages 49–58, 1991.Google Scholar
  9. 9.
    A. Cimatti, E. M. Clarke, F. Giunchiglia, and M. Roveri. NUSMV: A new symbolic model checker. Int. Journal on Software Tools for Technology Transfer, 2(4):410–425, 2000.zbMATHCrossRefGoogle Scholar
  10. 10.
    R. Dyckhoff, editor. Proceedings of TABLEAUX 2000, volume 1847 of LNAI. Springer Verlag, 2000.Google Scholar
  11. 11.
    D. Geist and H. Beer. Efficient model checking by automated ordering of transition relation partitions. In Proc. of the sixth Int. Conf. on CAV, pages 299–310, 1994.Google Scholar
  12. 12.
    E. Giunchiglia, M. Maratea, A. Tacchella, and D. Zambonin. Evaluating search heuristics and optimization techniques in propositional satisfiability. In IJCAR, pages 347–363, 2001.Google Scholar
  13. 13.
    F. Giunchiglia and R. Sebastiani. Building decision procedures for modal logics from propositional decision procedure-the case study of modal K(m). Infomation and Computation, 162:158–178, 2000.zbMATHCrossRefMathSciNetGoogle Scholar
  14. 14.
    J. Y. Halpern and Y. Moses. A guide to completeness and complexity for modal logics of knowledge and belief. Artificial Intelligence, 54:319–379, 1992.zbMATHCrossRefMathSciNetGoogle Scholar
  15. 15.
    A. Heuerding and S. Schwendimann. A benchmark method for the propositional modal logics K, KT, S4. Technical report, Universität Bern, Switzerland, 1996.Google Scholar
  16. 16.
    U. Hustadt and R. Schmidt. MSPASS: modal reasoning by translation and first order resolution. In [10], pages 67–71.Google Scholar
  17. 17.
    G. Kamhi, L. Fix, and Z. Binyamini. Symbolic model checking visualization. In Proc. of FMCAD’98, volume 1522 of LNCS, pages 290–303. Springer Verlag, November 1998.Google Scholar
  18. 18.
    R. E. Ladner. The computational complexity of provability in systems of modal propositional logic. SIAM J. Comput., 6(3):467–480, 1977.zbMATHCrossRefMathSciNetGoogle Scholar
  19. 19.
    F. Massacci and F. M. Donini. Design and results of TANCS-00. In [10], pages 52–56.Google Scholar
  20. 20.
    I.-H. Moon, G. D. Hachtel, and F. Somenzi. Border-block trianglular form and conjunction schedule in image computation. In W. H. Jr. and S. Johnson, editors, FMCAD2000, volume 1954 of LNCS, pages 73–90. Springer Verlag, 2000.Google Scholar
  21. 21.
    H. Ohlbach, A. Nonnengart, M. de Rijke, and D. Gabbay. Encoding two-valued non-classical logics in classical logic. In J. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning. Elsevier, 1999.Google Scholar
  22. 22.
    P. F. Patel-Schneider and I. Horrocks. DLP and FaCT. In Proc. of TABLEAUX-99, volume 1397 of LNAI, pages 19–23. Springer Verlag, 1999.Google Scholar
  23. 23.
    V. Pratt. A near-optimal method for reasoning about action. Journal of Computer and System Sciences, 20(2):231–254, 1980.zbMATHCrossRefMathSciNetGoogle Scholar
  24. 24.
    R. Ranjan, A. Aziz, R. Brayton, B. Plessier, and C. Pixley. Efficient BDD algorithms for FSM synthesis and verification. In Proceedings of IEEE/ACM International Workshop on Logic Synthesis, 1995.Google Scholar
  25. 25.
    F. Somenzi. CUDD: CU decision diagram package, 1998.Google Scholar
  26. 26.
    G. Sutcliffe and C. Suttner. Evaluating general purpose automated theorem proving systems. Artificial intelligence, 131:39–54, 2001.zbMATHCrossRefMathSciNetGoogle Scholar
  27. 27.
    A. Tacchella. *SAT system description. In Collected Papers from the International Description Logics Workshop (DL’99). CEUR, 1999.Google Scholar
  28. 28.
    J. van Benthem. Modal Logic and Classical Logic. Bibliopolis, 1983.Google Scholar
  29. 29.
    M. Vardi. What makes modal logic so robustly decidable? In N. Immerman and P. Kolaitis, editors, Descriptive Complexity and Finite Models, pages 149–183. American Mathematical Society, 1997.Google Scholar
  30. 30.
    A. Voronkov. How to optimize proof-search in modal logics: new methods of proving redundancy criteria for sequent calculi. Computational Logic, 2(2):182–215, 2001.CrossRefMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Guoqiang Pan
    • 1
  • Ulrike Sattler
    • 2
  • Moshe Y. Vardi
    • 1
  1. 1.Department of Computer ScienceRice UniversityHouston
  2. 2.Institut für Theoretische InformatikTU DresdenGermany

Personalised recommendations