How can I decide manually whether two CTL formulae are equivalent?
It seems to me that "$\Phi≡\Psi$" is equivalent to "Neither $(\Phi ∧ &#172;\Psi)$ nor $(\Psi ∧ &#172;\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".