×

SAT-based explicit LTL reasoning and its application to satisfiability checking. (English) Zbl 1425.68259

Summary: 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.

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
03B44 Temporal logic
68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
PDFBibTeX XMLCite
Full Text: DOI

References:

[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] Bradley, A.; Jhala, R. (ed.); Schmidt, D. (ed.), SAT-based model checking without unrolling, No. 6538, 70-87 (2011), Berlin · Zbl 1317.68109
[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-342
[4] Cimatti, A.; Clarke, E.; Giunchiglia, E.; Giunchiglia, F.; Pistore, M.; Roveri, M.; Sebastiani, R.; Tacchella, A.; Brinksma, E. (ed.); Larsen, KG (ed.), Nusmv 2: an opensource tool for symbolic model checking, No. 2404, 359-364 (2002), Berlin · Zbl 1010.68766
[5] Claessen K, Sörensson N (2012) A liveness checking algorithm that counts. In: Cabodi G, Singh S (eds) FMCAD, pp 52-59. IEEE
[6] Clarke E, Grumberg O, Peled D (1999) Model checking. MIT Press, Cambridge · Zbl 1423.68002
[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-288
[8] D’Agostino, M.; D’Agostino, M. (ed.); Gabbay, D. (ed.); Haehnle, R. (ed.); Posegga, J. (ed.), Tableau methods for classical propositional logic, 45-123 (1999), Dordrecht · Zbl 0972.03523
[9] Daniele, Marco; Giunchiglia, Fausto; Vardi, Moshe Y., Improved Automata Generation for Linear Temporal Logic, 249-260 (1999), Berlin, Heidelberg · Zbl 1046.68588
[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-83
[11] Eén N, Sörensson N (2003) An extensible SAT-solver. In: SAT, pp 502-518 · Zbl 1204.68191
[12] Fisher M (1997) A normal form for temporal logics and its applications in theorem-proving and execution. J Log Comput 7(4):429-456 · Zbl 0893.03003
[13] Fisher M, Dixon C, Peim M (2001) Clausal temporal resolution. ACM Trans Comput Log 2(1):12-56 · Zbl 1365.03017
[14] Gerth, R.; Peled, D.; Vardi, M.; Wolper, P.; Dembiski, P. (ed.); Sredniawa, M. (ed.), Simple on-the-fly automatic verification of linear temporal logic, 3-18 (1995), Boca Raton
[15] Giunchiglia, Fausto; Sebastiani, Roberto, Building decision procedures for modal logics from propositional decision procedures — The case study of modal K, 583-597 (1996), Berlin, Heidelberg · Zbl 1415.03022
[16] Heljanko, K.; Junttila, T.; Latvala, T.; Etessami, K. (ed.); Rajamani, S. (ed.), Incremental and complete bounded model checking for full PLTL, No. 3576, 98-111 (2005), Berlin · Zbl 1081.68621
[17] Holzmann G (2003) The SPIN model checker: primer and reference manual. Addison-Wesley, Boston
[18] Hustadt, Ullrich; Konev, Boris, TRP++ 2.0: A Temporal Resolution Prover, 274-278 (2003), Berlin, Heidelberg
[19] Kaminski, Mark; Tebbi, Tobias, InKreSAT: Modal Reasoning via Incremental Reduction to SAT, 436-442 (2013), Berlin, Heidelberg · Zbl 1381.68272
[20] Larrabee T (1992) Test pattern generation using boolean satisfiability. IEEE Trans Comput Aided Des Integr Circuits Syst 11(1):4-15
[21] Li J, Pu G, Zhang L, Vardi MY, He J (2014) Fast LTL satisfiability checking by SAT solvers. CoRR arXiv:1401.5677 · Zbl 1410.68235
[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-98
[23] Li J, Zhu S, Pu G, Vardi M (2015) SAT-based explicit LTL reasoning. Springer, Berlin, pp 209-224
[24] Malik S, Zhang L (2009) Boolean satisfiability from theoretical hardness to practical success. Commun ACM 52(8):76-82
[25] Manna Z, Pnueli A (1992) The temporal logic of reactive and concurrent systems: specification. Springer, Berlin
[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-239
[27] Marques-Silva, J.; Lynce, I.; Sakallah, K. (ed.); Simon, L. (ed.), On improving MUS extraction algorithms, No. 6695, 159-173 (2011), Berlin · Zbl 1330.68273
[28] McMillan K (1993) Symbolic model checking. Kluwer Academic Publishers, Dordrecht · Zbl 1132.68474
[29] McMillan, K. L., Interpolation and SAT-Based Model Checking, 1-13 (2003), Berlin, Heidelberg · Zbl 1278.68184
[30] Pnueli A (1977) The temporal logic of programs. In: Proceedings of 18th IEEE symposium on foundations of computer science, pp 46-57
[31] Rozier K, Vardi M (2010) LTL satisfiability checking. Int J Softw Tools Technol Transf 12(2):123-137
[32] Schuppan, Viktor; Darmawan, Luthfi, Evaluating LTL Satisfiability Solvers, 397-413 (2011), Berlin, Heidelberg
[33] Schwendimann, Stefan, A New One-Pass Tableau Calculus for PLTL, 277-291 (1998), Berlin, Heidelberg · Zbl 0903.03015
[34] Schwoon, Stefan; Esparza, Javier, A Note on On-the-Fly Verification Algorithms, 174-190 (2005), Berlin, Heidelberg · Zbl 1087.68599
[35] Somenzi, Fabio; Bloem, Roderick, Efficient Büchi Automata from LTL Formulae, 248-263 (2000), Berlin, Heidelberg · Zbl 0974.68086
[36] Suda M (2015) Variable and clause elimination for LTL satisfiability checking. Math Comput Sci 9(3):327-344 · Zbl 1341.68197
[37] Suda, Martin; Weidenbach, Christoph, A PLTL-Prover Based on Labelled Superposition with Partial Model Guidance, 537-543 (2012), Berlin, Heidelberg · Zbl 1358.68266
[38] Tabakov D, Rozier K, Vardi MY (2012) Optimized temporal monitors for SystemC. Form Methods Syst Des 41(3):236-268 · Zbl 1284.68206
[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-252
[40] Vardi, Moshe Y., Unified verification theory, 202-212 (1989), Berlin, Heidelberg
[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-344
[42] Williams, Richard; Konev, Boris, Propositional Temporal Proving with Reductions to a SAT Problem, 421-435 (2013), Berlin, Heidelberg · Zbl 1381.68277
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.