SAT для формулы LTL

Question

SAT-решатель доказывает выполнимость пропозициональной формулы F. Однако возможно ли использовать SAT для проверки выполнимости формулы LTL? Например, можем ли мы доказать, что следующая формула LTL неудовлетворительна?

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

Было бы замечательно, если бы вы могли указать на SAT-решатель, который может справиться с этим.

Большое спасибо!

Answer 1

Поскольку возможно генерировать автоматы Бучи из формулы LTL, если автоматы пусты, это означает, что невозможно удовлетворить исходную формулу.