SAT-based explicit LTL_f satisfiability checking
From MaRDI portal
Publication:2046017
Abstract: We present here 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 approximate four-fold speedup compared to the second-best solver.
Recommendations
- \(\mathrm{LTL}_{f}\) satisfiability checking
- An explicit transition system construction approach to LTL satisfiability checking
- SAT-based explicit LTL reasoning and its application to satisfiability checking
- Accelerating LTL satisfiability checking by SAT solvers
- Constraint LTL satisfiability checking without automata
Cites work
- A counting semantics for monitoring LTL specifications over finite traces
- Automata-Theoretic Model Checking Revisited
- Boolean Abstraction for Temporal Logic Satisfiability
- Linear temporal logic symbolic model checking
- LTL on finite and process traces: complexity results and a practical reasoner
- Model Checking Software
- More scalable LTL model checking via discovering design-space dependencies \((D^3)\)
- Planning for temporally extended goals.
- Reasoning with temporal logic on truncated paths.
- SAT-Based Model Checking without Unrolling
- Specifying and computing preferred plans
- Theory and Applications of Satisfiability Testing
- Using temporal logics to express search control knowledge for planning
Cited in
(19)- An explicit transition system construction approach to LTL satisfiability checking
- SAT-based explicit LTL reasoning and its application to satisfiability checking
- Linear templates of ACTL formulas with an application to SAT-based verification
- scientific article; zbMATH DE number 6708298 (Why is no real title available?)
- SAT-Based Model Checking without Unrolling
- SAT-Based Model Checking
- scientific article; zbMATH DE number 5158957 (Why is no real title available?)
- Accelerating LTL satisfiability checking by SAT solvers
- Constraint LTL satisfiability checking without automata
- scientific article; zbMATH DE number 2086516 (Why is no real title available?)
- Enhancing unsatisfiable cores for LTL with information on temporal relevance
- \(\mathrm{LTL}_{f}\) satisfiability checking
- Satisfiability checking for mission-time LTL
- Reasoning About Regular Properties: A Comparative Study
- Early verification of legal compliance via bounded satisfiability checking
- SAT meets tableaux for linear temporal logic satisfiability
- Towards ILP-based \(\mathrm{LTL_f}\) passive learning
- Bounded satisfiability checking of \(\mathrm{FOL}^*\) formulas with aggregations
- Inconsistency measurement in \(\mathrm{LTL_f}\) based on minimal inconsistent sets and minimal correction sets
This page was built for publication: SAT-based explicit \(\mathsf{LTL}_f\) satisfiability checking
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2046017)
