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 .

Operators

Logical operators

The logical operators are the usual ones: and . 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

Linear temporal logic (LTL) is a subset of CTL*.

See also

• Linear temporal logic