SAT-based Explicit LTLf Satisfiability Checking
Date
Authors
Major Professor
Advisor
Committee Member
Journal Title
Journal ISSN
Volume Title
Publisher
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.
Series Number
Journal Issue
Is Version Of
Versions
Series
Academic or Administrative Unit
Type
Comments
This is a pre-print of the article Li, Jianwen, Kristin Y. Rozier, Geguang Pu, Yueling Zhang, and Moshe Y. Vardi. "SAT-based Explicit LTLf Satisfiability Checking." arXiv preprint arXiv:1811.03176 (2018). Posted with permission.