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.

  • $\begingroup$ What are AFAG and AFG? $\:$ What is the * for? $\;\;$ $\endgroup$ – user6973 Jun 29 '12 at 8:54
  • $\begingroup$ 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. $\endgroup$ – dendini Jun 29 '12 at 15:30
  • 1
    $\begingroup$ 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. $\endgroup$ – Kaveh Jun 29 '12 at 16:51
  • $\begingroup$ @Kaveh Feel free to migrate to Computer Science $\endgroup$ – Gilles 'SO- stop being evil' Jun 30 '12 at 0:53

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.

| cite | improve this answer | |
  • $\begingroup$ 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! $\endgroup$ – dendini Jun 29 '12 at 15:39
  • $\begingroup$ 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. $\endgroup$ – Klaus Draeger Jun 29 '12 at 17:35

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

| cite | improve this answer | |
  • $\begingroup$ 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? $\endgroup$ – dendini Jun 29 '12 at 15:42
  • $\begingroup$ 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. $\endgroup$ – Guy Jun 29 '12 at 16:31
  • $\begingroup$ 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. $\endgroup$ – Guy Jun 29 '12 at 16:35

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