Computational tree logic
|
|
Computational tree logic (CTL) is a temporal logic. It is often used to express properties of a system in the context of formal verification or model checking.
It uses atomic propositions as its building blocks to make statements about the states of a system. CTL then combines theses propositions into formulas using logical operators and temporal operators.
| Contents |
Operators
Logical operators
The logical operators are the usual ones: <math>\neg,\or,\and,\rightarrow<math> and <math>\leftrightarrow<math>. Along with these operators CTL formulas can also make use of the boolean constants true and false.
Temporal operators
The temporal operators are the following:
State operators
These operators "select" states.
Unary operators
- N <math>\phi<math> - Next: <math>\phi<math> has to hold at the next state (this operator is sometimes noted X instead of N).
- G <math>\phi<math> - Globally: <math>\phi<math> has to hold on the entire subsequent path.
- F <math>\phi<math> - Finally: <math>\phi<math> eventually has to hold (somewhere on the subsequent path).
Binary operators:
- <math>\phi<math> U <math>\psi<math> - Until: <math>\phi<math> has to hold 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> - Weak 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".
Path operators
These operators "select" paths.
- A <math>\phi<math> - All: <math>\phi<math> has to hold on all paths starting from the current state.
- E <math>\phi<math> - Exists: there exists at least one path starting from the current state where <math>\phi<math> holds.
Relations with other logics
Computational tree logic (CTL) is a subset of CTL*.