Is there an algorithm on how to check if two LTL expressions (represented as binary trees) are semantically equivalent? Since there are many smaller equivalences such as $a\Rightarrow b \equiv \neg a \vee b$ or $F(a) \equiv true U a$ as well as commutativity, distributivity, etc. that need to be considered.
My initial idea was to create the truth table for both expressions and compare them. But then the temporal operators would not be taken into account. Creating and comparing the automaton for each expression sounds like it would be rather inefficient.

Is there a better way to do this?


1 Answer 1


Unfortunately, the approach of constructing automata for each formula and testing their equivalence is pretty much the best you can do.

The problem of checking whether an LTL formula is valid, that is, whether it is satisfied in every computation, is PSPACE complete (this is an easy exercise, given that LTL satisfiability is PSPACE complete).

Thus, checking whether two LTL formulas are equivalent is also at least PSPACE hard, since you can reduce from the former by testing equivalence with the formula "true".

In order to show membership in PSPACE, you can take the standard approach of checking equivalence of the corresponding automata "on the fly", without actually constructing them explicitly.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.