CTL trouble translating text into formula

Question

I have an excercise where I have to translate verbally formulated statements into CTL formulas. I have particularly trouble with this one:

On every path q is true at least once and p was true sometime before, after no longer. My attempt is the following: $AF q \land (EF p) AU q$

This is obvously wrong. The first part is easy, then the second is more difficult. What I've stated there implies that there exists a path to $p$ before $q$ but not that $p$ was true on the previous path, and the third part to me looks impossible. Can anyone help?

Answer 1

$\newcommand{AF}{\text{AF}\;}\newcommand{AG}{\text{AG}\;}$Try to decode this:

For each path:

• In the future: p and
  • In the future q and
    • Always in the future not p

---

You correctly concluded that the correct formula is

$$ \AF \left( p \land \AF \left( q \land \AG \neg p \right) \right).$$

The key thing to understand about CTL is that when you evaluate things like $\AF (p \land \AF q)$ then this is true if somewhere in the future $p \land \AF q$ is true, which means that $\AF q$ is evaluated in the state where $p$ is true.