×

SAT-based explicit \(\mathsf{LTL}_f\) satisfiability checking. (English) Zbl 07382223

Summary: Linear Temporal Logic over finite traces \((\mathsf{LTL}_f)\) was proposed in 2013 and has attracted increasing interest around the AI community. Though the theoretic basis for \(\mathsf{LTL}_f\) has been thoroughly explored since that time, there are still few algorithmic tools that are able to provide an efficient reasoning strategy for \(\mathsf{LTL}_f\). In this paper, we present a SAT-based framework for \(\mathsf{LTL}_f\) satisfiability checking, which is the foundation of \(\mathsf{LTL}_f\) reasoning. We use propositional SAT-solving techniques to construct a transition system, which is an automata-style structure, for an input \(\mathsf{LTL}_f\) formula; satisfiability checking is then reduced to a path-search problem over this transition system. Based on this framework, we further present CDLSC (Conflict-Driven \(\mathsf{LTL}_f\) Satisfiability Checking), a novel algorithm (heuristic) that leverages information produced by propositional SAT solvers, utilizing both satisfiability and unsatisfiability results. More specifically, the satisfiable results of the SAT solver are used to create new states of the transition system and the unsatisfiable results to accelerate the path search over the system. We evaluate all 5 off-the-shelf \(\mathsf{LTL}_f\) satisfiability algorithms against our new approach CDLSC. Based on a comprehensive evaluation over 4 different \(\mathsf{LTL}_f\) benchmark suits with a total amount of 9317 formulas, our time-cost analysis shows that 1) CDLSC performs best on checking unsatisfiable formulas by achieving approximately a 4X time speedup, compared to the second-best solution (K-LIVE [1]); 2) Although no approaches dominate checking satisfiable formulas, CDLSC performs best on 2 of the total 4 tested satisfiable benchmark suits; and 3) CDLSC gains the best overall performance when considering both satisfiable and unsatisfiable instances.

MSC:

68Txx Artificial intelligence

Software:

MiniSat; PPlan; nuXmv
PDF BibTeX XML Cite
Full Text: DOI arXiv

References:

[1] Claessen, K.; Sörensson, N., A liveness checking algorithm that counts, (FMCAD (2012), IEEE), 52-59
[2] De Giacomo, G.; Vardi, M., Linear temporal logic and linear dynamic logic on finite traces, (IJCAI (2013), AAAI Press), 2000-2007
[3] Rozier, K., Linear temporal logic symbolic model checking, Comput. Sci. Rev., 5, 2, 163-203 (2011) · Zbl 1298.68176
[4] Vardi, M., Automata-theoretic model checking revisited, (VMCAI. VMCAI, LNCS, vol. 4349 (2007), Springer), 137-150 · Zbl 1132.68483
[5] Bartocci, E.; Bloem, R.; Nickovic, D.; Roeck, F., A counting semantics for monitoring LTL specifications over finite traces, (Chockler, H.; Weissenbacher, G., Computer Aided Verification (2018), Springer International Publishing: Springer International Publishing Cham), 547-564
[6] Eisner, C.; Fisman, D.; Havlicek, J.; Lustig, Y.; McIsaac, A.; Van Campenhout, D., Reasoning with temporal logic on truncated paths, (Proc. 15th Int’l Conf. on Computer Aided Verification. Proc. 15th Int’l Conf. on Computer Aided Verification, Lecture Notes in Computer Science, vol. 2725 (2003), Springer), 27-39 · Zbl 1278.68168
[7] Bacchus, F.; Kabanza, F., Planning for temporally extended goals, Ann. Math. Artif. Intell., 22, 5-27 (1998) · Zbl 1034.68549
[8] De Giacomo, G.; Vardi, M., Automata-theoretic approach to planning for temporally extended goals, (Proc. European Conf. on Planning. Proc. European Conf. on Planning, Lecture Notes in AI, vol. 1809 (1999), Springer), 226-238
[9] Calvanese, D.; De Giacomo, G.; Vardi, M., Reasoning about actions and planning in LTL action theories, (Principles of Knowledge Representation and Reasoning (2002), Morgan Kaufmann), 593-602
[10] Patrizi, F.; Lipoveztky, N.; De Giacomo, G.; Geffner, H., Computing infinite plans for LTL goals using a classical planner, (IJCAI (2011), AAAI Press), 2003-2008
[11] Camacho, A.; Baier, J.; Muise, C.; McIlraith, A., Bridging the gap between LTL synthesis and automated planning (2017), U. Toronto, Tech. rep.
[12] Bacchus, F.; Kabanza, F., Using temporal logic to express search control knowledge for planning, Artif. Intell., 116, 1-2, 123-191 (2000) · Zbl 0939.68827
[13] Gabaldon, A., Precondition control and the progression algorithm, (KR (2004), AAAI Press), 634-643
[14] Bienvenu, M.; Fritz, C.; McIlraith, S., Planning with qualitative temporal preferences, (KR. KR, Lake District, UK (2006)), 134-144
[15] Bienvenu, M.; Fritz, C.; McIlraith, S. A., Specifying and computing preferred plans, Artif. Intell., 175, 7C8, 1308-1345 (2011) · Zbl 1225.68241
[16] Sohrabi, S.; Baier, J. A.; McIlraith, S. A., Preferred explanations: theory and generation via planning, (AAAI (2011)), 261-267
[17] De Giacomo, G.; Masellis, R. D.; Montali, M., Reasoning on LTL on finite traces: insensitivity to infiniteness, (AAAI (2014)), 1027-1033
[18] Rozier, K.; Vardi, M., LTL satisfiability checking, (SPIN. SPIN, LNCS, vol. 4595 (2007), Springer), 149-167
[19] Rozier, K.; Vardi, M., A multi-encoding approach for LTL symbolic satisfiability checking, (Int’l Symp. on Formal Methods. Int’l Symp. on Formal Methods, LNCS, vol. 6664 (2011), Springer), 417-431
[20] Rozier, K.; Vardi, M., LTL satisfiability checking, Int. J. Softw. Tools Technol. Transf., 12, 2, 123-137 (2010)
[21] Li, J.; Zhang, L.; Pu, G.; Vardi, M. Y.; He, J., \( \text{LTL}_f\) satisfiability checking, (ECAI (2014)), 91-98
[22] Malik, S.; Zhang, L., Boolean satisfiability from theoretical hardness to practical success, Commun. ACM, 52, 8, 76-82 (2009)
[23] Cavada, R.; Cimatti, A.; Dorigatti, M.; Griggio, A.; Mariotti, A.; Micheli, A.; Mover, S.; Roveri, M.; Tonetta, S., The NuXMV symbolic model checker, (CAV (2014)), 334-342
[24] Vizel, Y.; Weissenbacher, G.; Malik, S., Boolean satisfiability solvers and their applications in model checking, Proc. IEEE, 103, 11, 2021-2035 (2015)
[25] Bradley, A., SAT-based model checking without unrolling, (Jhala, R.; Schmidt, D., Verification, Model Checking, and Abstract Interpretation. Verification, Model Checking, and Abstract Interpretation, LNCS, vol. 6538 (2011), Springer), 70-87 · Zbl 1317.68109
[26] Een, N.; Mishchenko, A.; Brayton, R., Efficient implementation of property directed reachability, (FMCAD (2011)), 125-134
[27] Li, J.; Zhu, S.; Pu, G.; Vardi, M., SAT-based explicit LTL reasoning, (HVC (2015), Springer), 209-224
[28] Biere, A.; Cimatti, A.; Clarke, E.; Zhu, Y., Symbolic model checking without BDDs, (Proc. 5th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems. Proc. 5th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science, vol. 1579 (1999), Springer)
[29] Fionda, V.; Greco, G., The complexity of LTL on finite traces: hard and easy fragments, (AAAI (2016), AAAI Press), 971-977
[30] Cimatti, A.; Roveri, M.; Schuppan, V.; Tonetta, S., Boolean abstraction for temporal logic satisfiability, (Proc. 15th Int’l Conf. on Computer Aided Verification. Proc. 15th Int’l Conf. on Computer Aided Verification, Lecture Notes in Computer Science, vol. 4590 (2007), Springer), 532-546 · Zbl 1135.68469
[31] Li, J.; Rozier, K. Y.; Pu, G.; Zhang, Y.; Vardi, M. Y., SAT-based explicit LTLf satisfiability checking, (AAAI Conference on Artificial Intelligence (2019), AAAI)
[32] Gerth, R.; Peled, D.; Vardi, M.; Wolper, P., Simple on-the-fly automatic verification of linear temporal logic, (Dembiski, P.; Sredniawa, M., Protocol Specification, Testing, and Verification (1995), Chapman & Hall), 3-18
[33] Eén, N.; Sörensson, N., An extensible SAT-solver, (SAT (2003)), 502-518 · Zbl 1204.68191
[34] Schuppan, V.; Darmawan, L., Evaluating LTL satisfiability solvers, (Proceedings of the 9th International Conference on Automated Technology for Verification and Analysis. Proceedings of the 9th International Conference on Automated Technology for Verification and Analysis, AVTA’11 (2011), Springer-Verlag), 397-413
[35] Dureja, R.; Rozier, K. Y., More scalable LTL model checking via discovering design-space dependencies \(( D^3)\), (Beyer, D.; Huisman, M., Tools and Algorithms for the Construction and Analysis of Systems (2018), Springer International Publishing: Springer International Publishing Cham), 309-327 · Zbl 1423.68279
[36] Fionda, V.; Greco, G., Ltl on finite and process traces: complexity results and a practical reasoner, J. Artif. Intell. Res., 63, 557-623 (2018) · Zbl 1451.68176
[37] Geldenhuys, J.; Hansen, H., Larger automata and less work for LTL model checking, (SPIN. SPIN, LNCS, vol. 3925 (2006), Springer), 53-70 · Zbl 1178.68343
[38] Prescher, J.; Di Ciccio, C.; Mendling, J., From declarative processes to imperative models, (SIMPDA, vol. 1293 (2014)), 162-173
[39] Li, J.; Zhang, L.; Pu, G.; Vardi, M.; He, J., LTL satisfiability checking revisited, (TIME (2013)), 91-98
[40] Di Ciccio, C.; Maggi, F.; Mendling, J., Efficient discovery of target-branched declare constraints, Inf. Syst., 56, C, 258-283 (2016)
[41] Ciccio, C. D.; Mecella, M., On the discovery of declarative control flows for artful processes, ACM Trans. Manag. Inf. Syst., 5, 4, 24:1-24:37 (2015)
[42] Bozzano, M.; Cimatti, A.; Fernandes Pires, A.; Jones, D.; Kimberly, G.; Petri, T.; Robinson, R.; Tonetta, S., Formal design and safety analysis of AIR6110 wheel brake system, (Kroening, D.; Păsăreanu, C. S., Computer Aided Verification (2015), Springer International Publishing: Springer International Publishing Cham), 518-535
[43] Gario, M.; Cimatti, A.; Mattarei, C.; Tonetta, S.; Rozier, K. Y., Model checking at scale: automated air traffic control design space exploration, (Chaudhuri, S.; Farzan, A., Computer Aided Verification (2016), Springer International Publishing: Springer International Publishing Cham), 3-22
[44] Li, J.; Dureja, R.; Pu, G.; Rozier, K. Y.; Vardi Simplecar, M. Y., An efficient bug-finding tool based on approximate reachability, (Chockler, H.; Weissenbacher, G., Computer Aided Verification (2018), Springer International Publishing: Springer International Publishing Cham), 37-44
[45] Li, J.; Zhu, S.; Zhang, Y.; Pu, G.; Vardi, M. Y., Safety model checking with complementary approximations, (ICCAD (2017))
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.