CTL* is a superset of computational tree logic (CTL) and linear temporal logic (LTL). It freely combines path quantifiers and temporal operators. Like CTL, CTL* is a branching-time logic. The formal semantics of CTL* formulae are defined with respect to a given Kripke structure.
LTL had been proposed for the verification of computer programs, first by Amir Pnueli in 1977. Four years later in 1981 E. M. Clarke and E. A. Emerson invented CTL and CTL model checking. CTL* was defined by E. A. Emerson and Joseph Y. Halpern in 1983.[1]
CTL and LTL were developed independently before CTL*. Both sublogics have become standards in the model checking community, while CTL* is of practical importance because it provides an expressive testbed for representing and comparing these and other logics. This is surprising because the computational complexity of model checking in CTL* is not worse than that of LTL: they both lie in PSPACE.
The language of well-formed CTL* formulae is generated by the following unambiguous (with respect to bracketing) context-free grammar:
\Phi::=\bot\mid\top\midp\mid(\neg\Phi)\mid(\Phi\land\Phi)\mid(\Phi\lor\Phi)\mid(\Phi ⇒ \Phi)\mid(\Phi\Leftrightarrow\Phi)\midA\phi\midE\phi
\phi::=\Phi\mid(\neg\phi)\mid(\phi\land\phi)\mid(\phi\lor\phi)\mid(\phi ⇒ \phi)\mid(\phi\Leftrightarrow\phi)\midX\phi\midF\phi\midG\phi\mid[\phiU\phi]\mid[\phiR\phi]
where
p
\Phi
\phi
\Phi\lor\Phi
The operators basically are the same as in CTL. However, in CTL, every temporal operator (
X,F,G,U
A\phi=\negE\neg\phi
EX(p)\landAFG(p)
AFG(p)
EX(p)
AG(p)
Remark: When taking LTL as subset of CTL*, any LTL formula is implicitly prefixed with the universal path quantifier
A
The semantics of CTL* are defined with respect to some Kripke structure. As the names imply, state formulae are interpreted with respect to the states of this structure, while path formulae are interpreted over paths on it.
If a state
s
\Phi
s\models\Phi
((l{M},s)\models\top)\land((l{M},s)\not\models\bot)
((l{M},s)\modelsp)\Leftrightarrow(p\inL(s))
((l{M},s)\models\neg\Phi)\Leftrightarrow((l{M},s)\not\models\Phi)
((l{M},s)\models\Phi1\land\Phi2)\Leftrightarrow(((l{M},s)\models\Phi1)\land((l{M},s)\models\Phi2))
((l{M},s)\models\Phi1\lor\Phi2)\Leftrightarrow(((l{M},s)\models\Phi1)\lor((l{M},s)\models\Phi2))
((l{M},s)\models\Phi1 ⇒ \Phi2)\Leftrightarrow(((l{M},s)\not\models\Phi1)\lor((l{M},s)\models\Phi2))
((l{M},s)\models\Phi1\Leftrightarrow\Phi2)\Leftrightarrow((((l{M},s)\models\Phi1)\land((l{M},s)\models\Phi2))\lor(\neg((l{M},s)\models\Phi1)\land\neg((l{M},s)\models\Phi2)))
((l{M},s)\modelsA\phi)\Leftrightarrow(\pi\models\phi
\pi
s)
((l{M},s)\modelsE\phi)\Leftrightarrow(\pi\models\phi
\pi
s)
The satisfaction relation
\pi\models\phi
\phi
\pi=s0\tos1\to …
\pi[n]
sn\tosn+1\to …
(\pi\models\Phi)\Leftrightarrow((l{M},s0)\models\Phi)
(\pi\models\neg\phi)\Leftrightarrow(\pi\not\models\phi)
(\pi\models\phi1\land\phi2)\Leftrightarrow((\pi\models\phi1)\land(\pi\models\phi2))
(\pi\models\phi1\lor\phi2)\Leftrightarrow((\pi\models\phi1)\lor(\pi\models\phi2))
(\pi\models\phi1 ⇒ \phi2)\Leftrightarrow((\pi\not\models\phi1)\lor(\pi\models\phi2))
(\pi\models\phi1\Leftrightarrow\phi2)\Leftrightarrow(((\pi\models\phi1)\land(\pi\models\phi2))\lor(\neg(\pi\models\phi1)\land\neg(\pi\models\phi2)))
(\pi\modelsX\phi)\Leftrightarrow(\pi[1]\models\phi)
(\pi\modelsF\phi)\Leftrightarrow(\existsn\geqslant0:\pi[n]\models\phi)
(\pi\modelsG\phi)\Leftrightarrow(\foralln\geqslant0:\pi[n]\models\phi)
(\pi\models[\phi1U\phi2])\Leftrightarrow(\existsn\geqslant0:(\pi[n]\models\phi2\land\forall0\leqslantk<n:~\pi[k]\models\phi1))
CTL* model checking (of an input formula on a fixed model) is PSPACE-complete [2] and the satisfiability problem is 2EXPTIME-complete.[3]