Computation tree logic: Difference between revisions

Revision as of 09:24, 28 May 2018

Revision as of 11:21, 11 October 2018

Line 8:

:<math>\begin{align}

\phi &::= \bot \mid \top \mid p \mid (\neg\phi) \mid (\phi\andland\phi) \mid (\phi\orlor\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

Line 15:

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, \andland, \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)''