Abstract
Bounded Model Checking (BMC) is a technique for encoding an LTL model checking problem into a problem of propositional satisfiability. Since the seminal paper by Biere et al. [2], the research on BMC has been primarily directed at achieving higher efficiency for solving reachability properties. In this paper, we tackle the problem of improving BMC encodings for the full class of LTL properties. We start noticing some properties of the encoding of [2], and we exploit them to define improvements that make the resulting boolean formulas smaller or simpler to solve.
The fourth author is sponsored under the MURST COFIN99 project “Model checking and satisfiability: development of novel decision procedures and comparative evaluation and experimental analysis in significant application areas - Moses”, protocol number 9909261583. The first, second and fourth authors are sponsored by the CALCULEMUS! IHP-RTN EC project, contract code HPRN-CT-2000-00102, and have thus benefited of the financial contribution of the Commission through the IHP program.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
P. A. Abdullah, P. Bjesse, and N. Een. Symbolic Reachability Analysis based on SAT-Solvers. In Sixth Int.nl Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’00), 2000.
A. Biere, A. Cimatti, E. M. Clarke, and Yunshan Zhu. Symbolic Model Checking without BDDs. In Proc. TACAS’99, pages 193–207, 1999.
A. Biere, E. Clarke, R. Raimi, and Y. Zhu. Verifying safety proeprties of a power pc microprocessor using symbolic model checking without BDDs. In Proc CAV99, volume 1633 of LNCS, pages 60–71, Berlin, 1999. Springer.
R. E. Bryant. Symbolic Boolean manipulation with ordered binary-decision diagrams. ACM Computing Surveys, 24(3):293–318, September 1992.
J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. J. Hwang. Symbolic Model Checking: 1020 States and Beyond. Information and Computation, 98(2):142–170, June 1992.
A. Cimatti, E. M. Clarke, F. Giunchiglia, and M. Roveri. NuSMV: a new symbolic model checker. International Journal on Software Tools for Technology Transfer (STTT), 2(4), March 2000.
E. Clarke, O. Grumberg, and D. Long. Model Checking. In Proceedings of the International Summer School on Deductive Program Design, Marktoberdorf, Germany, 1994.
E.M. Clarke, E.A. Emerson, and A.P. Sistla. Automatic verification of finitestate concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems, 8(2):244–263, 1986.
F. Copty, L. Fix, E. Giunchiglia, G. Kamhi, A. Tacchella, and M. Vardi. Benefits of Bounded Model Checking at an Industrial Setting. In Proc. CAV’2001, LNCS, Berlin, 2001. Springer.
E. Giunchiglia and R. Sebastiani. Applying the Davis-Putnam procedure to nonclausal formulas. In Proc. AI*IA’99, number 1792 in Lecture Notes in Artificial Intelligence. Springer Verlag, 1999.
K.L. McMillan. Symbolic Model Checking. Kluwer Academic Publ., 1993.
D.A. Plaisted and S. Greenbaum. A Structure-preserving Clause Form Translation. Journal of Symbolic Computation, 2:293–304, 1986.
D. Sheridan and T. Walsh. Clause Forms Generated by Bounded Model Checking. In Proc. Eighth Workshop on Automated Reasoning: Bridging the Gap between Theory and Practice, University of York, March 2001.
O. Shtrichmann. Tuning SAT checkers for bounded model checking. In Conference of Computer Aided Verification, volume 1855 of LNCS, pages 480–494, Berlin, 2000. Springer.
M. Y. Vardi and P. Wolper. Automata-Theoretic Techniques for Modal Logics of Programs. Journal of Computer and System Sciences, 32:183–221, 1986.
P. F. Williams, A. Biere, E. M. Clarke, and A. Gupta. Combining Decision Diagrams and SAT Procedures for Efficient Symbolic Model Checking. In Proc. CAV’2000, volume 1855 of LNCS, pages 124–138, Berlin, 2000. Springer.
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
Cimatti, A., Pistore, M., Roveri, M., Sebastiani, R. (2002). Improving the Encoding of LTL Model Checking into SAT. In: Cortesi, A. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2002. Lecture Notes in Computer Science, vol 2294. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-47813-2_14
Download citation
DOI: https://doi.org/10.1007/3-540-47813-2_14
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43631-7
Online ISBN: 978-3-540-47813-3
eBook Packages: Springer Book Archive