What is the LTL formula equivalent for this?

Question

'$\phi$' holds at least as long as '$\psi$' does.

I came up with $\mathsf G\,(\phi\to\psi)$, where $\sf G$ indicates globally forever.

Answer 1

In my view, “$\phi$ holds at least as long as $\psi$ does” should mean the following.

For any moment $t_0$ when $\psi$ holds, $\phi$ must also hold.

So, the formula should be thus: $$\mathsf{G}(\psi\rightarrow\phi)$$