SAT-based explicit LTL f satisfiability checking

Linear Temporal Logic over finite traces ( LTL f ) was proposed in 2013 and has attracted increasing interest around the AI community. Though the theoretic basis for LTL f has been thoroughly explored since that time, there are still few algorithmic tools that are able to provide an efficient reasoning strategy for LTL f. In this paper, we present a SAT-based framework for LTL f satisfiability checking, which is the foundation of LTL f reasoning. We use propositional SAT-solving techniques to construct a transition system, which is an automata-style structure, for an input LTL f 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 LTL f 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 LTL f satisfiability algorithms against our new approach CDLSC. Based on a comprehensive evaluation over 4 different LTL f 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.

Authors

• Jianwen Li
• Geguang Pu East China Normal University Shanghai Trusted Industrial Control Platform Co.,Ltd., China
• Yueling Zhang
• Moshe Y. Vardi
• Kristin Y. Rozier

Keywords

• LTL over finite traces
• Satisfiability checking
• SAT-based satisfiability checking
• Conflict-driven satisfiability checking