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.
Research supported in part by NSF grants CDA-9303181, CCR-9404921, CCR-9505562, CDA-9504275, and AFOSR grants F49620-95-1-0508 and F49620-96-1-0087.
Chapter PDF
Similar content being viewed by others
Keywords
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
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.
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.
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.
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.
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.
E. M. Clarke, K. McMillan, S. Campos, and V. Hartonas-GarmHausen. Symbolic model checking. In Alur and Henzinger [AH96], pages 419–422.
R. Cleaveland and S. Sims. The NCSU concurrency workbench. In Alur and Henzinger [AH96], pages 394–397.
W. Chen and D.S. Warren. Tabled evaluation with delaying for general logic programs. Journal of the ACM, 43(1):20–74, January 1996.
E. M. Clarke and J. M. Wing. Formal methods: State of the art and future directions. ACM Computing Surveys, 28(4), December 1996.
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.
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.
R. Gerth, R. Kuiper, W. Penczek, and D. Peled. A partial order approach to branching time model checking. Information and Computation, 1997.
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.
G. J. Holzmann and D. Peled. The state of SPIN. In Alur and Henzinger [AH96], pages 385–389.
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.
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.
R. Milner. Communication and Concurrency. International Series in Computer Science. Prentice Hall, 1989.
Z, Manna and A. Pnueli. Temporal Verification of Reactive Systems: Safety. Springer-Verlag, 1995.
J. S. Ostroff. Constraint logic programming for reasoning about discrete event processes. Journal of Logic Programming, 11(2/3):243–270, Oct./Nov. 1991.
A. Pnueli and E. Shahar. A platform for combining deductive with algorithmic verification. In Alur and Henzinger [AH96], pages 184–195.
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.
A. Rauzy. Toupie=μ-calculus + constraints. In Wolper [Wol95], pages 114–126.
S. Rajan, N. Shankar, and M. K. Srivas. An integration of model checking with automated proof checking. In Wolper [Wol95], pages 84–97.
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.
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.
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.
H. B. Sipma, T. E. Uribe, and Z. Manna. Deductive model checking. In Alur and Henzinger [AH96], pages 208–219.
H. Tamaki and T. Sato. OLDT resolution with tabulation. In Third Int'l Conf. on Logic Programming, pages 84–98, 1986.
J. D. Ullman. Principles of Data and Knowledge-base Systems, Volume I. Computer Science Press, Rockville, MD, 1988.
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.
P. Wolper, editor. Computer Aided Verification (CAV '95), volume 939 of Lecture Notes in Computer Science, Liege, Belgium, July 1995. Springer-Verlag.
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.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ramakrishna, Y.S., Ramakrishnan, C.R., Ramakrishnan, I.V., Smolka, S.A., Swift, T., Warren, D.S. (1997). Efficient model checking using tabled resolution. In: Grumberg, O. (eds) Computer Aided Verification. CAV 1997. Lecture Notes in Computer Science, vol 1254. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-63166-6_16
Download citation
DOI: https://doi.org/10.1007/3-540-63166-6_16
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-63166-8
Online ISBN: 978-3-540-69195-2
eBook Packages: Springer Book Archive