3
$\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.

Improve this question
$\endgroup$
2
  • $\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
    Commented Jun 16, 2016 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
    Commented Jun 17, 2016 at 4:26

1 Answer 1

Reset to default
9
$\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.

Improve this answer
$\endgroup$
2
  • $\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
    Commented Apr 1, 2014 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
    Commented Apr 2, 2014 at 13: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.