Advertisement

SAT-based explicit LTL reasoning and its application to satisfiability checking

  • Jianwen Li
  • Shufang Zhu
  • Geguang PuEmail author
  • Lijun Zhang
  • Moshe Y. Vardi
Article
  • 35 Downloads

Abstract

We present here a new explicit reasoning framework for linear temporal logic (LTL), which is built on top of propositional satisfiability (SAT) solving. The crux of our approach is a construction of temporal transition system that is based on SAT-solving rather than tableau to construct states and transitions. As a proof-of-concept of this framework, we describe a new LTL satisfiability algorithm. We tested the effectiveness of this approach by demonstrating that it significantly outperforms all existing LTL-satisfiability-checking algorithms.

Keywords

Satisfiability checking Linear temporal logic SAT-based LTL checking 

Notes

Acknowledgements

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. Jianwen Li is partially supported by NSFC Projects No. 61572197 and No. 61632005. Geguang Pu is partially supported by MOST NKTSP Project 2015BAG19G02 (Grant No. ZF1213) and STCSM Project No. 16DZ1100600. Lijun Zhang is supported by NSFC Grant No. 61532019.

References

  1. 1.
    Bertello M, Gigante N, Montanari A, Reynolds M (2016) Leviathan: a new LTL satisfiability checking tool based on a one-pass tree-shaped tableau. In: Proceedings of the twenty-fifth international joint conference on artificial intelligence, IJCAI’16, pp 950–956. AAAI Press. http://dl.acm.org/citation.cfm?id=3060621.3060753
  2. 2.
    Bradley A (2011) SAT-based model checking without unrolling. In: Jhala R, Schmidt D (eds) Verification, model checking, and abstract interpretation. Lecture notes in computer science, vol 6538. Springer, Berlin, pp 70–87CrossRefGoogle Scholar
  3. 3.
    Cavada R, Cimatti A, Dorigatti M, Griggio A, Mariotti A, Micheli A, Mover S, Roveri M, Tonetta S (2014) The nuXmv symbolic model checker. In: CAV, pp 334–342Google Scholar
  4. 4.
    Cimatti A, Clarke E, Giunchiglia E, Giunchiglia F, Pistore M, Roveri M, Sebastiani R, Tacchella A (2002) Nusmv 2: an opensource tool for symbolic model checking. In: Brinksma E, Larsen KG (eds) Computer aided verification. Lecture notes in computer science, vol 2404. Springer, Berlin, pp 359–364CrossRefGoogle Scholar
  5. 5.
    Claessen K, Sörensson N (2012) A liveness checking algorithm that counts. In: Cabodi G, Singh S (eds) FMCAD, pp 52–59. IEEEGoogle Scholar
  6. 6.
    Clarke E, Grumberg O, Peled D (1999) Model checking. MIT Press, CambridgeGoogle Scholar
  7. 7.
    Courcoubetis C, Vardi M, Wolper P, Yannakakis M (1992) Memory efficient algorithms for the verification of temporal properties. Form Methods Syst Des 1:275–288CrossRefzbMATHGoogle Scholar
  8. 8.
    D’Agostino M (1999) Tableau methods for classical propositional logic. In: D’Agostino M, Gabbay D, Haehnle R, Posegga J (eds) Handbook of tableau methods. Springer, Dordrecht, pp 45–123CrossRefGoogle Scholar
  9. 9.
    Daniele N, Guinchiglia F, Vardi M (1999) Improved automata generation for linear temporal logic. In: Proceedings of the 11th international conference on computer aided verification. Lecture notes in computer science, vol 1633. Springer, Berlin, pp 249–260Google Scholar
  10. 10.
    Duret-Lutz A, Poitrenaud D (2004) 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. IEEE Computer Society, pp 76–83Google Scholar
  11. 11.
    Eén N, Sörensson N (2003) An extensible SAT-solver. In: SAT, pp 502–518Google Scholar
  12. 12.
    Fisher M (1997) A normal form for temporal logics and its applications in theorem-proving and execution. J Log Comput 7(4):429–456MathSciNetCrossRefzbMATHGoogle Scholar
  13. 13.
    Fisher M, Dixon C, Peim M (2001) Clausal temporal resolution. ACM Trans Comput Log 2(1):12–56MathSciNetCrossRefzbMATHGoogle Scholar
  14. 14.
    Gerth R, Peled D, Vardi M, Wolper P (1995) Simple on-the-fly automatic verification of linear temporal logic. In: Dembiski P, Sredniawa M (eds) Protocol specification, testing, and verification. Chapman & Hall, Boca Raton, pp 3–18Google Scholar
  15. 15.
    Giunchiglia F, Sebastiani R (1996) Building decision procedures for modal logics from propositional decision procedure—the case study of modal K. In: Proceedings of 13th international conference on automated deduction. Lecture notes in computer science, vol 1104. Springer, Berlin, pp 583–597Google Scholar
  16. 16.
    Heljanko K, Junttila T, Latvala T (2005) Incremental and complete bounded model checking for full PLTL. In: Etessami K, Rajamani S (eds) Computer aided verification. Lecture notes in computer science, vol 3576. Springer, Berlin, pp 98–111CrossRefGoogle Scholar
  17. 17.
    Holzmann G (2003) The SPIN model checker: primer and reference manual. Addison-Wesley, BostonGoogle Scholar
  18. 18.
    Hustadt U, Konev B (2003) Trp++ 2.0: a temporal resolution prover. In: Proceedings of CADE-19. LNAI. Springer, Berlin, pp 274–278Google Scholar
  19. 19.
    Kaminski M, Tebbi T (2013) Inkresat: modal reasoning via incremental reduction to sat. In: Bonacina MP (ed) International conference on automated deduction—CADE-24. Springer, Berlin, pp 436–442Google Scholar
  20. 20.
    Larrabee T (1992) Test pattern generation using boolean satisfiability. IEEE Trans Comput Aided Des Integr Circuits Syst 11(1):4–15CrossRefGoogle Scholar
  21. 21.
    Li J, Pu G, Zhang L, Vardi MY, He J (2014) Fast LTL satisfiability checking by SAT solvers. CoRR arXiv:1401.5677
  22. 22.
    Li J, Zhang L, Pu G, Vardi M, He J (2013) LTL satisfibility checking revisited. In: The 20th international symposium on temporal representation and reasoning, pp 91–98Google Scholar
  23. 23.
    Li J, Zhu S, Pu G, Vardi M (2015) SAT-based explicit LTL reasoning. Springer, Berlin, pp 209–224Google Scholar
  24. 24.
    Malik S, Zhang L (2009) Boolean satisfiability from theoretical hardness to practical success. Commun ACM 52(8):76–82CrossRefGoogle Scholar
  25. 25.
    Manna Z, Pnueli A (1992) The temporal logic of reactive and concurrent systems: specification. Springer, BerlinCrossRefzbMATHGoogle Scholar
  26. 26.
    Manquinho VM, Flores PF, Silva JPM, Oliveira AL (1997) Prime implicant computation using satisfiability algorithms. In: Proceedings of ninth IEEE international conference on tools with artificial intelligence, pp 232–239Google Scholar
  27. 27.
    Marques-Silva J, Lynce I (2011) On improving MUS extraction algorithms. In: Sakallah K, Simon L (eds) Theory and applications of satisfiability testing—SAT 2011. Lecture notes in computer science, vol 6695. Springer, Berlin, pp 159–173CrossRefGoogle Scholar
  28. 28.
    McMillan K (1993) Symbolic model checking. Kluwer Academic Publishers, DordrechtCrossRefzbMATHGoogle Scholar
  29. 29.
    McMillan K (2003) Interpolation and SAT-based model checking. In: Hunt WA Jr., Somenzi F (eds) International conference on computer aided verification. Lecture notes in computer science, vol 2725. Springer, Berlin, pp 1–13Google Scholar
  30. 30.
    Pnueli A (1977) The temporal logic of programs. In: Proceedings of 18th IEEE symposium on foundations of computer science, pp 46–57Google Scholar
  31. 31.
    Rozier K, Vardi M (2010) LTL satisfiability checking. Int J Softw Tools Technol Transf 12(2):123–137CrossRefGoogle Scholar
  32. 32.
    Schuppan V, Darmawan L (2011) Evaluating LTL satisfiability solvers. In: Proceedings of the 9th international conference on automated technology for verification and analysis, ATVA’11. Springer, Berlin, pp 397–413Google Scholar
  33. 33.
    Schwendimann S (1998) A new one-pass tableau calculus for PLTL. In: Proceedings of the international conference on automated reasoning with analytic tableaux and related methods. Springer, Berlin, pp 277–292Google Scholar
  34. 34.
    Schwoon S, Esparza J (2005) A note on on-the-fly verification algorithms. In: Proceedings 11th international conference on tools and algorithms for the construction and analysis of systems. Lecture notes in computer science, vol 3440. Springer, Berlin, pp 174–190Google Scholar
  35. 35.
    Somenzi F, Bloem R (2000) Efficient Büchi automata from LTL formulae. In: Proceedings of 12th international conference on computer aided verification. Lecture notes in computer science, vol 1855. Springer, Berlin, pp 248–263Google Scholar
  36. 36.
    Suda M (2015) Variable and clause elimination for LTL satisfiability checking. Math Comput Sci 9(3):327–344MathSciNetCrossRefzbMATHGoogle Scholar
  37. 37.
    Suda M, Weidenbach C (2012) A PLTL-prover based on labelled superposition with partial model guidance. In: International joint conference on automated reasoning. Lecture notes in computer science, vol 7364. Springer, Berlin, pp 537–543Google Scholar
  38. 38.
    Tabakov D, Rozier K, Vardi MY (2012) Optimized temporal monitors for SystemC. Form Methods Syst Des 41(3):236–268CrossRefzbMATHGoogle Scholar
  39. 39.
    Vardi M (1989) On the complexity of epistemic reasoning. In: Proceedings of the fourth annual symposium on logic in computer science. IEEE Press, Piscataway, pp 243–252Google Scholar
  40. 40.
    Vardi M (1989) Unified verification theory. In: Banieqbal B, Barringer H, Pnueli A (eds) Proceedings of temporal logic in specification, vol 398. Springer, Berlin, pp 202–212Google Scholar
  41. 41.
    Vardi M, Wolper P (1986) An automata-theoretic approach to automatic program verification. In: Proceedings of 1st IEEE symposium on logic in computer science, pp 332–344Google Scholar
  42. 42.
    Williams R, Konev B (2013) Propositional temporal proving with reductions to a sat problem. In: Bonacina MP (ed) International conference on automated deduction—CADE-24. Springer, Berlin, pp 421–435Google Scholar

Copyright information

© Springer Science+Business Media, LLC, part of Springer Nature 2019

Authors and Affiliations

  1. 1.Rice UniversityHoustonUSA
  2. 2.East China Normal UniversityShanghaiChina
  3. 3.University of Chinese Academy of SciencesBeijingChina

Personalised recommendations