Computation Tree Logic - Syntax of CTL

Syntax of CTL

The language of well formed formulas for CTL is generated by the following grammar:

$\phi::=\bot |\top |p|(\neg\phi)|(\phi\and\phi)|(\phi\or\phi)| (\phi\Rightarrow\phi)|(\phi\Leftrightarrow\phi)|\mbox{AX }\phi|\mbox{EX }\phi|\mbox{AF }\phi|\mbox{EF }\phi|\mbox{AG }\phi|\mbox{EG }\phi| \mbox{A }|\mbox{E }$

where ranges over a set of atomic formulas. Not all of these connectives are needed – for example, comprises a complete set of connectives, and the others can be defined using them.

means 'along All paths' (Inevitably)
means 'along at least (there Exists) one path' (possibly)

For example, the following is a well-formed CTL formula:

The following is not a well-formed CTL formula:

The problem with this string is that can occur only when paired with an or an . It uses atomic propositions as its building blocks to make statements about the states of a system. CTL then combines these propositions into formulas using logical operators and temporal logics.

Read more about this topic: Computation Tree Logic