How to prove a LTL formula correct in a specific model?

Question

I have been learning Verification by model checking recently and I get the following question:

$Whether\ the\ LTL\ formula\ M, q_3\ \models (X\ \lnot a) \rightarrow (F\ G\ \lnot a)\ is\ established\ or\ not\ in\ this\ model\ M?$

And there is the description of the model. .

I think it is correct, because the next state of $q_3$ is $q_1$ or $q_2$ and the next state of $q_1$ is $q_2$. So I get an infinite loop about $q_2$, which satisfies $F\ G\ \lnot a$. But I only can give the thought of my prove in natural language not mathematical rigor way.

if not mind, could anyone tell me my thought is right or wrong and prove it in a mathematical rigor way?

Thanks in advances

Answer 1

Your intuition is correct.

Consider an arbitrary path starting from $q_3$: let it be $q_3\, q\, q'\, q'' \ldots$. We need to prove it satisfies $\varphi = (X\lnot a)\rightarrow (FG \lnot a)$.

We proceed by cases on the second state $q$ in the path. It can be one of $q_1,q_2,q_4$.

If $q=q_4$ then $X\lnot a$ is false in the path, hence $\varphi$ is true in the path.

If $q=q_1$ or $q_2$ then we must have $q'=q''=\cdots=q_2$. The whole path is of the form $q_3\, q\, q_2\, q_2\, q_2 \ldots$. This path makes $FG\lnot a$ true, since there exists a suffix (namely, $q_2\, q_2\, q_2 \ldots$) where $G\lnot a$ is true ($a$ is false in each state of the suffix). Hence, $\varphi$ is true in the path.

You could make this even more formal by explicitly referring to the definition of validity.