CTL: Are AGEF$\phi$ and AF$\phi$ Equivalent?

Question

I'm was studying CTL when I realized that it is quite difficult (at least for me) to separate when to use $AG\ EF\phi$ and when to use $AF\phi$.

I read $AG\ EF\phi$ (starting at some $s_0$) as:

For all states reachable from the initial state ($AG$), there exists some state that is possible to reach ($EF$) where $\phi$ holds.

I read $AF\phi$ as:

All paths reachable from the initial state contain some state where $\phi$ holds.

I have the same problem with other types of compositions as well, where I tend to think of $AG$ and $EF$ as "pure", and create compositions of them instead of using AF and EG. Could someone explain whether the two example formulas are equivalent and explain why/why not? It would really help me in realizing when to use compositions and when to use "just one".

Thanks!

PS. I can't tag it with CTL/Temporal Logic :(

Answer 1

I believe I have found an answer. I will post it here, and hopefully this will be of any use in the future.

After some analysis, here are my conclusions:

• $AGEF\phi$ says that all states along all paths are able to reach some future state where $\phi$ holds.
• $AF\phi$ says that all paths will reach some future state where $\phi$ holds.

So the first one does not necessarily have to ever enter a state where $\phi$ holds. Even if we wait infinitely long, we can always chose to not take the branch that leads to the future state where $\phi$ holds, creating a path that never reaches the future state but is always able to.

On the other hand, the second one will always reach the future state where $\phi$ holds, no matter which path we choose. If we wait infinitely long for that future state, eventually we will get to it.

So they are not equivalent.

Hope this helps anyone :)

Answer 2

As I slightly disagree with @Simon Sirak 's explanation, let me add another answer (unfortunately, my reputation is yet too low for a comment on the math part of StackExchange). For readability in the following I will abbreviate reaching a state fulfilling $\phi$ by reaching $\phi$.

• $AG EF \phi$: As Simon says, in all states of your system, $\phi$ can be reached. Or, more closely aligned with the meaning of the symbols, in all branches leaving the current state it always (in each state of the respective branch) holds that there exists at least one branch where $\phi$ can eventually be reached.
• $AF \phi$: On all branches leaving the current state $\phi$ can be eventually reached.

With just these formulas given, the current state they refer to would be the starting state (or root of the associated computation tree). Consider the following computation trees (sorry, again my reputation is too low to include the images in the answer).

• Computation tree fulfilling AF(phi)
• Computation tree fulfilling AGEF(phi)

The first tree fulfills $AF \phi$ as on each branch of the root $\phi$ can be reached. Even in presence of the infinite loop between $b$ and $\phi$ the property holds.

Now $AGEF \phi$ would require that on each state you could finally reach $\phi$. Again, this holds on the infinite branch. But clearly not for the states $a$, $d$, $c$, and $e$.

The second tree fulfills the property $AGEF \phi$.

Edit: Thinking about the differences between $AGEF \phi$ and $AGAF \phi$, I realized that the following tree does fulfill the first but not the latter.

• Computation tree fulfilling AGEF(phi) but not AGAF(phi)