|
===Logical operators===
The [[Logical connective|logical operators]] are the usual ones: <math>\neg¬,\∨,\∧,\Rightarrow</math>⇒ and <math>\Leftrightarrow</math>⇐. Along with these operators CTL formulas can also make use of the boolean constants [[Truth|true]] and [[False (logic)|false]].
===Temporal operators===
The temporal operators are the following:
* Quantifiers over paths
**'''A''' <math>\phi</math>''φ'' – '''A'''ll: <math>\phi</math>''φ'' has to hold on all paths starting from the current state.
**'''E''' <math>\phi</math>''φ'' – '''E'''xists: there exists at least one path starting from the current state where <math>\phi</math>''φ'' holds.
* Path-specific quantifiers
**'''X''' <math>\phi</math>''φ'' – Ne'''x'''t: <math>\phi</math>''φ'' has to hold at the next state (this operator is sometimes noted '''N''' instead of '''X''').
**'''G''' <math>\phi</math>''φ'' – '''G'''lobally: <math>\phi</math>''φ'' has to hold on the entire subsequent path.
**'''F''' <math>\phi</math>''φ'' – '''F'''inally: <math>\phi</math>''φ'' eventually has to hold (somewhere on the subsequent path).
**<math>\phi</math>''φ'' '''U''' <math>\psi</math>''ψ'' – '''U'''ntil: <math>\phi</math>''φ'' has to hold ''at least'' until at some position <math>\psi</math>''ψ'' holds. This implies that <math>\psi</math>''ψ'' will be verified in the future.
**<math>\phi</math>''φ'' '''W''' <math>\psi</math>''ψ'' – '''W'''eak until: <math>\phi</math>''φ'' has to hold until <math>\psi</math>''ψ'' holds. The difference with '''U''' is that there is no guarantee that <math>\psi</math>''ψ'' will ever be verified. The '''W''' operator is sometimes called "unless".
In [[CTL*]], the temporal operators can be freely mixed. In CTL, the operator must always be grouped in two: one path operator followed by a state operator. See the examples below. [[CTL*]] is strictly more expressive than CTL.
===Minimal set of operators===
In CTL there is a minimal set of operators. All CTL formulas can be transformed to use only those operators. This is useful in [[model checking]]. One minimal set of operators is: {true, <math>\∨, \neg</math>¬, '''EG''', '''EU''', '''EX'''}.
Some of the transformation used for temporal operator are:
*'''EF'''<math>\phi</math>''φ'' == '''E'''[true'''U'''(<math>\phi</math>''φ'')] ( because '''F'''<math>\phi</math>''φ'' == [true'''U'''(<math>\phi</math>''φ'')] )
*'''AX'''<math>\phi</math>''φ'' == <math>\neg</math>¬'''EX'''(<math>\neg</math><math>\phi</math>¬''φ'')
*'''AG'''<math>\phi</math>''φ'' == <math>\neg</math>¬'''EF'''(<math>\neg</math><math>\phi</math>¬''φ'') == <math>\neg</math>¬ '''E'''[true'''U'''(<math>\neg</math><math>\phi</math>¬''φ'')]
*'''AF'''<math>\phi</math>''φ'' == '''A'''[true'''U'''<math>\phi</math>''φ''] == <math>\neg</math>¬'''EG'''(<math>\neg</math><math>\phi</math>¬''φ'')
*'''A'''[<math>\phi</math>''φ'''''U'''<math>\psi</math>''ψ''] == <math>\neg</math>¬( '''E'''[(<math>\neg</math><math>\psi</math>¬''ψ'')'''U'''<math>\neg</math>¬(<math>\phi</math><math>\''φ''&or</math><math>\psi</math>;''ψ'')] <math>\&or</math>; '''EG'''(<math>\neg</math><math>\psi</math>¬''ψ'') )
<!---
*'''F''' <math>\phi</math>''φ'' = '''true''' '''U''' <math>\phi</math>''φ''
*'''G''' <math>\phi</math>''φ'' = <math>\neg</math>¬ '''F''' <math>\neg</math><math>\phi</math>¬''φ''
--->
| 