Computer Science Stack Exchange is a question and answer site for students, researchers and practitioners of computer science. It only takes a minute to sign up.
Sign up to join this community
I have got confused in undressing the informal definition of LTL below: $$G(\phi \Longrightarrow\psi)\Longrightarrow(G\phi \Longrightarrow G\psi)$$
You seem to be pretty confused, so let's sort some things out. First, it's "implies", not "replies". That is, the formula $\phi\implies \psi$ means that if $\phi$ holds, then $\psi$ holds.
To be more precise, the formula $\phi\implies \psi$ is true in one of two cases: either $\phi$ is false, in which case we say that the implication is vacuously true, or if both $\phi$ and $\psi$ are true.
Now, in LTL, the operator $G$ means that something holds in every position in the computation. Let's examine the two "sides" of your formula with respect to that.
The formula $G(\phi\implies \psi)$ means that in every point of the computation, the formula $\phi\implies \psi$ is true, in the form mentioned above.
The formula $G\phi\implies G\psi$ means, as above, that either $G\phi$ is false, or both $G\phi$ and $G\psi$ is true.
Now it is fairly easy to see why the formula you have is true: if $G(\phi\implies \psi)$ is true, then, if $G\phi$ is true, then $\phi$ is true in every position, but then according to the LHS we have that $\psi$ is also true in every position, so $G\phi\implies G\psi$ is true.
For your second question, an informal way to think about this (there are many others, probably) is this: if you require that whenever $\phi$ holds, then $\psi$ must also hold, then in particular, if $\phi$ is always true, then $\psi$ is also always true.
