SAT-Based Explicit LTLf Satisfiability Checking

Thumbnail Image
Date
2019-07-17
Authors
Li, Jianwen
Rozier, Kristin
Pu, Geguang
Zhang, Yueling
Vardi, Moshe
Major Professor
Advisor
Committee Member
Journal Title
Journal ISSN
Volume Title
Publisher
Authors
Research Projects
Organizational Units
Organizational Unit
Organizational Unit
Organizational Unit
Journal Issue
Is Version Of
Versions
Series
Department
Aerospace EngineeringComputer ScienceElectrical and Computer Engineering
Abstract

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 approximate four-fold speed-up compared to the second-best solver.

Comments

This is a manuscript of a proceeding published as Li, Jianwen, Kristin Y. Rozier, Geguang Pu, Yueling Zhang, and Moshe Y. Vardi. "SAT-Based Explicit LTLf Satisfiability Checking." In Proceedings of the AAAI Conference on Artificial Intelligence 33, no. 1 (2019): 2946-2953. DOI: 10.1609/aaai.v33i01.33012946. Posted with permission.

Description
Keywords
Citation
DOI
Subject Categories
Copyright
Tue Jan 01 00:00:00 UTC 2019