CTL* - Syntax

Syntax

The language of well-formed CTL* formulae is generated by the following unambiguous (wrt bracketing) context-free grammar:

$\Phi::=\bot \mid \top \mid p \mid (\neg\Phi) \mid (\Phi\and\Phi) \mid (\Phi\or\Phi) \mid (\Phi\Rightarrow\Phi) \mid (\Phi\Leftrightarrow\Phi) \mid A\phi \mid E\phi$

$\phi::=\Phi \mid (\neg\phi) \mid (\phi\and\phi) \mid (\phi\or\phi) \mid (\phi\Rightarrow\phi) \mid (\phi\Leftrightarrow\phi) \mid X\phi \mid F\phi \mid G\phi \mid$

where ranges over a set of atomic formulas. Valid CTL*-formulae are built using the nonterminal . These formulae are called state formulae, while those created by the symbol are called path formulae. (The above grammar contains some redundancies; for example as well as implication and equivalence can be defined as just for Boolean algebras (or propositional logic) from negation and conjunction, and the temporal operators X and U are sufficient to define the other two.)

The operators basically are the same as in CTL. However, in CTL, every temporal operator has to be directly preceded by a quantifier, while in CTL* this is not required. The universal path quantifier may be defined in CTL* in the same way as for classical predicate calculus, although this in not possible in the CTL fragment.