Computational tree logic

From Freepedia

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 4 References

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*.

See also

• Linear temporal logic

References

• Emerson, E. A. and Halpern, J. Y. (1985). Decision procedures and expressiveness in the temporal logic of branching time. Journal of Computer and System Sciences 30 (1): 1-24.

• Clarke, E. M., Emerson, E. A., and Sistla, A. P. (1986). Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems 8 (2): 244-263.

• Emerson, E. A. (1990). "Temporal and modal logic". In J. van Leeuwen (ed.), Handbook of Theoretical Computer Science, vol. B, pp. 955-1072. MIT Press. ISBN 0262220393.