0

SAT ソルバーは、命題式 F の充足可能性を証明します。しかし、LTL 式の充足可能性をテストするために SAT を使用することは可能ですか? たとえば、次の LTL 式が満たされないことを証明できますか?

G (A => B) および (A = 真) および (B = 偽)

これを処理できる SAT ソルバーを教えていただければ幸いです。

どうもありがとうございました！

4

1 に答える 1

-1

Because is possible to generate a buchi automata from an LTL formula if the automata is empty means that is not possible to satisfy the original formula.

于 2014-08-26T10:16:50.860 に答える