Formal Aspects of Computing

, Volume 30, Issue 2, pp 193–217 | Cite as

An explicit transition system construction approach to LTL satisfiability checking

Original Article
  • 31 Downloads

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.

Keywords

LTL satisfiability checking Obligation set LTL transition system 

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. BCCZ99.
    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. SpringerGoogle Scholar
  2. BCM+92.
    Burch JR, Clarke EM, McMillan KL, Dill DL, Hwang LJ (1992) Symbolic model checking: \({10^{20}}\) states and beyond. Inf Comput 98(2): 142–170MathSciNetCrossRefMATHGoogle Scholar
  3. Bra11.
    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, BerlinGoogle Scholar
  4. Bry86.
    Bryant RE (1986) Graph-based algorithms for Boolean-function manipulation. IEEE Trans Comput C-35(8):677–691Google Scholar
  5. Bry92.
    Bryant RE (1992) Symbolic boolean manipulation with ordered binary-decision diagrams. ACM Comput Surv 24(3): 293–318MathSciNetCrossRefGoogle Scholar
  6. CBRZ01.
    Clarke EM, Bierea A, Raimi R, Zhu Y (2001) Bounded model checking using satisfiability solving. Formal Methods Syst Des 19(1): 7–34CrossRefMATHGoogle Scholar
  7. CCG+02.
    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. SpringerGoogle Scholar
  8. CCGR00.
    Cimatti A, Clarke EM, Giunchiglia F, Roveri M (2000) NuSMV: a new symbolic model checker. Int J Softw Tools Technol Transf 2(4): 410–425CrossRefMATHGoogle Scholar
  9. CGP99.
    Clarke EM, Grumberg O, Peled D (1999) Model checking. MIT Press, CambridgeGoogle Scholar
  10. CPRS02.
    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, LondonGoogle Scholar
  11. CRST07.
    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. SpringerGoogle Scholar
  12. CVWY92.
    Courcoubetis C, Vardi MY, Wolper P, Yannakakis M (1992) Memory efficient algorithms for the verification of temporal properties. Formal Methods Syst Des 1: 275–288CrossRefMATHGoogle Scholar
  13. DAC98.
    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. ACMGoogle Scholar
  14. DDMR08.
    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. SpringerGoogle Scholar
  15. DGV99.
    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. SpringerGoogle Scholar
  16. DLP04.
    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 SocietyGoogle Scholar
  17. DTZ08.
    Duan Z, Tian C, Zhang L (2008) A decision procedure for propositional projection temporal logic with infinite models. Acta Inf 45(1): 43–78MathSciNetCrossRefMATHGoogle Scholar
  18. ES03.
    Eén N, Sörensson N (2003) An extensible sat-solver. In: SAT, pp 502–518Google Scholar
  19. FDP01.
    Fisher M, Dixon C, Peim M (2001) Clausal temporal resolution. ACM Trans Comput Logic 2(1): 12–56MathSciNetCrossRefMATHGoogle Scholar
  20. Fis91.
    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 KaufmanGoogle Scholar
  21. FKL04.
    Foster HD, Krolnik A, Lacey DJ (2004) Assertion-based design. Springer, BerlinGoogle Scholar
  22. Hol97.
    Holzmann GJ (1997) The model checker SPIN. IEEE Trans Softw Eng 23(5): 279–295CrossRefGoogle Scholar
  23. KMMP93.
    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. SpringerGoogle Scholar
  24. LPZ+13.
    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. SpringerGoogle Scholar
  25. LZP+13.
    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
  26. McM99.
    McMillan K (1999) The SMV language. Technical report, Cadence Berkeley LabGoogle Scholar
  27. McM03.
    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, BerlinGoogle Scholar
  28. PSC+06.
    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. ACMGoogle Scholar
  29. RV07.
    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. SpringerGoogle Scholar
  30. RV10.
    Rozier KY, Vardi MY (2010) LTL satisfiability checking. Int J Softw Tools Technol Transf 12(2): 1230–137Google Scholar
  31. RV11.
    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. SpringerGoogle Scholar
  32. SC82.
    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–168Google Scholar
  33. SC85.
    Sistla AP, Clarke EM (1985) The complexity of propositional linear temporal logic. J ACM 32: 733–749MathSciNetCrossRefMATHGoogle Scholar
  34. Sch98.
    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. SpringerGoogle Scholar
  35. Sch10.
    Schuppan V (2010) Towards a notion of unsatisfiable cores for ltl. In: Fundamentals of software engineering, pp 129–145Google Scholar
  36. SD11.
    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. SpringerGoogle Scholar
  37. Tar72.
    Tarjan RE (1972) Depth first search and linear graph algorithms. SIAM J Comput 1(2): 146–160MathSciNetCrossRefMATHGoogle Scholar
  38. Var07.
    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. SpringerGoogle Scholar
  39. VGS10.
    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–125MathSciNetCrossRefGoogle Scholar
  40. VW86.
    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–344Google Scholar
  41. Wol85.
    Wolper P (1985) The tableau method for temporal logic: an overview. Logique Anal 110(−111): 119–136MathSciNetMATHGoogle Scholar

Copyright information

© British Computer Society 2017

Authors and Affiliations

  1. 1.Shanghai Key Laboratory of Trustworthy ComputingEast China Normal UniversityShanghaiChina
  2. 2.State Key Laboratory of Computer ScienceInstitute of Software, Chinese Academy of SciencesBeijingChina
  3. 3.Computer ScienceRice UniversityHoustonUSA

Personalised recommendations