How can I decide manually whether two CTL formulae are equivalent?

Assume I have two formulae $\Phi$ and $\Psi$ (over the same set of atomic propositions $AP$) in CTL. We have that $\Phi \equiv \Psi$ iff $Sat_{TS}(\Phi) = Sat_{TS}(\Psi)$ for all transition systems $TS$ over $AP$.

Given that there are infinitely many transition systems, it's impossible to check them all. I thought about using PNF (Positive Normal Form, allowing negation only next to literals) because judging from its name it should give me the same formula for $\Phi$ as for $\Psi$ iff they are equivalent, but I'm not convinced this works in all cases (you could say, I'm not convinced PNF is actually a normal form).

For example, take $\forall \mathrm{O} \forall \lozenge \Phi_0 \stackrel{?}{\equiv} \forall \lozenge \forall \mathrm{O} \Phi_0$ (where $\mathrm{O}$ is the next operator and $\lozenge$ is the eventually operator). I'm looking for a way do do this by hand.

It seems to me that "$\Phi≡\Psi$" is equivalent to "Neither $(\Phi ∧ ¬\Psi)$ nor $(\Psi ∧ ¬\Phi)$ is satisfiable".

Therefore deciding equivalence is as difficult as deciding satisfiability, since "$\Phi$ satisfiable" is equivalent to "not ($¬\Phi≡\top$)".

In this article there is a mention of a an exponential procedure to decide satisfiability in CTL, so it should be enough to run the algorithm on the two formulas I wrote above.

PS: I am not at all an expert in this field, so please check what I wrote. If this makes sense, I will remove the various "seems" and "should".

StackExchange Computer Science Q#616, answer score: 6