3
$\begingroup$

Both Logic in Computer Science (Huth and Ryan, 2004) and Branching vs. Linear Time: Final Showdown (Vardi, 2002), state something to this effect (paraphrased):

In LTL, X F p and F X p are equivalent, meaning "p is eventually true in some state that is not the current state". In CTL, AX AF p and AF AX p are not equivalent. AX AF p does mean the same as the above LTL formulas, but AF AX p means something different, which we leave as an exercise to the reader.

Both works emphasize that the meaning of AF AX p is something very strange.

From what I understand of CTL, AF AX p would mean "all paths from this state eventually reach a state where p is true in all next states", but that doesn't seem particularly strange. Am I correct in that understanding?

Improve this question
$\endgroup$

1 Answer 1

Reset to default
4
$\begingroup$

Your understanding of $AF AX p$ is correct (in my opinion). But whether it seems particularly strange or hard to understand is rather subjective. The argument you quote compares the expressiveness or usability of LTL and CTL, and tries to convince readers that LTL is easier to understand (especially for engineers in practice).

In my experience, it indeed takes more time for me to figure out and confirm the meaning of $AF\,AX\,p$ than that of $AX\,AF\,p$, which is in turn more than that of $X\,F\,p$ or $F\,X\,p$. By the way, if $AF\,AX\,p$ were easier to understand than the other three formulas, you would probably not bother asking for confirmations here.

Improve this answer
$\endgroup$
4
  • $\begingroup$ Is AF AX p equivalent to AF p? $\endgroup$
    – Lee Sleek
    Dec 9, 2016 at 17:02
  • $\begingroup$ @LeeSleek No, they are not equivalent. As you already know, $AF\,AX\,p$ requires "(a) state where $p$ is true in all next states". $\endgroup$
    – hengxin
    Dec 10, 2016 at 8:58
  • $\begingroup$ But if every path eventually reaches p, every path must have a state before that p from which all transitions reach p — hence AF AX p. $\endgroup$
    – Lee Sleek
    Dec 10, 2016 at 17:36
  • $\begingroup$ @LeeSleek "All paths reach $p$" (for $AF\,p$) does not imply that "all next states reach $p$" (for $AF\,AX\,p$). Maybe you can post another question if you are still confused. $\endgroup$
    – hengxin
    Dec 11, 2016 at 3:45

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.