Yes, you can use an LTL-to-Buchi-automaton translator for this.
Let's assume that you want to check if $\psi \rightarrow \psi'$ is a valid LTL formula, i.e., every word satisfying the LTL property $\psi$ also satisfies the LTL property $\psi'$. This case is equivalent to finding out if $\psi \wedge \neg \psi'$ is satisfiable. Your $\psi \models \psi'$ notation is another way of writing this, but I would avoid it, since the $\models$ relation is often defined differently in current research papers on the topic.
If we translate $\psi \wedge \neg \psi'$ to a Buchi automaton, we can easily check if its language is empty. In fact, optimizing LTL-to-Buchi translators remove states with an empty language, and hence you only need to check if the resulting automaton has no accepting state.
On example LTL-to-Buchi translator is ltl3ba. For instance, if you want to check if $\mathsf{F G }\,a$ implies $\mathsf{G F}\,a$, you can do that as follows:
./ltl3ba -f "(F G a) && !(G F a)"
Here, "-f" stands for "translate this formula that is given as a parameter".
The result is given in SPIN never claim form:
never { /* (F G a) && !(G F a) */
T0_init:
false;
}
There is no state ending with "_accept" in the name (or any transition), so $(\mathsf{F G }\,a) \wedge \neg (\mathsf{G F}\,a)$ is not satisfiable.
There is also at least one LTL-to-Buchi translator with a web interface, namely the one from the SPOT framework.