- Syntax. A quantifier in a CTL formula are in form of a path quantifier $A,E$ following by a state quantifier $F,X,G,U,W$. A quantifier in an LTL is a combination of state quantifiers.
- States and paths. A CTL formula $\phi$ is a state formula, meaning that the temporal operators are state-based in structure: the derivation of a given formula is per-state and depends on the derivation of subformulas for subsequent states. For example, computing the set of states satisfying $AG\ φ$ relies on computing the set of states satisfying $φ$.
In contrast, LTL formula $\psi$ is a path formula: the derivation of a given formula depends on the derivation of subformulas for suffixes of a path. - Entailments. We write $M,s \models \phi$ and $M,p \models \psi$ for state $s$ and path $p$. Given a set $I$ of the initial states of $M$, we shall write $M ⊨ φ$ if $M, s ⊨ φ$ for all $s ∈ I$, and write $M ⊨ ψ$ if $M, s ⊨ ψ$ for all paths starting from $I$.
- LTL and CTL are incomparable. The reset property $AG (EF\ φ)$ (i.e. there is always a possibility that $\phi$ could hold, though it may never hold) cannot be expressed in LTL. The stability property $FG\ φ$ cannot be expressed in CTL.
- Structure vs traces. CTL can characterize the structure while LTL only characterizes the traces. Consider the following two systems:
$A:$ $(s_1,s_2),\ (s_1,s_3),\ (s_2,s_4),\ (s_3,s_5),\ (s_4,s_1),\ (s_5,s_1)$
$B:$ $(s_1,s_2),\ (s_2,s_4),\ (s_2,s_5),\ (s_4,s_1),\ (s_5,s_1)$
where $L(s_1)=a,\ L(s_2)=L(s_3)=b,\ L(s_4)=c,\ L(s_5)=d$. Both systems have traces $(ab(c+d))^\omega$ and thus cannot be distinguished in LTL. On the other hand, $B$ is a model of $AG(b\Rightarrow EX\ c)$ while $A$ isn't. - There is a lot of discussion of the best logic to express properties for software verification. LTL can express important properties for software system modelling (e.g. fairness) when the CTL must have a new semantics to express them. But CTL algorithms are usually more efficient and can use BDD-based algorithms.
References
1. Making prophecies with decision predicates
2. Branching vs. Linear Time: Final Showdown
2. Branching vs. Linear Time: Final Showdown
