LTL Satisfiability Checking Revisited

We propose a novel algorithm for the satisfiability problem for Linear Temporal Logic (LTL). Existing approaches first transform the LTL formula into a B"uchi automaton and then perform an emptiness checking of the resulting automaton. Instead, our approach works on-the-fly by inspecting the formula directly, thus enabling finding a satisfying model quickly without constructing the full automaton. This makes our algorithm particularly fast for satisfiable formulas. We report on a prototype implementation, showing that our approach significantly outperforms state-of-the-art tools.

Authors

• Jianwen Li
• Lijun Zhang 0001
• Geguang Pu
• Moshe Y. Vardi
• Jifeng He 0001

Keywords

• Tagging
• Noise measurement
• Benchmark testing
• Model checking
• Automata
• Gold
• Mathematical model
• Linear Temporal Logic
• Satisfiability Checking
• Emptiness
• Obligations
• Connective
• Syntactic
• Reachable
• Explicit Model
• Normal Form
• Transit System
• Consistent Set
• Finite Sequence
• Infinite Sequence
• Semantic Equivalence
• Notion Of Set
• Obligation Set
• LTL satisfiability checking
• LTL Transition system