Title

SAT-Based Explicit LTLf Satisfiability Checking

Campus Units

Aerospace Engineering, Computer Science, Electrical and Computer Engineering

Document Type

Conference Proceeding

Conference

Thirty-Third AAAI Conference on Artificial Intelligence (AAAI-19)

Publication Version

Accepted Manuscript

Link to Published Version

https://doi.org/10.1609/aaai.v33i01.33012946

Publication Date

7-17-2019

Journal or Book Title

Proceedings of the AAAI Conference on Artificial Intelligence

Volume

33

Issue

1

First Page

2946

Last Page

2953

DOI

10.1609/aaai.v33i01.33012946

Conference Title

Thirty-Third AAAI Conference on Artificial Intelligence (AAAI-19)

Conference Date

January 27-February 1, 2019

City

Honolulu, HI

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.

Copyright Owner

Association for the Advancement of Artificial Intelligence

Language

en

File Format

application/pdf

Published Version

Share

Article Location

 
COinS