zbMATH — the first resource for mathematics

Variable and clause elimination for LTL satisfiability checking. (English) Zbl 1341.68197
Summary: We study preprocessing techniques for clause normal forms of LTL formulas. Applying the mechanism of labeled clauses enables us to reinterpret LTL satisfiability as a set of purely propositional problems and thus to transfer simplification ideas from SAT to LTL. We demonstrate this by adapting variable and clause elimination, a very effective preprocessing technique used by modern SAT solvers. Our experiments confirm that even in the temporal setting substantial reductions in formula size and subsequent decrease of solver runtime can be achieved.

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
03B35 Mechanization of proofs and logical operations
03B44 Temporal logic
MiniSat; TRP++
PDF BibTeX Cite
Full Text: DOI
[1] Bolotov, A.; Fisher, M.; Dixon, C., On the relationship between \(ω\)-automata and temporal logic normal forms, J. Logic Comput., 12, 561-581, (2002) · Zbl 1007.03014
[2] Clarke, E.M.; Grumberg, O.; Hamaguchi, K., Another look at LTL model checking, Form. Methods Syst. Des., 10, 47-71, (1997)
[3] Clarke E.M., Grumberg O., Peled D.: Model checking. MIT Press, Cambridge (2001) · Zbl 0847.68063
[4] Degtyarev, A., Fisher, M., Konev, B.: A simplified clausal resolution procedure for propositional linear-time temporal logic. In: TABLEAUX ’02. LNCS, vol. 2381, pp. 85-99. Springer, Berlin (2002) · Zbl 1015.03015
[5] Eén, N., Biere, A.: Effective preprocessing in SAT through variable and clause elimination. In: SAT’05. LNCS, vol. 3569, pp. 61-75. Springer, Berlin (2005) · Zbl 1128.68463
[6] Eén, N., Sörensson, N.: An extensible SAT-solver. In: SAT’03. LNCS, vol. 2919, pp. 502-518. Springer, Berlin (2003) · Zbl 1204.68191
[7] Fisher, M.: A resolution method for temporal logic. In: IJCAI’91, pp. 99-104. Morgan Kaufmann Publishers Inc., Menlo Park (1991) · Zbl 0745.68091
[8] Fisher, M.; Dixon, C.; Peim, M., Clausal temporal resolution, ACM Trans. Comput. Logic, 2, 12-56, (2001) · Zbl 1365.03017
[9] Gerth, R., Peled, D., Vardi, M., Wolper, P.: Simple on-the-fly automatic verification of linear temporal logic. In: In Protocol Specification Testing and Verification, pp. 3-18. Chapman & Hall, London (1995) · Zbl 1007.03014
[10] Hustadt, U., Konev, B.: Trp++ 2.0: a temporal resolution prover. In: CADE-19. LNCS, vol. 2741, pp. 274-278. Springer, Berlin (2003)
[11] Järvisalo, M., Biere, A., Heule, M.: Blocked clause elimination. In: TACAS. LNCS, vol. 6015, pp. 129-144. Springer, Berlin (2010) · Zbl 1284.03208
[12] Pill, I., Semprini, S., Cavada, R., Roveri, M., Bloem, R., Cimatti, A.: Formal analysis of hardware requirements. In: DAC ’06, pp. 821-826. ACM, New York (2006) · Zbl 1160.68401
[13] Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science, pp. 46-57. IEEE, Washington (1977) · Zbl 1007.03014
[14] Rozier, K., Vardi, M.: LTL satisfiability checking. In: 14th International SPIN Workshop. LNCS, vol. 4595, pp. 149-167. Springer, Berlin (2007) · Zbl 0632.68034
[15] Rozier, K., Vardi, M.: A multi-encoding approach for LTL symbolic satisfiability checking. In: FM. LNCS, vol. 6664, pp. 417-431. Springer, Berlin (2011)
[16] Schuppan, V., Darmawan, L.: Evaluating LTL satisfiability solvers. In: ATVA’11. LNCS, vol. 6996, pp. 397-413. Springer, Berlin (2011)
[17] Sistla, A.P.; Clarke, E.M., The complexity of propositional linear temporal logics, J. ACM, 32, 733-749, (1985) · Zbl 0632.68034
[18] Suda, M., Weidenbach, C.: Labelled superposition for PLTL. In: LPAR-18. LNCS, vol. 7180, pp. 391-405. Springer, Berlin (2012) · Zbl 1352.68164
[19] Suda, M., Weidenbach, C.: Labelled superposition for PLTL. Research Report MPI-I-2012-RG1-001, Max-Planck-Institut für Informatik, Saarbrücken (2012) · Zbl 1352.68164
[20] Suda, M., Weidenbach, C.: A PLTL-prover based on labelled superposition with partial model guidance. In: IJCAR. LNCS, vol. 7364, pp. 537-543. Springer, Berlin (2012) · Zbl 1358.68266
[21] Wolper, P., Temporal logic can be more expressive, Inf. Control, 56, 72-99, (1983) · Zbl 0534.03009
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.