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

1 Operators

1.1 Logical operators
1.2 Temporal operators

1.2.1 State operators
1.2.2 Path operators

2 Relations with other logics

3 See also

Operators

Logical operators

The logical operators are the usual ones: $\neg,\or,\and,\rightarrow$ and $\leftrightarrow$ . 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 $φ$ - Next: $φ$ has to hold at the next state (this operator is sometimes noted X instead of N).
G $φ$ - Globally: $φ$ has to hold on the entire subsequent path.
F $φ$ - Finally: $φ$ eventually has to hold (somewhere on the subsequent path).

Binary operators:

$φ$ U $ψ$ - Until: $φ$ has to hold until at some position $ψ$ holds. This implies that $ψ$ will be verified in the future.
$φ$ W $ψ$ - Weak until: $φ$ has to hold until $ψ$ holds. The difference with U is that there is no guarantee that $ψ$ will ever be verified. The W operator is sometimes called "unless".

Path operators

These operators "select" paths.

A $φ$ - All: $φ$ has to hold on all paths starting from the current state.
E $φ$ - Exists: there exists at least one path starting from the current state where $φ$ holds.

Relations with other logics

Computational tree logic (CTL) is a subset of CTL*.