<p>If given one object (e.g. trace in case of LTL), you consider only <em>one</em> future for every point in time, in CTL you have a plethora of them.</p>

<p>In particular, <code>next</code> gives a unique action in LTL but (potentially) a whole set in CTL.</p>

CC BY-SA 3.0
2011-05-25T19:56:28.727Z
But you typically apply the LTL formula to all runs of the system, rather than just one, thus closing the gap between the one/many future issue. It would be more precise to say that LTL deals with linear-time, whereas CTL deals with branching time.
Dave Clarke
CC BY-SA 3.0
2011-05-25T21:47:59.840Z
Saying, in LTL you consider one future is like saying in CTL you consider one state. Satisfiability is defined this way. It's not about how many futures, but the structure of the future. In one it is a trace, in the other, a tree.
Vijay D
CC BY-SA 3.0
2011-05-26T05:17:50.497Z
@Vijay - indeed, the structure matters. E.g. you can't just take an LTL formula, transform it like FGp -> AF AG p and get an equivalent CTL formula (these two formulae are not equivalent; moreover FGp is not expressible in CTL and AF AG p is not expressible in LTL).
jkff
CC BY-SA 3.0
2011-05-26T05:57:14.627Z
I assumed the OP was familiar with the formal definition and asking for some kind of intuition, hence my try. Can this answer be salvaged by saying "one future per model"?
Raphael
CC BY-SA 3.0
2011-05-26T10:34:27.807Z
I cannot tell what the OP is familiar with. For example, is it clear to them what a model is in each case?
Vijay D
CC BY-SA 3.0
2011-06-03T12:27:08.413Z
After checking my intuition, I rephrased my answer to be more specific. I wanted to refer to one fixed object under consideration.
Raphael
CC BY-SA 3.0
2011-05-25T19:05:58.023Z
2011-06-03T12:25:59.893Z
2011-06-03T12:25:59.893Z
Raphael
<p>To really understand the difference between LTL and CTL you have to study the semantics of both languages. LTL formulae denote properties that will be interpreted on each execution of a program. For each possible execution (a run), which can be see as a sequence of events or states on a line — and this is why it is named "linear time" — satisfiability is checked on the run with no possibility of switching to another run during the checking. On the other hand, CTL semantics checks a formula on all possible runs and will try either all possible runs (<strong>A</strong> operator) or only one run (<strong>E</strong> operator) when facing a branch. </p>

<p>In practice this means that some formulae of each language cannot be stated in the other language. For example, the reset property (an important reachability property for circuit design) states that there is always a <em>possibility</em> that a state can be reached during a run, even if it is never actually reached (<em>AG EF reset</em>). LTL can only state that the <em>reset</em> state is actually reached and not that it can be reached. </p>

<p>On the other hand, the LTL formula $\Diamond\Box s$ cannot be translated into CTL. This formula denotes the property of stability : in each execution of the program, <em>s</em> will finally be true until the end of the program (or forever if the program <em>never</em> stops). CTL can only provide a formula that is too strict (<em>AF AG s</em>) or too permissive (<em>AF EG s</em>). The second one is clearly wrong. It is not so straightforward for the first. But <em>AF AG s</em> is erroneous. Consider a system that loops on <em>A1</em>, can go from <em>A1</em> to <em>B</em> and then will go to <em>A2</em> on the next move. Then the system will stay in <em>A2</em> state forever. Then "the system will finally stay in a <em>A</em> state" is a property of the type $\Diamond\Box s$. It is obvious that this property holds on the system. However, <em>AF AG s</em> cannot capture this property since the opposite is true : there is a run in which the system will always be in the state from which a run finally goes in a non <em>A</em> state.</p>

<p>I don't know if this answers to your question, but I would like to add some comments.</p>

<p>There is a lot of discussion of the best logic to express properties for software verification... but the real debate is somewhere else. LTL can express important properties for software system modelling (fairness) when the CTL must have a new semantics (a new satisfiability relation) to express them. But CTL algorithms are usually more efficient and can use BDD-based algorithms. So... there is no best solution. Only two different approaches, so far.</p>

<p>One of the commenters suggests Vardi's paper <a href="https://www.researchgate.net/profile/Moshe_Vardi/publication/225174169_Branching_vs_Linear_Time_Final_Showdown/links/0912f511f7ee781586000000.pdf" rel="noreferrer">"Branching versus Linear Time: Final Showdown"</a>.</p>

CC BY-SA 3.0
2011-06-20T08:03:35.400Z
see a discussion on LTL vs CTL by Vardi: "Branching vs. Linear Time: Final Showdown"
Guy
CC BY-SA 3.0
2011-06-21T22:45:55.503Z
thanks a bunch, that is exactly the kind of insight I was looking for!
Anonymous Coward
CC BY-SA 4.0
2024-10-14T08:00:02.383Z
I understand this is a very very old thread. But I have a question. In the example you gave, the system might always be in A1 states that means there is a path where it can reach a B state. But isn't it addressed with fairness? Or did CTL not have fairness constraints like LTL?
JackDaniels
CC BY-SA 4.0
2024-10-15T14:53:36.330Z
Your point is slightly out of the scope of the OP question. However, the fairness constraint is not inherent in the "usual" satisfiability of a CTL formula. As I mention, you can embedded a fairness constraint in a LTL formula (e.g., ◻◊B to ensure that a B will always finally be executed), but you cannot do it in CTL without changing the semantics.
Benoît Fraikin
CC BY-SA 3.0
2011-06-17T04:05:26.767Z
2018-01-12T09:22:29.857Z
2018-01-12T09:22:29.857Z
Benoît Fraikin
<p>I already read examples of formulas in CTL but not in LTL and vice-versa, but I'm having trouble gaining a mental grasp on LTL formulas and <em>really</em> what, at the heart, is the difference.</p>

CC BY-SA 3.0
2011-05-25T19:08:28.567Z
Loads of notes on the interwebs deal with this issue. Have googled for "the difference between LTL and CTL"?
Dave Clarke
CC BY-SA 3.0
2011-05-25T21:45:11.827Z
Try writing down simple formulae and evaluating their semantics on Kripke structures.
Vijay D
<lo.logic><model-checking><temporal-logic>
What is the difference between LTL and CTL?
Anonymous Coward
# What is the difference between LTL and CTL?

(Asked by: username_0 on 2011-05-25)

I already read examples of formulas in CTL but not in LTL and vice-versa, but I'm having trouble gaining a mental grasp on LTL formulas and *really* what, at the heart, is the difference.

**Tags:** lo.logic, model-checking, temporal-logic
> **Comments:**
> **username_1**: Loads of notes on the interwebs deal with this issue. Have googled for "the difference between LTL and CTL"?  
> **username_2**: Try writing down simple formulae and evaluating their semantics on Kripke structures.  

---

## 2 answers

### Answer by username_5 on 2011-06-17. Score: 23 | Accepted answer

To really understand the difference between LTL and CTL you have to study the semantics of both languages. LTL formulae denote properties that will be interpreted on each execution of a program. For each possible execution (a run), which can be see as a sequence of events or states on a line — and this is why it is named "linear time" — satisfiability is checked on the run with no possibility of switching to another run during the checking. On the other hand, CTL semantics checks a formula on all possible runs and will try either all possible runs (**A** operator) or only one run (**E** operator) when facing a branch.

In practice this means that some formulae of each language cannot be stated in the other language. For example, the reset property (an important reachability property for circuit design) states that there is always a *possibility* that a state can be reached during a run, even if it is never actually reached (*AG EF reset*). LTL can only state that the *reset* state is actually reached and not that it can be reached.

On the other hand, the LTL formula $\Diamond\Box s$ cannot be translated into CTL. This formula denotes the property of stability : in each execution of the program, *s* will finally be true until the end of the program (or forever if the program *never* stops). CTL can only provide a formula that is too strict (*AF AG s*) or too permissive (*AF EG s*). The second one is clearly wrong. It is not so straightforward for the first. But *AF AG s* is erroneous. Consider a system that loops on *A1*, can go from *A1* to *B* and then will go to *A2* on the next move. Then the system will stay in *A2* state forever. Then "the system will finally stay in a *A* state" is a property of the type $\Diamond\Box s$. It is obvious that this property holds on the system. However, *AF AG s* cannot capture this property since the opposite is true : there is a run in which the system will always be in the state from which a run finally goes in a non *A* state.

I don't know if this answers to your question, but I would like to add some comments.

There is a lot of discussion of the best logic to express properties for software verification... but the real debate is somewhere else. LTL can express important properties for software system modelling (fairness) when the CTL must have a new semantics (a new satisfiability relation) to express them. But CTL algorithms are usually more efficient and can use BDD-based algorithms. So... there is no best solution. Only two different approaches, so far.

One of the commenters suggests Vardi's paper ["Branching versus Linear Time: Final Showdown"](https://www.researchgate.net/profile/Moshe_Vardi/publication/225174169_Branching_vs_Linear_Time_Final_Showdown/links/0912f511f7ee781586000000.pdf).

> **Comments:**
> **username_6**: see a discussion on LTL vs CTL by Vardi: "Branching vs. Linear Time: Final Showdown"  
> **username_0**: thanks a bunch, that is exactly the kind of insight I was looking for!  
> **username_7**: I understand this is a very very old thread. But I have a question. In the example you gave, the system might always be in A1 states that means there is a path where it can reach a B state. But isn't it addressed with fairness? Or did CTL not have fairness constraints like LTL?  
> **username_5**: Your point is slightly out of the scope of the OP question. However, the fairness constraint is not inherent in the "usual" satisfiability of a CTL formula. As I mention, you can embedded a fairness constraint in a LTL formula (e.g., ◻◊B to ensure that a B will always finally be executed), but you cannot do it in CTL without changing the semantics.  

---

### Answer by username_3 on 2011-05-25. Score: 2

If given one object (e.g. trace in case of LTL), you consider only *one* future for every point in time, in CTL you have a plethora of them.

In particular, `next` gives a unique action in LTL but (potentially) a whole set in CTL.

> **Comments:**
> **username_1**: But you typically apply the LTL formula to all runs of the system, rather than just one, thus closing the gap between the one/many future issue. It would be more precise to say that LTL deals with linear-time, whereas CTL deals with branching time.  
> **username_2**: Saying, in LTL you consider one future is like saying in CTL you consider one state. Satisfiability is defined this way. It's not about how many futures, but the structure of the future. In one it is a trace, in the other, a tree.  
> **username_4**: @Vijay - indeed, the structure matters. E.g. you can't just take an LTL formula, transform it like FGp -> AF AG p and get an equivalent CTL formula (these two formulae are not equivalent; moreover FGp is not expressible in CTL and AF AG p is not expressible in LTL).  
> **username_3**: I assumed the OP was familiar with the formal definition and asking for some kind of intuition, hence my try. Can this answer be salvaged by saying "one future per model"?  
> **username_2**: I cannot tell what the OP is familiar with. For example, is it clear to them what a model is in each case?  
> **username_3**: After checking my intuition, I rephrased my answer to be more specific. I wanted to refer to one fixed object under consideration.  

---

