Skip to main content
SpringerLink
Log in

An explicit transition system construction approach to LTL satisfiability checking

  • Original Article
  • Published:
Formal Aspects of Computing

Abstract

We propose a novel algorithm for the satisfiability problem for linear temporal logic (LTL). Existing automata-based approaches first transform the LTL formula into a Büchi automaton and then perform an emptiness checking of the resulting automaton. Instead, our approach works on-the-fly by inspecting the formula directly, thus enabling to find a satisfying model quickly without constructing the full automaton. This makes our algorithm particularly fast for satisfiable formulas. We construct experiments on different pattern formulas, the experimental results show that our approach is superior to other solvers under automata-based framework.

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

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. Biere A, Cimatti A, Clarke EM, Zhu Y (1999) Symbolic model checking without BDDs. In: Proceedings of the 5th international conference on tools and algorithms for the construction and analysis of systems, volume 1579 of Lecture notes in computer science. Springer

  2. Burch JR, Clarke EM, McMillan KL, Dill DL, Hwang LJ (1992) Symbolic model checking: \({10^{20}}\) states and beyond. Inf Comput 98(2): 142–170

    Article  MathSciNet  MATH  Google Scholar 

  3. Bradley A (2011) Sat-based model checking without unrolling. In: Jhala R, Schmidt D (eds) Verification, model checking, and abstract interpretation, volume 6538 of Lecture notes in computer science, pp 70–87. Springer, Berlin

  4. Bryant RE (1986) Graph-based algorithms for Boolean-function manipulation. IEEE Trans Comput C-35(8):677–691

  5. Bryant RE (1992) Symbolic boolean manipulation with ordered binary-decision diagrams. ACM Comput Surv 24(3): 293–318

    Article  MathSciNet  Google Scholar 

  6. Clarke EM, Bierea A, Raimi R, Zhu Y (2001) Bounded model checking using satisfiability solving. Formal Methods Syst Des 19(1): 7–34

    Article  MATH  Google Scholar 

  7. Cimatti A, Clarke EM, Giunchiglia E, Giunchiglia F, Pistore M, Roveri M, Sebastiani R, Tacchella A (2002) Nusmv 2: an opensource tool for symbolic model checking. In: Computer aided verification, Lecture notes in computer science 2404, pp 359–364. Springer

  8. Cimatti A, Clarke EM, Giunchiglia F, Roveri M (2000) NuSMV: a new symbolic model checker. Int J Softw Tools Technol Transf 2(4): 410–425

    Article  MATH  Google Scholar 

  9. Clarke EM, Grumberg O, Peled D (1999) Model checking. MIT Press, Cambridge

    Google Scholar 

  10. Cimatti A, Pistore M, Roveri M, Sebastiani R (2002) Improving the encoding of ltl model checking into sat. In: Revised papers from the third international workshop on verification, model checking, and abstract interpretation, VMCAI ’02, pp 196–207. Springer, London

  11. Cimatti A, Roveri M, Schuppan V, Tonetta S (2007) Boolean abstraction for temporal logic satisfiability. In: Proceedings of the 15th international conference on computer aided verification, volume 4590 of Lecture notes in computer science, pp 532–546. Springer

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

    Article  MATH  Google Scholar 

  13. Dwyer MB, Avrunin GS, Corbett JC (1998) Property specification patterns for finite-state verification. In: Proceedings of the 2nd workshop on formal methods in software practice, pp 7–15. ACM

  14. De Wulf M, Doyen L, Maquet N, Raskin J-F (2008) Antichains: alternative algorithms for ltl satisfiability and model-checking. In: Tools and algorithms for the construction and analysis of systems, volume 4963 of Lecture notes in computer science, pp 63–77. Springer

  15. Daniele N, Guinchiglia F, Vardi MY (1999) Improved automata generation for linear temporal logic. In: Proceedings of the 11th intenational conference on computer aided verification, volume 1633 of Lecture notes in computer science, pp 249–260. Springer

  16. 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, pp 76–83. IEEE Computer Society

  17. Duan Z, Tian C, Zhang L (2008) A decision procedure for propositional projection temporal logic with infinite models. Acta Inf 45(1): 43–78

    Article  MathSciNet  MATH  Google Scholar 

  18. Eén N, Sörensson N (2003) An extensible sat-solver. In: SAT, pp 502–518

  19. Fisher M, Dixon C, Peim M (2001) Clausal temporal resolution. ACM Trans Comput Logic 2(1): 12–56

    Article  MathSciNet  MATH  Google Scholar 

  20. Fisher M (1991) A resolution method for temporal logic. In: In proceedings of the twelfth international joint conference on artificial intelligence, pp 99–104. IJCAI, Morgan Kaufman

  21. Foster HD, Krolnik A, Lacey DJ (2004) Assertion-based design. Springer, Berlin

    Google Scholar 

  22. Holzmann GJ (1997) The model checker SPIN. IEEE Trans Softw Eng 23(5): 279–295

    Article  Google Scholar 

  23. Kesten Y, Manna Z, McGuire H, Pnueli A (1993) A decision algorithm for full propositional temporal logic. In: Courcoubeti C (ed) Proceedings of the 5th conference on computer aided verification, volume 697 of Lecture notes in computer science, pp 97–109. Springer

  24. Li J, Pu G, Zhang L, Wang Z, He J, Larsen KG (2013) On the relationship between ltl normal forms and büchi automata. In: Liu Z, Jim W, Zhu H (eds) Theories of programming and formal methods, volume 8051 of Lecture notes in computer science, pp 256–270. Springer

  25. 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–98

  26. McMillan K (1999) The SMV language. Technical report, Cadence Berkeley Lab

  27. McMillan K (2003) Interpolation and sat-based model checking. In: Jr. Hunt, WarrenA, Somenzi Fabio (eds) Computer aided verification, volume 2725 of Lecture notes in computer science, pp 1–13. Springer, Berlin

  28. Pill I, Semprini S, Cavada R, Roveri M, Bloem R, Cimatti A (2006) Formal analysis of hardware requirements. In: Proceedings of the 43rd design automation conference, pp 821–826. ACM

  29. Rozier KY, Vardi MY (2007) LTL satisfiability checking. In: Proceedings of the 14th international SPIN workshop, volume 4595 of Lecture notes in computer science, pp 149–167. Springer

  30. Rozier KY, Vardi MY (2010) LTL satisfiability checking. Int J Softw Tools Technol Transf 12(2): 1230–137

  31. Rozier KY, Vardi MY (2011) A multi-encoding approach for LTL symbolic satisfiability checking. In: Proceedings of the 17th International symposium on formal methods, volume 6664 of Lecture notes in computer science, pp 417–431. Springer

  32. Sistla AP, Clarke EM (1982) The complexity of propositional linear temporal logics. In: Proceedings of the 14th annual ACM symposium on theory of computing, pp 159–168

  33. Sistla AP, Clarke EM (1985) The complexity of propositional linear temporal logic. J ACM 32: 733–749

    Article  MathSciNet  MATH  Google Scholar 

  34. 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, pp 277–292. Springer

  35. Schuppan V (2010) Towards a notion of unsatisfiable cores for ltl. In: Fundamentals of software engineering, pp 129–145

  36. Schuppan V, Darmawan L (2011) Evaluating ltl satisfiability solvers. In: Proceedings of the 9th international conference on Automated technology for verification and analysis, AVTA’11, pp 397–413. Springer

  37. Tarjan RE (1972) Depth first search and linear graph algorithms. SIAM J Comput 1(2): 146–160

    Article  MathSciNet  MATH  Google Scholar 

  38. Vardi MY (2007) Automata-theoretic model checking revisited. In: Proceedings of the 8th international conference on verification, model checking, and abstract interpretation, volume 4349 of Lecture notes in computer science, pp 137–150. Springer

  39. Kyrilov A, Goranko V, Shkatov D (2010) Tableau tool for testing satisfiability in ltl: Implementation and experimental analysis. Electr Notes Theory Comput Sci 262: 113–125

    Article  MathSciNet  Google Scholar 

  40. Vardi MY, Wolper P (1986) An automata-theoretic approach to automatic program verification. In: Proceedings of the 1st IEEE symposium on logic in computer science, pp 332–344

  41. Wolper P (1985) The tableau method for temporal logic: an overview. Logique Anal 110(−111): 119–136

    MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, Shanghai, China

    Jianwen Li, Shufang Zhu, Geguang Pu & Jifeng He

  2. State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing, China

    Lijun Zhang

  3. Computer Science, Rice University, Houston, TX, USA

    Moshe Y. Vardi

Authors
  1. Jianwen Li
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Lijun Zhang
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Shufang Zhu
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Geguang Pu
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Moshe Y. Vardi
    View author publications

    You can also search for this author in PubMed Google Scholar

  6. Jifeng He
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding authors

Correspondence to Shufang Zhu or Geguang Pu.

Additional information

Jim Woodcock

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Li, J., Zhang, L., Zhu, S. et al. An explicit transition system construction approach to LTL satisfiability checking. Form Asp Comp 30, 193–217 (2018). https://doi.org/10.1007/s00165-017-0442-2

Download citation

  • Received:

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s00165-017-0442-2

Keywords

Search

Navigation