User:PhS/CTL

This is my draft for a CTL article -- PhS 21:58, 13 February 2006 (UTC)

CTL, the Computation tree logic, is a temporal logic used in computer science. It arose in the 1980s as a convenient formalism for stating and checking behavioral properties of systems and played in a key rôle in the early development of model checking. Nowadays, the widespread use of powerful symbolic CTL-based model checkers makes it one of the most famous temporal logics.

CTL can express statements about the correctness of a system's behavior, like for example "pressing a stop button is always eventually followed by the system shutting down but not before the engine halts". It is then possible to check automatically whether such statements are satisfied by a given actual system model, a procedure called model checking.

The popularity of CTL comes from the good compromise it offers between, on the one hand, its simplicity and expressive power, and on the other hand, the existence of simple and efficient model-checking methods for CTL statements.

CTL formulae and their meaning

CTL views the behavior of a nondeterministic system as a set of runs, or computations, arranged in a branching tree of configurations. Times progresses when one moves along a run, from past configurations to future ones.

Simple CTL modalities

A CTL formula states a property of some current configuration. This property can refer to properties at other configurations that may happen in the future.

For example, the formula $EFp$ states that there is a possible future configuration where $p$ holds. One can read it as " $p$ is possible", or " $p$ may happen the future".

The formula $AFp$ states that whatever path is followed, some configuration where $p$ holds will eventually be reached. It can be read as " $p$ is inevitable", or " $p$ will happen in the future".

In the above examples, $EF$ and $AF$ are modalities. They link "simpler" statements about other configurations in order to build a "more complex" statement about the current configuration. They also define how these configurations are linked. With $EF$ we require one configuration reachable from the current configuration, hence a configuration that may happen in the future. With $AF$ we also refer to one future configuration but we require at least one such configuration along every run that start from the current configuration. Hence we require a set of configurations that will inevitably be visited.

Other CTL modalities

Other modalities are $EG$ and $AG$ . $EGp$ states that there is a run along which $p$ is always verified. One can read it as "it is possible that $p$ always holds." $AGp$ states that all reachable configurations satisfy $p$ , hence $p$ will always hold whatever path is chosen. One can read it as " $p$ will always holds."

Combining modalities

Checking CTL formulae over systems

The expressive power of CTL

Extensions of CTL

Bibliography

Operators

Logical operators

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

Binary operators:

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

Path operators

These operators "select" paths.

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

Relations with other logics

EME90 ^[1], MC ^[2], CTL vs. CTL+ ^[3], etc.

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

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.{{cite journal}}: CS1 maint: multiple names: authors list (link)
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.{{cite journal}}: CS1 maint: multiple names: authors list (link)
Emerson, E. A. (1990). "Temporal and modal logic". In J. van Leeuwen (ed.) (ed.). Handbook of Theoretical Computer Science, vol. B. MIT Press. pp. pp. 955–1072. ISBN 0262220393. {{cite book}}: |editor= has generic name (help); |pages= has extra text (help)