Editing Computation tree logic (section)

== Syntax of CTL ==
The [[Regular Language|language]] of [[well-formed formula]]s for CTL is generated by the following [[Context-free grammar|grammar]]:

:<math>\begin{align}
\phi &::= \bot \mid \top \mid p \mid (\neg\phi) \mid (\phi\land\phi) \mid (\phi\lor\phi) \mid 
(\phi\Rightarrow\phi) \mid (\phi\Leftrightarrow\phi) \\
&\mid\quad \mbox{AX }\phi \mid \mbox{EX }\phi \mid \mbox{AF }\phi \mid \mbox{EF }\phi \mid \mbox{AG }\phi \mid \mbox{EG }\phi \mid 
\mbox{A }[\phi \mbox{ U } \phi] \mid \mbox{E }[\phi \mbox{ U } \phi]
\end{align}</math>

where <math>p</math> ranges over a set of [[atomic formula]]s. It is not necessary to use all connectives&nbsp;&ndash; for example,
<math>\{\neg, \land, \mbox{AX}, \mbox{AU}, \mbox{EU}\}</math> comprises a complete set of connectives, and the others can be defined using them.

*<math>\mbox{A}</math> means 'along All paths' ''(inevitably)''
*<math>\mbox{E}</math> means 'along at least (there Exists) one path' ''(possibly)''

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

:<math>\mbox{EF }(\mbox{EG } p \Rightarrow \mbox{AF } r)</math>

The following is not a well-formed CTL formula:

:<math>\mbox{EF }\big(r \mbox{ U } q\big)</math>

The problem with this string is that <math>\mathrm U</math> can occur only when paired with an <math>\mathrm A</math> or an <math>\mathrm E</math>. <!-- TODO: explain it is evaluated over multiple paths /// here is a copy-paste from the LTL page: build up from proposition variables p1,p2,..., LTL formulas are generally evaluated over paths and a position on that path. A LTL formula as such is satisfied if and only if it is satisfied for position 0 on that path. -->

CTL uses [[First-order logic#Vocabulary|atomic propositions]] as its building blocks to make statements about the states of a system. <!-- TODO: give an example of an atomic proposition. --> These propositions are then combined into formulas using [[logical operator]]s and [[temporal logic|temporal operator]]s.