have a common subset, which is a proper subset of both CTL and LTL. FG.P exists in LTL but not in CTL. AG(P⇒((EX.Q)∧(EX¬Q))) and AG.EF.P exist in CTL but not in LTL. Extensions CTL has been extended with second-order quantification and to quantified computational tree logic (QCTL). There are two semantics: the tree semantics. We label nodes of the computation tree. QCTL* = QCTL = MSO over trees. Model checking and satisfiability are tower complete. the structure semantics. We label states. QCTL* = QCTL = MSO over graphs. Model checking is PSPACE-complete but satisfiability is undecidable. A reduction from the model-checking problem of QCTL with the structure semantics, to TQBF (true quantified Boolean formulae) has been proposed, in order to take advantage of the QBF solvers. See also Probabilistic CTL Fair computational tree logic Linear temporal logic References External links Teaching slides of CTL Logic in computer science Temporal logic Automata (computation)