2015/07/09 by Jianwen Li, Li, Jianwen, Shufang Zhu +6
Computer Science · #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #cs.LO
paper · pdf · doi:10.48550/arxiv.1507.02519
openalex publication_date 2015/07/09 · arxiv created 2015/12/04 · arxiv updated 2015/12/08 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
We present here a new explicit reasoning framework for linear temporal logic (LTL), which is built on top of propositional satisfiability (SAT) solving. As a proof-of-concept of this framework, we describe a new LTL satisfiability tool, Aalta_v2.0, which is built on top of the MiniSAT SAT solver. We test the effectiveness of this approach by demonnstrating that Aalta_v2.0 significantly outperforms all existing LTL satisfiability solvers. Furthermore, we show that the framework can be extended from propositional LTL to assertional LTL (where we allow theory atoms), by replacing MiniSAT with the Z3 SMT solver, and demonstrating that this can yield an exponential improvement in performance.