# What does "AF AX p" mean in CTL?

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?

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.
• @LeeSleek No, they are not equivalent. As you already know, $AF\,AX\,p$ requires "(a) state where $p$ is true in all next states". Dec 10 '16 at 8:58
• @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. Dec 11 '16 at 3:45