<p>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.</p>

<p>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.</p>

<p>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.</p>

CC BY-SA 3.0
2012-06-29T15:39:45.303Z
what is AFPp ? When you say "In particular, for the path which always stays in the first state, this is true even though a ¬p-state is reachable.", this sounds like a contradiction to me without any further explanation!
dendini
CC BY-SA 3.0
2012-06-29T17:35:23.840Z
That was a typo - was supposed to be $AFGp$, thanks for catching it. As for the apparent contradiction: The point really is that for this formula, each path is checked individually for whether $FGp$ holds along it. That the $\neg p$-state is reachable from the first one is irrelevant for the path which does not in fact reach it.
Klaus Draeger
CC BY-SA 3.0
2012-06-29T11:16:04.083Z
2012-06-29T17:29:51.320Z
2012-06-29T17:29:51.320Z
Klaus Draeger
<p>Lets name the states $s_1,s_2,s_3$, from left to right.</p>

<p>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)$. </p>

<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)$. </p>

<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$. </p>

<p>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)$. </p>

<p>I hope this helps..</p>

CC BY-SA 3.0
2012-06-29T15:42:50.293Z
You jumped the part which interests me, that is AFG(p) looping on state s1, why don't I consider the fact that it can always in a future state jump to s2 while in CTL I condider that??... moreover you considered FG(p), shouldn't AF be one unbreakable construct and G(p) another one?
dendini
CC BY-SA 3.0
2012-06-29T16:31:03.483Z
AFGp is an LTL formula, which I find easier to understand. By definition, s1 satisfies AFGp iff all paths starting from s1 satisfy the path formula FGp. So that's what I showed in the answer - I went over all the options of paths starting from s1 and showed they satisfy FGp.
Guy
CC BY-SA 3.0
2012-06-29T16:35:21.357Z
Why doesn't this work for AFAGp: This is a CTL formula and formally it talks about trees. Intuitively, it means: all paths eventually reach a point from which all paths satisfy Gp. You can think of it as a tree: every branch in the tree corresponds to a computation of the Kripke struct. So every node in the tree is labeled with a subset of AP. The tree satisfies the formula iff every path from the root reaches a subtree in which every node has `p`.
Guy
CC BY-SA 3.0
2012-06-29T09:36:43.187Z
2012-06-29T09:36:43.187Z
Guy
<p>I have this Kripke model $M$:</p>

<p>$$
\begin{array}{ccccccc}
  \to &amp; (p, q) &amp; \to &amp; (\neg p, \neg q) &amp; \to &amp; (p, \neg q) \\
  &amp; \circlearrowright &amp; &amp; &amp; &amp; \circlearrowright &amp; \\
\end{array}
$$</p>

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

<p>Now I cannot wrap my mind as to why:</p>

<ul>
<li>$M \vDash \mathop{\mathbf{A}}\mathop{\mathbf{F}}\mathop{\mathbf{A}}\mathop{\mathbf{G}}p$ is false in CTL;</li>
<li>$M \vDash \mathop{\mathbf{A}}\mathop{\mathbf{F}}\mathop{\mathbf{G}}p$ is true in CTL<sup>*</sup>.</li>
</ul>

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

CC BY-SA 3.0
2012-06-29T15:30:22.557Z
AFAG is AF(AG(p)) where AF stand for All Finally and AG stands for All Globally, CTL* is a temporal language. If you don't understand the above I think you should first read a book on the subject.
dendini
CC BY-SA 3.0
2012-06-29T16:51:21.567Z
Welcome to cstheory, a Q&A site for *research-level* questions in *theoretical computer science* (TCS). Your question does not appear to be a research-level question in TCS. Please see the [FAQ] for more information on what is meant by this and suggestions for sites that might welcome your question. Finally, if your question is closed for being out of scope, and you believe you can edit the question to make it a research-level question, please feel free to do so. Closing is not permanent and questions can be reopened, check the [FAQ] for more information.
Kaveh
CC BY-SA 3.0
2012-06-30T00:53:51.603Z
@Kaveh Feel free to migrate to [cs.se]
Gilles 'SO- stop being evil'
<lo.logic><model-checking><temporal-logic>
Kripke model and LTL vs CTL formulae interpretation
dendini
# Kripke model and LTL vs CTL formulae interpretation

(Asked by: username_0 on 2012-06-29)

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.

**Tags:** lo.logic, model-checking, temporal-logic
> **Comments:**
> **username_0**: AFAG is AF(AG(p)) where AF stand for All Finally and AG stands for All Globally, CTL* is a temporal language. If you don't understand the above I think you should first read a book on the subject.  
> **username_1**: Welcome to cstheory, a Q&A site for *research-level* questions in *theoretical computer science* (TCS). Your question does not appear to be a research-level question in TCS. Please see the [FAQ] for more information on what is meant by this and suggestions for sites that might welcome your question. Finally, if your question is closed for being out of scope, and you believe you can edit the question to make it a research-level question, please feel free to do so. Closing is not permanent and questions can be reopened, check the [FAQ] for more information.  
> **username_2**: @Kaveh Feel free to migrate to [cs.se]  

---

## 2 answers

### Answer by username_3 on 2012-06-29. Score: 3 | Accepted answer

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.

> **Comments:**
> **username_0**: what is AFPp ? When you say "In particular, for the path which always stays in the first state, this is true even though a ¬p-state is reachable.", this sounds like a contradiction to me without any further explanation!  
> **username_3**: That was a typo - was supposed to be $AFGp$, thanks for catching it. As for the apparent contradiction: The point really is that for this formula, each path is checked individually for whether $FGp$ holds along it. That the $\neg p$-state is reachable from the first one is irrelevant for the path which does not in fact reach it.  

---

### Answer by username_4 on 2012-06-29. Score: 0

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..

> **Comments:**
> **username_0**: You jumped the part which interests me, that is AFG(p) looping on state s1, why don't I consider the fact that it can always in a future state jump to s2 while in CTL I condider that??... moreover you considered FG(p), shouldn't AF be one unbreakable construct and G(p) another one?  
> **username_4**: AFGp is an LTL formula, which I find easier to understand. By definition, s1 satisfies AFGp iff all paths starting from s1 satisfy the path formula FGp. So that's what I showed in the answer - I went over all the options of paths starting from s1 and showed they satisfy FGp.  
> **username_4**: Why doesn't this work for AFAGp: This is a CTL formula and formally it talks about trees. Intuitively, it means: all paths eventually reach a point from which all paths satisfy Gp. You can think of it as a tree: every branch in the tree corresponds to a computation of the Kripke struct. So every node in the tree is labeled with a subset of AP. The tree satisfies the formula iff every path from the root reaches a subtree in which every node has `p`.  

---

