publication . Article . Preprint . 2019

SAT-based Explicit LTLf Satisfiability Checking

Jianwen Li; Geguang Pu; Yueling Zhang; Moshe Y. Vardi; Kristin Y. Rozier;
Open Access
  • Published: 17 Jul 2019 Journal: Artificial Intelligence, volume 289, page 103,369 (issn: 0004-3702, Copyright policy)
  • Publisher: Elsevier BV
Abstract
<jats:p>We present a SAT-based framework for LTLf (Linear Temporal Logic on Finite Traces) satisfiability checking. We use propositional SAT-solving techniques to construct a transition system for the input LTLf formula; satisfiability checking is then reduced to a path-search problem over this transition system. Furthermore, we introduce CDLSC (Conflict-Driven LTLf Satisfiability Checking), a novel algorithm that leverages information produced by propositional SAT solvers from both satisfiability and unsatisfiability results. Experimental evaluations show that CDLSC outperforms all other existing approaches for LTLf satisfiability checking, by demonstrating an ...
Subjects
arXiv: Computer Science::Logic in Computer Science
ACM Computing Classification System: TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES
free text keywords: Linguistics and Language, Artificial Intelligence, Language and Linguistics, Computer Science - Logic in Computer Science
Related Organizations
42 references, page 1 of 3

[Bacchus and Kabanza 1998] F. Bacchus and F. Kabanza. Planning for temporally extended goals. Ann. of Mathematics and Artificial Intelligence, 22:5-27, 1998.

[Bacchus and Kabanza 2000] F. Bacchus and F. Kabanza. Using temporal logic to express search control knowledge for planning. [OpenAIRE]

Artificial Intelligence, 116(1-2):123-191, 2000.

[Bienvenu et al. 2011] M. Bienvenu, C. Fritz, and S. A. McIlraith.

Specifying and computing preferred plans. Artificial Intelligence, 175(7 Aˆ¨C8):1308 - 1345, 2011.

[Biere et al. 1999] A. Biere, A. Cimatti, E.M. Clarke, and Y. Zhu.

Symbolic model checking without BDDs. In Proc. 5th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, volume 1579 of Lecture Notes in Computer Science. Springer, 1999.

[Bradley 2011] A. Bradley. SAT-based model checking without unrolling. In Ranjit Jhala and David Schmidt, editors, Verification, Model Checking, and Abstract Interpretation, volume 6538 of LNCS, pages 70-87. Springer, 2011.

[Calvanese et al. 2002] D. Calvanese, G. De Giacomo, and M.Y.

Vardi. Reasoning about actions and planning in LTL action theories. In Principles of Knowledge Representation and Reasoning, pages 593-602. Morgan Kaufmann, 2002.

[Camacho et al. 2017] A. Camacho, J.A. Baier, C. Muise, and A.S. [OpenAIRE]

McIlraith. Bridging the gap between LTL synthesis and automated planning. Technical report, U. Toronto, 2017.

[Cavada et al. 2014] R. Cavada, A. Cimatti, M. Dorigatti, A. Griggio, A. Mariotti, A. Micheli, S. Mover, M. Roveri, and S. Tonetta.

The NuXMV symbolic model checker. In CAV, pages 334-342, 2014.

[Claessen and So¨rensson 2012] K. Claessen and N. So¨rensson. A liveness checking algorithm that counts. In FMCAD, pages 52-59.

42 references, page 1 of 3
Abstract
<jats:p>We present a SAT-based framework for LTLf (Linear Temporal Logic on Finite Traces) satisfiability checking. We use propositional SAT-solving techniques to construct a transition system for the input LTLf formula; satisfiability checking is then reduced to a path-search problem over this transition system. Furthermore, we introduce CDLSC (Conflict-Driven LTLf Satisfiability Checking), a novel algorithm that leverages information produced by propositional SAT solvers from both satisfiability and unsatisfiability results. Experimental evaluations show that CDLSC outperforms all other existing approaches for LTLf satisfiability checking, by demonstrating an ...
Subjects
arXiv: Computer Science::Logic in Computer Science
ACM Computing Classification System: TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES
free text keywords: Linguistics and Language, Artificial Intelligence, Language and Linguistics, Computer Science - Logic in Computer Science
Related Organizations
42 references, page 1 of 3

[Bacchus and Kabanza 1998] F. Bacchus and F. Kabanza. Planning for temporally extended goals. Ann. of Mathematics and Artificial Intelligence, 22:5-27, 1998.

[Bacchus and Kabanza 2000] F. Bacchus and F. Kabanza. Using temporal logic to express search control knowledge for planning. [OpenAIRE]

Artificial Intelligence, 116(1-2):123-191, 2000.

[Bienvenu et al. 2011] M. Bienvenu, C. Fritz, and S. A. McIlraith.

Specifying and computing preferred plans. Artificial Intelligence, 175(7 Aˆ¨C8):1308 - 1345, 2011.

[Biere et al. 1999] A. Biere, A. Cimatti, E.M. Clarke, and Y. Zhu.

Symbolic model checking without BDDs. In Proc. 5th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, volume 1579 of Lecture Notes in Computer Science. Springer, 1999.

[Bradley 2011] A. Bradley. SAT-based model checking without unrolling. In Ranjit Jhala and David Schmidt, editors, Verification, Model Checking, and Abstract Interpretation, volume 6538 of LNCS, pages 70-87. Springer, 2011.

[Calvanese et al. 2002] D. Calvanese, G. De Giacomo, and M.Y.

Vardi. Reasoning about actions and planning in LTL action theories. In Principles of Knowledge Representation and Reasoning, pages 593-602. Morgan Kaufmann, 2002.

[Camacho et al. 2017] A. Camacho, J.A. Baier, C. Muise, and A.S. [OpenAIRE]

McIlraith. Bridging the gap between LTL synthesis and automated planning. Technical report, U. Toronto, 2017.

[Cavada et al. 2014] R. Cavada, A. Cimatti, M. Dorigatti, A. Griggio, A. Mariotti, A. Micheli, S. Mover, M. Roveri, and S. Tonetta.

The NuXMV symbolic model checker. In CAV, pages 334-342, 2014.

[Claessen and So¨rensson 2012] K. Claessen and N. So¨rensson. A liveness checking algorithm that counts. In FMCAD, pages 52-59.

42 references, page 1 of 3
Powered by OpenAIRE Research Graph
Any information missing or wrong?Report an Issue