Content deleted Content added
Citation bot (talk | contribs) m Alter: journal, isbn, template type, title. | You can use this bot yourself. Report bugs here. | User-activated. |
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
*'''EF'''''φ'' == '''E'''[true'''U'''(''φ'')] ( because '''F'''''φ'' == [true'''U'''(''φ'')] )
*'''AX'''''φ'' == ¬'''EX'''(¬''φ'')
| |||