Kripke model and LTL vs CTL formulae interpretation [closed]

Question

I have this Kripke model $M$:

$$ \begin{array}{ccccccc} \to & (p, q) & \to & (\neg p, \neg q) & \to & (p, \neg q) \\ & \circlearrowright & & & & \circlearrowright & \\ \end{array} $$

where $(p, \neg q)$ means “$p$ and not $q$” and $\circlearrowright$ is a self loop.

Now I cannot wrap my mind as to why:

• $M \vDash \mathop{\mathbf{A}}\mathop{\mathbf{F}}\mathop{\mathbf{A}}\mathop{\mathbf{G}}p$ is false in CTL;
• $M \vDash \mathop{\mathbf{A}}\mathop{\mathbf{F}}\mathop{\mathbf{G}}p$ is true in CTL^*.

If you have a reasonable explanation for the above I might post a second analogous example which might disprove your intuition.

Answer 1

Intuitively, what happens here is that for $AFGp$, you check each individual path for whether after some point, $p$ will always be true - no matter what other choices are available in a given state.

In particular, for the path which always stays in the first state, this is true even though a $\neg p$-state is reachable. On all other paths it is true because they eventually reach the third state.

In the case of $AFAGp$, the second path quantifier "overwrites" the first in a sense: here you have to check whether for all paths, you eventually reach a state such that all paths from that state - not just the one you were originally following - always satisfy $p$. For the path staying in the first state, this is not true, because there is always a branch going to the second state.

Answer 2

Lets name the states $s_1,s_2,s_3$, from left to right.

First, we show why the first formula is false: In order to see this, we first need to check which states satisfy the sub-formula $AG(p)$.

$s_3$ satisfies $AG(p)$ because there is only one infinite computation starting from $s_3$ which is $s_3^\omega$. However, $s_1$ does not satisfy $AG(p)$ since there is a computation, namely $s_1 s_2 s_3^\omega$, starting from $s_1$ that does not satisfy $AG(p)$.

Next, we check if $s_1$ satisfies $AFAG(p)$. By the above, we need to check, informally, if $s_1$ satisfies $AF(s_3)$. Clearly, it doesn't because of the computation $s_1^\omega$.

Next, we show that the structure satisfies $AFG(p)$: The computations starting from $s_1$ have one of two formats: either $s_1^\omega$ or $s_1^* \cdot s_2 \cdot s_3^\omega$ (i.e., a finite prefix of $s_1$ and visit to $s_2$ and an infinite suffix of $s_3$). A computation of this form satisfies $FG(p)$, because it either ends in $s_3$ or $s_1$. Since these are all the computations starting from $s_1$ we have that $s_1$ satisfies $AFG(p)$.

I hope this helps..