2
$\begingroup$

I am trying to understand these subtle differences between LTL and CTL logic and one thing I simply don't have an idea how to understand.

Formula

AG AF p 

in CTL and a formula

GF p

in LTL. Why aren't they equivalent? Can you give me an example, please? I tried finding and drawing things, but I simply can't find a counter example and there is no explanation in the lecture materials I have.

$\endgroup$
  • $\begingroup$ 'darxsys' asked about AGAFp vs GFp, and Klaus responded about a different pair of formulae, AFAGp vs FGp. I'd appreciate someone answering the original question, about AGAFp vs GFp, because it's on my mind today, too. $\endgroup$ – user40446 Jun 16 '16 at 14:40
  • $\begingroup$ @RichardRaimi, the answer by Klaus Draeger clearly states that AG AF p is equivalent to G F p. $\endgroup$ – Radu GRIGore Jun 17 '16 at 4:26
8
$\begingroup$

There are already some rather good related answers regarding LTL versus CTL. In a nutshell, LTL is first and foremost a logic of traces, and an LTL formula is true for a transition system $S$ if and only if it is true for each trace of $S$. CTL, on the other hand, is a branching-time logic, which can in a sense talk about multiple paths at the same time.

One standard example here (not the one you give, about which more below) is a labelled transition system $S=(Q,T,q_0,L)$ with set of locations $Q=\{q_0,q_1,q_2\}$, set of transitions $T=\{(q_0,q_0),(q_0,q_1),(q_1,q_2),(q_2,q_2)\}$, and labelling given by $L(q_0)=L(q_2)=\{p\}$, $L(q_1)=\emptyset$. This system satisfies $FGp$, but not $AFAGp$, which can be seen as follows.

$FGp$ means that for every path $\pi=s_1,s_2,\dots$ in a given system, there is some point after which $p$ is always satisfied, i.e. there is some $i$ such that for all $j\geq i$, $p\in L(s_i)$. This is satisfied by $S$ since every path in $S$ either remains in $q_0$ forever (such that $p$ is always satisfied) or eventually gets to $p_2$ (after which $p$ is always satisfied).

On the other hand, $AFAGp$ means that every path $\pi=s_1,s_2,\dots$ eventually reaches a state satisfying $AGp$, i.e. a state such that on every path $\pi'$ starting there, $p$ is always satisfied. Formally, this means that there is an $i$ such that for all $\pi'=s_1',s_2',\dots$ with $s_1'=s_i$ and all $j$, we have $p\in L(s_j')$. But in $S$, for the path which always remains in $q_0$, the transition to $q_1$, where $p$ is not satisfied, is always available, so that at no point of that path $AGp$ holds; therefore $AFAGp$ is not satisfied by $S$.

As for your example, this is actually a case where two formulas are equivalent. This does happen. The proof is a little involved, but I can add it if you are interested.

$\endgroup$
  • $\begingroup$ Thanks for help, but how is then not possible to give fairness constraints in CTL with AG AF if GF is used in LTL to do the same? $\endgroup$ – darxsys Apr 1 '14 at 19:31
  • 1
    $\begingroup$ You can do that, if all you want to do is express that every path satisfies the (unconditional) fairness condition. What you usually want to express, though, is that all fair paths (or some fair path) satisfy some other formula, i.e. something like $A(fair\Rightarrow\varphi)$. This is not allowed in CTL - you cannot have boolean combinations of path formulas. The lecture slides at react.uni-saarland.de/teaching/verification-11-12/downloads/… have some more information that you may find helpful (including the fairness issue, on slides 17,18). $\endgroup$ – Klaus Draeger Apr 2 '14 at 13:41

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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