基于SAT的显式LTL推理
SAT-based Explicit LTL Reasoning
摘要：
我们提出了一个新的显式推理框架的线性时序逻辑（LTL），这是建立在命题可满足性（SAT）解决。作为这个框架的概念验证，我们描述了一个新的LTL可满足性工具，Aalta\_v2.0，这是建立在MiniSAT SAT求解器。我们测试这种方法的有效性，证明Aalta_v2.0显着优于所有现有的LTL可满足性求解器。此外，我们表明，该框架可以扩展到命题LTL断言LTL（我们允许理论原子），通过用Z3 SMT求解器替换MiniSAT，并证明这可以产生指数级的性能改善。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
