Content deleted Content added
m →Syntax of CTL: better spacing around the pipe |
Replace all "\begin{aligned}" with "\begin{align}" - see talk Talk:Acceleration (special relativity)#Parse error |
||
Line 7:
The [[Regular Language|language]] of [[well formed formula]]s for CTL is generated by the following [[Context-free grammar|grammar]]:
:<math>\begin{
\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\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{
where <math>p</math> ranges over a set of [[atomic formula]]s. It is not necessary to use all connectives – for example,
| |||