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?


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

  • $\begingroup$ $AF(p \land AF(q \land AF AG(-p)))$ $\endgroup$
    – Iwan5050
    Dec 12, 2021 at 8:58
  • $\begingroup$ The problem is I dont know how to express "in the future" because I only have aviable $A$ and $E$ $\endgroup$
    – Iwan5050
    Dec 12, 2021 at 9:12
  • $\begingroup$ I always feel bad if dont get the hints people give me sorry xD. Im going to try it again. I already knew what that meant, there are even more great combinations :) $\endgroup$
    – Iwan5050
    Dec 12, 2021 at 10:26
  • $\begingroup$ Im just thinking about how to state for all path excluded the path i've already been $\endgroup$
    – Iwan5050
    Dec 12, 2021 at 10:27
  • $\begingroup$ I think I see. Due to the stacked and we find automatically the structure of a series. $\endgroup$
    – Iwan5050
    Dec 12, 2021 at 10:41

Your Answer

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

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