Abstract
The Bounded Model Checking approach to the LTL model checking problem, based on an encoding to Boolean satisfiability, has seen a growth in popularity due to recent improvements in SAT technology. The currently available encodings have certain shortcomings, particularly in the size of the clause forms that it generates. We address this by making use of the established correspondence between temporal logic expressions and the fixpoints of predicate transformers as used in symbolic model checking. We demonstrate how an encoding based on fixpoints can result in improved performance in the SAT checker.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Adnan Aziz et al. Examples of HW verification using VIS, 1997. http://vlsi.colorado.edu/~vis/texas-97/
Armin Biere, Alessandro Cimatti, Edmund Clarke, and Yunshan Zhu. Symbolic model checking without BDDs. In W.R. Cleaveland, editor, Tools and Algorithms for the Construction and Analysis of Systems. 5th International Conference, TACAS’99, volume 1579 of Lecture Notes in Computer Science, pages 193–207. Springer-Verlag Inc., July 1999.
Alexander Bolotov and Michael Fisher. A resolution method for CTL branching-time temporal logic. In Proceedings of the Fourth International Workshop on Temporal Representation and Reasoning (TIME). IEEE Press, 1997.
Alessandro Cimatti, Marco Pistore, Marco Roveri, and Roberto Sebastiani. Improving the encoding of LTL model checking into SAT. In Agostino Cortesi, editor, Third International Workshop on Verification, Model Checking and Abstract Interpretation, volume 2294 of Lecture Notes in Computer Science. Springer-Verlag Inc., January 2002.
Martin Davis and Hilary Putnam. A computing procedure for quantification theory. Journal of the ACM, 7:201–215, 1960.
M.B. Dwyer, G.S. Avrunin, and J.C. Corbett. Property Specification Patterns for Finite-State Verification. In M. Ardis, editor, 2nd Workshop on Formal Methods in Software Practice, pages 7–15, March 1998.
M.B. Dwyer, G.S. Avruning, and J.C. Corbett. Patterns in property specifications for finite-state verification. In 21st International Conference on Software Engineering, Los Angeles, California, May 1999.
E. Allen Emerson and Edmund M. Clarke. Characterizing correctness properties of parallel programs using fixpoints. In Jan van Leeuwen J. W. de Bakker, editor, Automata, Languages and Programming, 7th Colloquium, volume 85 of Lecture Notes in Computer Science, pages 169–181. Springer-Verlag Inc, 1980.
Michael Fisher. A resolution method for temporal logic. In Proceedings of Twelfth International Joint Conference on Artificial Intelligence (IJCAI). Morgan Kaufmann, August 1991.
Michael Fisher and Philippe Noël. Transformation and synthesis in MetateM Part I: Propositional MetateM. Technical Report UMCS-92-2-1, Department of Computer Science, University of Manchester, Manchester M13 9PL, England, February 1992.
Dov Gabbay. The declarative past and imperative future. In H. Barringer, editor, Proccedings of the Colloquium on Temporal Logic and Specifications, volume 398 of Lecture Notes in Computer Science, pages 409–448. Springer-Verlag, 1989.
The VIS Group. VIS: A system for verification and synthesis. In R. Alur and T. Henzinger, editors, Proceedings of the 8th International Conference on Computer Aided Verification, volume 1102 of Lecture Notes in Computer Science, pages 428–432, New Brunswick, NJ, July 1996. Springer.
A. J. Martin. The design of a self-timed circuit for distributed mutual exclusion. In Henry Fuchs, editor, Proceedings of the 1985 Chapel Hill Conference on VLSI, pages 245–260. Computer Science Press, 1985.
K. L. McMillan. Symbolic Model Checking: An Approach to the State Explosion Problem. PhD thesis, Carnegie Mellon University, 1992.
M. Moskewicz, C. Madigan, Y. Zhao, L. Zhang, and S. Malik. Chaff: Engineering an efficient SAT solver. In 39th Design Automation Conference, Las Vegas, June 2001.
Daniel Sheridan. Using fixpoint characterisations of LTL for bounded model checking. Technical Report APES-41-2002, APES Research Group, January 2002. Available from http://www.dcs.st-and.ac.uk/~apes/apesreports.html
Daniel Sheridan and Toby Walsh. Clause forms generated by bounded model checking. In Andrei Voronkov, editor, Eighth Workshop on Automated Reasoning, 2001.
A. Tarski. A lattice-theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics, 5:285–309, 1955.
Pierre Wolper. Specification and synthesis of communicating processes using an extended temporal logic. In Proceeding of the 9th Symposium on Principles of Programming Languages, pages 20–33, Albuquerque, January 1982.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Frisch, A., Sheridan, D., Walsh, T. (2002). A Fixpoint Based Encoding for Bounded Model Checking. In: Aagaard, M.D., O’Leary, J.W. (eds) Formal Methods in Computer-Aided Design. FMCAD 2002. Lecture Notes in Computer Science, vol 2517. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36126-X_15
Download citation
DOI: https://doi.org/10.1007/3-540-36126-X_15
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-00116-4
Online ISBN: 978-3-540-36126-8
eBook Packages: Springer Book Archive