Computation tree logic: Difference between revisions

Revision as of 07:53, 23 May 2020

Revision as of 18:04, 25 May 2020

Line 34:

===Logical operators===

The [[Logical connective|logical operators]] are the usual ones: ¬¬,∨,∧,⇒⇒ and ⇔. Along with these operators CTL formulas can also make use of the boolean constants [[Truth|true]] and [[False (logic)|false]].

===Temporal operators===

Line 51:

===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, ∨, ¬¬, '''EG''', '''EU''', '''EX'''}.

Some of the transformations used for temporal operators are:

*'''EF'''''φ'' == '''E'''[true'''U'''(''φ'')] ( because '''F'''''φ'' == [true'''U'''(''φ'')] )

*'''AX'''''φ'' == ¬¬'''EX'''(¬¬''φ'')

*'''AG'''''φ'' == ¬¬'''EF'''(¬¬''φ'') == ¬¬ '''E'''[true'''U'''(¬¬''φ'')]

*'''AF'''''φ'' == '''A'''[true'''U'''''φ''] == ¬¬'''EG'''(¬¬''φ'')

*'''A'''[''φ'''''U'''''ψ''] == ¬¬( '''E'''[(¬¬''ψ'')'''U'''¬¬(''φ''∨''ψ'')] ∨ '''EG'''(¬¬''ψ'') )

<!---

*'''F''' ''φ'' = '''true''' '''U''' ''φ''