SAT-based Explicit LTLf Satisfiability Checking

Thumbnail Image
Date
2020-08-18
Authors
Li, Jianwen
Pu, Geguang
Zhang, Yueling
Vardi, Moshe
Rozier, Kristin Yvonne
Major Professor
Advisor
Committee Member
Journal Title
Journal ISSN
Volume Title
Publisher
Authors
Person
Rozier, Kristin Yvonne
Associate Professor
Research Projects
Organizational Units
Organizational Unit
Organizational Unit
Organizational Unit
Organizational Unit
Organizational Unit
Mathematics
Welcome to the exciting world of mathematics at Iowa State University. From cracking codes to modeling the spread of diseases, our program offers something for everyone. With a wide range of courses and research opportunities, you will have the chance to delve deep into the world of mathematics and discover your own unique talents and interests. Whether you dream of working for a top tech company, teaching at a prestigious university, or pursuing cutting-edge research, join us and discover the limitless potential of mathematics at Iowa State University!
Journal Issue
Is Version Of
Versions
Series
Department
Aerospace EngineeringComputer ScienceVirtual Reality Applications CenterElectrical and Computer EngineeringMathematics
Abstract

Linear Temporal Logic over finite traces (LTLf ) was proposed in 2013 and has attracted increasing interest around the AI community. Though the theoretic basis for LTLf has been thoroughly explored since that time, there are still few algorithmic tools that are able to provide an efficient reasoning strategy for LTLf . In this paper, we present a SAT-based framework for LTLf satisfiability checking, which is the foundation of LTLf reasoning. We use propositional SAT-solving techniques to construct a transition system, which is an automata-style structure, for an input LTLf formula; satisfiability checking is then reduced to a path-search problem over this transition system. Based on this framework, we further present CDLSC (Conflict-Driven LTLf Satisfiability Checking), a novel algorithm (heuristic) that leverages information produced by propositional SAT solvers, utilizing both satisfiability and unsatisfiability results. More specifically, the satisfiable results of the SAT solver are used to create new states of the transition system and the unsatisfiable results to accelerate the path search over the system. We evaluate all 5 off-the-shelf LTLf satisfiability algorithms against our new approach CDLSC. Based on a comprehensive evaluation over 4 different LTLf benchmark suits with a total amount of 9317 formulas, our time-cost analysis shows that 1) CDLSC performs best on checking unsatisfiable formulas by achieving approximately a 4X time speedup, compared to the second-best solution (K-LIVE [1]); 2) Although no approaches dominate checking satisfiable formulas, CDLSC performs best on 2 of the total 4 tested satisfiable benchmark suits; and 3) CDLSC gains the best overall performance when considering both satisfiable and unsatisfiable instances.

Comments

This is a manuscript of an article published as Li, Jianwen, Geguang Pu, Yueling Zhang, Moshe Y. Vardi, and Kristin Y. Rozier. "SAT-based Explicit LTLf Satisfiability Checking." Artificial Intelligence (2020): 103369. DOI: 10.1016/j.artint.2020.103369. Posted with permission.

Description
Keywords
Citation
DOI
Copyright
Wed Jan 01 00:00:00 UTC 2020
Collections