SAT for a LTL公式

Question

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

G (A => B) and (A =真) and (B =假)

如果你能指出一个可以处理这个问题的SAT求解器，那就太好了。

非常感谢!

Answer 1

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