0
$\begingroup$

I have got confused in undressing the informal definition of LTL below: $$G(\phi \Longrightarrow\psi)\Longrightarrow(G\phi \Longrightarrow G\psi)$$

  1. in many literatures I have seen implies is said as replies like for LHS we can say Always/Globally $\psi$ replies to $\phi$. is it correct?
  2. Does the LHS implies the RHS if so what is the informal interpretation of the formula? (Alway $\psi$ replies to Always $\phi$) replies to (Always $\psi$ replies to $\phi$)
$\endgroup$
2
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.