What is the difference between LTL and CTL?

Question

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.

Answer 1

To really understand the difference between LTL and CTL you have to study semantics of both language. The 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" —, the satisfiability is checked on the run with no possibility of switching to another run during the checking. On the other hand, the 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 properties (an important reachability property for circuit design) states that there is always a possibility that a state can be reached during the run, even if it is never reach actually (AG EF reset). The LTL can only states that the reset state is actually reached and not that it can be reached. In the same time, the LTL formula $\Diamond\Box s$ cannot be translate in 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). The 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. Indeed, consider the system that loop on A1, can goes from A1 to B and then will goes to A2 on the next move. Then the system will go in A2 state forever. Then "the system will finally stayed 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 reply to your question, but I would like to add some comment.

There is a lot of discussion on the best logic to express property for software verification... but the real debate is somewhere else. The LTL can express an 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 differents approaches, until now.

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