Voir la source de CTL*

=== Formules de chemin ===
On note <math>\pi\models\phi</math> lorsqu'un chemin <math>\pi = s_0 \to s_1 \to \cdots</math> d'une structure de Kripke satisfait une formule de chemin <math>\phi</math>. Notons également <math>\ \pi[n]</math> le sous-chemin <math>s_n \to s_{n+1} \to \cdots</math>. Cette relation de satisfaction est définie inductivement par les règles suivantes :

# <math>(\mathcal{M}, \pi) \models \Phi</math> si et seulement si <math>(\mathcal{M}, s_0) \models \Phi</math> ;
# <math>(\mathcal{M}, \pi) \models \neg\phi</math> si et seulement si<math>(\mathcal{M}, \pi) \not\models \phi</math> ;
# <math>(\mathcal{M}, \pi) \models \phi_1 \land \phi_2</math> si et seulement si <math>(\mathcal{M}, \pi) \models \phi_1 </math> et <math>(\mathcal{M}, \pi) \models \phi_2 </math> ;
# <math>( \mathcal{M}, \pi) \models X\phi</math> si et seulement si <math>(\mathcal{M}, \pi[1]) \models \phi</math> ;
# <math>(\mathcal{M}, \pi) \models (\phi_1U\phi_2)</math>si et seulement si <math>\exists n\geqslant 0</math> tel que <math>(\mathcal{M},\pi[n]) \models\phi_2 </math> et <math>\forall 0\leqslant k < n</math> on a <math>(\mathcal{M},\pi[k]) \models \phi_1</math>.