Content deleted Content added
Singular to plural |
Singular to plural |
||
Line 53:
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, ∨, ¬, '''EG''', '''EU''', '''EX'''}.
Some of the transformations used for temporal
*'''EF'''''φ'' == '''E'''[true'''U'''(''φ'')] ( because '''F'''''φ'' == [true'''U'''(''φ'')] )
*'''AX'''''φ'' == ¬'''EX'''(¬''φ'')
| |||