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?