Test two LTL expression trees for equivalence

Question

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?

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.