Skip to main content
SpringerLink
Log in
Book cover

Haifa Verification Conference

HVC 2015: Hardware and Software: Verification and Testing pp 209–224Cite as

SAT-Based Explicit LTL Reasoning

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 9434))

Abstract

We present here a new explicit reasoning framework for linear temporal logic (LTL), which is built on top of propositional satisfiability (SAT) solving. As a proof-of-concept of this framework, we describe a new LTL satisfiability algorithm. We implemented the algorithm in a tool, Aalta_v2.0, which is built on top of the Minisat SAT solver. We tested the effectiveness of this approach by demonstrating that Aalta_v2.0 significantly outperforms all existing LTL satisfiability solvers.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Notes

  1. 1.

    See http://www.satcompetition.org/.

  2. 2.

    It can be downloaded at www.lab205.org/aalta.

  3. 3.

    http://cgi.csc.liv.ac.uk/~konev/software/trp++/.

References

  1. Bradley, A.R.: SAT-based model checking without unrolling. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 70–87. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  2. Cavada, R., Cimatti, A., Dorigatti, M., Griggio, A., Mariotti, A., Micheli, A., Mover, S., Roveri, M., Tonetta, S.: The nuXmv symbolic model checker. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 334–342. Springer, Heidelberg (2014)

    Google Scholar 

  3. Claessen, K., Sörensson, N.: A liveness checking algorithm that counts. In: Cabodi, G., Singh, S. (ed.) FMCAD, pp. 52–59. IEEE (2012)

    Google Scholar 

  4. Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)

    Google Scholar 

  5. Courcoubetis, C., Vardi, M.Y., Wolper, P., Yannakakis, M.: Memory efficient algorithms for the verification of temporal properties. Formal Methods Syst. Des. 1, 275–288 (1992)

    Article  MATH  Google Scholar 

  6. D’Agostino, M.: Tableau methods for classical propositional logic. In: D’Agostino, M., Gabbay, D.M., Hähnle, R., Posegga, J. (eds.) Handbook of Tableau Methods, pp. 45–123. Springer, Netherlands (1999)

    Chapter  Google Scholar 

  7. Daniele, M., Giunchiglia, F., Vardi, M.Y.: Improved automata generation for linear temporal logic. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 249–260. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  8. Duret-Lutz, A., Poitrenaud, D: SPOT: an extensible model checking library using transition-based generalized büchi automata. In: Proceedings of the 12th International Workshop on Modeling, Analysis, and Simulation of Computer and Telecommunication Systems, pp. 76–83. IEEE Computer Society (2004)

    Google Scholar 

  9. Eén, N., Sörensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  10. Fisher, M.: A normal form for temporal logics and its applications in theorem-proving and execution. J. Logic Comput. 7(4), 429–456 (1997)

    Article  MathSciNet  MATH  Google Scholar 

  11. Gerth, R., Peled, D., Vardi, M.Y., Wolper, P.: Simple on-the-fly automatic verification of linear temporal logic. In: Dembiski, P., Sredniawa, M. (eds.) Protocol Specification, Testing, and Verification, pp. 3–18. Chapman & Hall, Warsaw (1995)

    Google Scholar 

  12. Giunchiglia, F., Sebastiani, R.: Building decision procedures for modal logics from propositional decision procedures - the case study of modal K. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS, vol. 1104, pp. 583–597. Springer, Heidelberg (1996)

    Chapter  Google Scholar 

  13. Heljanko, K., Junttila, T.A., Latvala, T.: Incremental and complete bounded model checking for full PLTL. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 98–111. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  14. Holzmann, G.J.: The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley, Reading (2003)

    Google Scholar 

  15. Hustadt, U., Konev, B.: TRP++ 2.0: a temporal resolution prover. In: Baader, F. (ed.) CADE 2003. LNCS (LNAI), vol. 2741, pp. 274–278. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  16. Larrabee, T.: Test pattern generation using Boolean satisfiability. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst 11(1), 4–15 (1992)

    Article  Google Scholar 

  17. Li, J., Pu, G., Zhang, L., Vardi, M.Y., He, J.: Fast LTL satisfiability checking by SAT solvers. CoRR, abs/1401.5677 (2014)

    Google Scholar 

  18. Li, J., Zhang, L., Pu, G., Vardi, M., He, J.: LTL satisfibility checking revisited. In: 20th International Symposium on Temporal Representation and Reasoning, pp. 91–98 (2013)

    Google Scholar 

  19. Malik, S., Zhang, L.: Boolean satisfiability from theoretical hardness to practical success. Commun. ACM 52(8), 76–82 (2009)

    Article  Google Scholar 

  20. Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer, New York (1992)

    Book  MATH  Google Scholar 

  21. Marques-Silva, J., Lynce, I.: On improving MUS extraction algorithms. In: Sakallah, K.A., Simon, L. (eds.) SAT 2011. LNCS, vol. 6695, pp. 159–173. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  22. McMillan, K.L.: Interpolation and SAT-based model checking. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 1–13. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  23. McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Publishers, Boston (1993)

    Book  MATH  Google Scholar 

  24. Pnueli, A.: The temporal logic of programs. In: Proceedings of the 18th IEEE Symposium on Foundations of Computer Science, pp. 46–57 (1977)

    Google Scholar 

  25. Rozier, K.Y., Vardi, M.Y.: LTL satisfiability checking. Int. J. Softw. Tools Technol. Transf. 12(2), 123–137 (2010)

    Article  Google Scholar 

  26. Schuppan, V., Darmawan, L.: Evaluating LTL satisfiability solvers. In: Bultan, T., Hsiung, P.-A. (eds.) ATVA 2011. LNCS, vol. 6996, pp. 397–413. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  27. Schwoon, S., Esparza, J.: A note on on-the-fly verification algorithms. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 174–190. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  28. Somenzi, F., Bloem, R.: Efficient Büchi automata from LTL formulae. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  29. Suda, M., Weidenbach, C.: A PLTL-prover based on labelled superposition with partial model guidance. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol. 7364, pp. 537–543. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  30. Tabakov, D., Rozier, K.Y., Vardi, M.Y.: Optimized temporal monitors for SystemC. Formal Methods Syst. Des. 41(3), 236–268 (2012)

    Article  MATH  Google Scholar 

  31. Vardi, M.: On the complexity of epistemic reasoning. In: Proceedings of the Fourth Annual Symposium on Logic in Computer Science, pp. 243–252. IEEE Press, Piscataway (1989)

    Google Scholar 

  32. Vardi, M.Y.: Unified verification theory. In: Banieqbal, B., Barringer, H., Pnueli, A. (eds.) Temporal Logic in Specification. LNCS, vol. 398, pp. 202–212. Springer, Heidelberg (1989)

    Chapter  Google Scholar 

  33. Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Proceedings of the 1st IEEE Symposium on Logic in Computer Science, pp. 332–344 (1986)

    Google Scholar 

Download references

Acknowledgment

The authors thank anonymous reviewers for useful comments. The work is supported in part by NSF grants CCF-1319459, by NSF Expeditions in Computing project “ExCAPE: Expeditions in Computer Augmented Program Engineering”, and by BSF grant 9800096. Geguang Pu is partially supported by the NSFC grants No. 61202069 and No. 61361136002. Jianwen Li is partially supported by Shanghai Collaborative Innovation Center of Trustworthy Software for Internet of Things (ZF1213).

Author information

Authors and Affiliations

  1. Department of Computer Science, Rice University, Houston, USA

    Jianwen Li & Moshe Y. Vardi

  2. Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, Shanghai, People’s Republic of China

    Jianwen Li, Shufang Zhu & Geguang Pu

Authors
  1. Jianwen Li
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Shufang Zhu
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Geguang Pu
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Moshe Y. Vardi
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Jianwen Li .

Editor information

Editors and Affiliations

  1. University of Leicester, Leicester, United Kingdom

    Nir Piterman

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer International Publishing Switzerland

About this paper

Cite this paper

Li, J., Zhu, S., Pu, G., Vardi, M.Y. (2015). SAT-Based Explicit LTL Reasoning. In: Piterman, N. (eds) Hardware and Software: Verification and Testing. HVC 2015. Lecture Notes in Computer Science(), vol 9434. Springer, Cham. https://doi.org/10.1007/978-3-319-26287-1_13

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-26287-1_13

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-26286-4

  • Online ISBN: 978-3-319-26287-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation