• It's classical that LTL and CTL have different power. Here, I write down the example that shows how.
• First, let's recall what LTL and CTL can talk about.
• Call a system as a finite transition system, so we have states, transitions, and predicates over states.
• Both LTL and CTL formulae can talk about boolean combinations of atomic predicates, along with box and diamond modalities.
• LTL can talk about traces . A system satisfies an LTL formula iff every trace satisfies the formula. So, truth in LTL depends on the set of traces. Truth is defined on a (trace, index) pair. The toplevel truth is given by starting at index 0 and stepping forward.
• CTL can talk about states , and in CTL, we talk about branching that happens at a state. In CTL, every □ or ◇ is with a quantifier, ∀ or ∃.
• For example, ∀□p means: for all paths from the current state, for all states , the predicate p holds.
• For example, ∃□p means: for some path from the current state, for some state , the predicate p holds.
• For example, ∀◇p means: for all paths from the current state, for all states , the predicate p holds.

§ CTL but not LTL

CTL can say "reset is always possible". That is, ∀□(E◇ reset). This says that for all paths from a given state, it is always the case that there exists a path to a state where reset holds.

However, LTL cannot express this, since LTL can only reason about the current trace. The way to show this is to create two machines T and F ( T where the reset predicate is true, F where the reset predicate is false), but whose set of traces is the same.

§ LTL but not CTL

This is more counterintuitive: How can it be that something that can talk about branching cannot capture something that LTL can? Consider the LTL formula ◇□p. This says that p eventually stabilizes. This is clearly an LTL formula.

Let's to write it in CTL. Intuitively, we want to say that there exists a path, along with p always happens. So we may try ∃◇?m where ?m is something we ned to fill. Clearly, this starts with the right shape, wher we're saying that 'for some state along some path...'. Then, we can say ∃□p, which is