# 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: [itex]\neg,\or,\and,\rightarrow[itex] and [itex]\leftrightarrow[itex]. 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 [itex]\phi[itex] - Next: [itex]\phi[itex] has to hold at the next state (this operator is sometimes noted X instead of N).
• G [itex]\phi[itex] - Globally: [itex]\phi[itex] has to hold on the entire subsequent path.
• F [itex]\phi[itex] - Finally: [itex]\phi[itex] eventually has to hold (somewhere on the subsequent path).

Binary operators:

• [itex]\phi[itex] U [itex]\psi[itex] - Until: [itex]\phi[itex] has to hold until at some position [itex]\psi[itex] holds. This implies that [itex]\psi[itex] will be verified in the future.
• [itex]\phi[itex] W [itex]\psi[itex] - Weak until: [itex]\phi[itex] has to hold until [itex]\psi[itex] holds. The difference with U is that there is no guarantee that [itex]\psi[itex] will ever be verified. The W operator is sometimes called "unless".

#### Path operators

These operators "select" paths.

• A [itex]\phi[itex] - All: [itex]\phi[itex] has to hold on all paths starting from the current state.
• E [itex]\phi[itex] - Exists: there exists at least one path starting from the current state where [itex]\phi[itex] holds.

## Relations with other logics

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

• Art and Cultures
• Countries of the World (http://www.academickids.com/encyclopedia/index.php/Countries)
• Space and Astronomy