Advertisement

Efficient model checking using tabled resolution

  • Y. S. Ramakrishna
  • C. R. Ramakrishnan
  • I. V. Ramakrishnan
  • Scott A. Smolka
  • Terrance Swift
  • David S. Warren
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1254)

Abstract

We demonstrate the feasibility of using the XSB tabled logic programming system as a programmable fixed-point engine for implementing efficient local model checkers. In particular, we present XMC, an XSB-based local model checker for a CCS-like value-passing language and the alternation-free fragment of the modal mu-calculus. XMC is written in under 200 lines of XSB code, which constitute a declarative specification of CCS and the modal mu-calculus at the level of semantic equations.

In order to gauge the performance of XMC as an algorithmic model checker, we conducted a series of benchmarking experiments designed to compare the performance of XMC with the local model checkers implemented in C/C++ in the Concurrency Factory and SPIN specification and verification environments. After applying certain newly developed logic-programming-based optimizations (along with some standard ones), XMC's performance became extremely competitive with that of the Factory and shows promise in its comparison with SPIN.

Keywords

Model Check Logic Program Temporal Logic Constraint Logic Programming 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. [AH96]
    R. Alur and T. A. Henzinger, editors. Computer Aided Verification (CAV '96), volume 1102 of Lecture Notes in Computer Science, New Brunswick, New Jersey, July 1996. Springer-Verlag.Google Scholar
  2. [BBC+96]
    N. Bjørner, A. Browne, E. Chang, M. Colón, A. Kapur, Z. Manna, H. B. Sipma, and T. E. Uribe. STeP: Deductive-algorithmic verification of reactive and real-time systems. In Alur and Henzinger [AH96], pages 415–418.Google Scholar
  3. [CE81]
    E. M. Clarke and E. A. Emerson. Design and synthesis of synchronization skeletons using branching-time temporal logic. In D. Kozen, editor, Proceedings of the Workshop on Logic of Programs, Yorktown Heights, volume 131 of Lecture Notes in Computer Science, pages 52–71. Springer-Verlag, 1981.Google Scholar
  4. [CES86]
    E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM TOPLAS, 8(2), 1986.Google Scholar
  5. [CLSS96]
    R. Cleaveland, P. M. Lewis, S. A. Smolka, and O. Sokolsky. The Concurrency Factory: A development environment for concurrent systems. In Alur and Henzinger [AH96], pages 398–401.Google Scholar
  6. [CMCHG96]
    E. M. Clarke, K. McMillan, S. Campos, and V. Hartonas-GarmHausen. Symbolic model checking. In Alur and Henzinger [AH96], pages 419–422.Google Scholar
  7. [CS96]
    R. Cleaveland and S. Sims. The NCSU concurrency workbench. In Alur and Henzinger [AH96], pages 394–397.Google Scholar
  8. [CW96a]
    W. Chen and D.S. Warren. Tabled evaluation with delaying for general logic programs. Journal of the ACM, 43(1):20–74, January 1996.Google Scholar
  9. [CW96b]
    E. M. Clarke and J. M. Wing. Formal methods: State of the art and future directions. ACM Computing Surveys, 28(4), December 1996.Google Scholar
  10. [DRRS95]
    S. Dawson, C.R. Ramakrishnan, I.V. Ramakrishnan, and T. Swift. Optimizing clause resolution: Beyond unification factoring. In International Logic Programming Symposium, pages 194–208. MIT Press, 1995.Google Scholar
  11. [EL86]
    E. A. Emerson and C.-L. Lei. Efficient model checking in fragments of the propositional mu-calculus. In Proceedings of the First Annual Symposium on Logic in Computer Science, pages 267–278, 1986.Google Scholar
  12. [GKPP97]
    R. Gerth, R. Kuiper, W. Penczek, and D. Peled. A partial order approach to branching time model checking. Information and Computation, 1997.Google Scholar
  13. [HP95]
    G. J. Holzmann and D. Peled. An improvement in formal verification. In Seventh Int. Conf. on Formal Description Techniques (FORTE '94), pages 177–194. Chapman and Hall, 1995.Google Scholar
  14. [HP96]
    G. J. Holzmann and D. Peled. The state of SPIN. In Alur and Henzinger [AH96], pages 385–389.Google Scholar
  15. [HPP96]
    G. Holzmann, D. Peled, and V. Pratt, editors. Partial-Order Methods in Verification (POMIV '96), DIMACS Series in Discrete Mathematics and Theoretical Computer Science, New Brunswick, New Jersey, July 1996. American Mathematical Society.Google Scholar
  16. [JPO95]
    L. J. Jagadeesan, C. Puchol, and J. E. Von Olnhausen. Safety property verification of ESTEREL programs and applications to telecommunications software. In Wolper [Wol95], pages 127–140.Google Scholar
  17. [Mil89]
    R. Milner. Communication and Concurrency. International Series in Computer Science. Prentice Hall, 1989.Google Scholar
  18. [MP95]
    Z, Manna and A. Pnueli. Temporal Verification of Reactive Systems: Safety. Springer-Verlag, 1995.Google Scholar
  19. [Ost91]
    J. S. Ostroff. Constraint logic programming for reasoning about discrete event processes. Journal of Logic Programming, 11(2/3):243–270, Oct./Nov. 1991.Google Scholar
  20. [PS96]
    A. Pnueli and E. Shahar. A platform for combining deductive with algorithmic verification. In Alur and Henzinger [AH96], pages 184–195.Google Scholar
  21. [QS82]
    J. P. Queille and J. Sifakis. Specification and verification of concurrent systems in Cesar. In Proceedings of the International Symposium in Programming, volume 137 of Lecture Notes in Computer Science, Berlin, 1982. Springer-Verlag.Google Scholar
  22. [Rau95]
    A. Rauzy. Toupie=μ-calculus + constraints. In Wolper [Wol95], pages 114–126.Google Scholar
  23. [RSS95]
    S. Rajan, N. Shankar, and M. K. Srivas. An integration of model checking with automated proof checking. In Wolper [Wol95], pages 84–97.Google Scholar
  24. [SCK+95]
    B. Steffen, A. Classen, M. Klein, J. Knoop, and T. Margaria. The fixpoint-analysis machine. In I. Lee and S. A. Smolka, editors, Proceedings of the Sixth International Conference on Concurrency Theory (CONCUR '95), Vol. 962 of Lecture Notes in Computer Science, pages 72–87. Springer-Verlag, 1995.Google Scholar
  25. [SHIR96]
    S. K. Shukla, H. B. Hunt III, and D. J. Rosenkrantz. HORNSAT, model checking, verification and games. In Alur and Henzinger [AH96], pages 99–110.Google Scholar
  26. [SSW96]
    K. Sagonas, T. Swift, and D.S. Warren. An abstract machine to compute fixed-order dynamically stratified programs. In International Conference on Automated Deduction (CADE), 1996.Google Scholar
  27. [SUM96]
    H. B. Sipma, T. E. Uribe, and Z. Manna. Deductive model checking. In Alur and Henzinger [AH96], pages 208–219.Google Scholar
  28. [TS86]
    H. Tamaki and T. Sato. OLDT resolution with tabulation. In Third Int'l Conf. on Logic Programming, pages 84–98, 1986.Google Scholar
  29. [U1188]
    J. D. Ullman. Principles of Data and Knowledge-base Systems, Volume I. Computer Science Press, Rockville, MD, 1988.Google Scholar
  30. [Wol86]
    P. Wolper. Expressing interesting properties of programs in propositional temporal logic. In Proc. 13th ACM Symp. on Principles of Programming, pages 184–192, St. Petersburgh, January 1986.Google Scholar
  31. [Wol95]
    P. Wolper, editor. Computer Aided Verification (CAV '95), volume 939 of Lecture Notes in Computer Science, Liege, Belgium, July 1995. Springer-Verlag.Google Scholar
  32. [ZSS94]
    S. Zhang, O. Sokolsky, and S. A. Smolka. On the parallel complexity of model checking in the modal mu-calculus. In Proceedings of the 9th IEEE Symposium on Logic in Computer Science, London, England, July 1994.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1997

Authors and Affiliations

  • Y. S. Ramakrishna
    • 1
  • C. R. Ramakrishnan
    • 1
  • I. V. Ramakrishnan
    • 1
  • Scott A. Smolka
    • 1
  • Terrance Swift
    • 1
  • David S. Warren
    • 1
  1. 1.Department of Computer ScienceSUNY at Stony BrookStony BrookUSA

Personalised recommendations