Test two LTL expression trees for equivalence
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 &quot;true&quot;.
In order to show membership in PSPACE, you can take the standard approach of checking equivalence of the corresponding automata &quot;on the fly&quot;, without actually constructing them  explicitly.