optimization - LTL 公式的 SAT

Question

SAT 求解器证明命题公式 F 的可满足性。但是，是否可以使用 SAT 来测试 LTL 公式的可满足性？例如，我们能证明下面的 LTL 公式是不可满足的吗？

G (A => B) 和 (A = True) 和 (B = False)

如果您能指出可以处理此问题的 SAT 求解器，那就太好了。

非常感谢！

Answer 1

因为如果自动机为空意味着不可能满足原始公式，则可以从 LTL 公式生成 buchi 自动机。