PhS |
I am Philippe Schnoebelen, b. 1961, French citizen, currently living in Paris.
Some pages on my TODO list:
=CTL=
Regarding CTL, I keep a current draft here:
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 EF p 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 AF p 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. EG p states that there is a run along which p is always verified. One can read it as it is possible that p always holds. AG p 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: eg,or,and, ightarrow 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 , MC , CTL vs. CTL+ , etc.
Computational tree logic (CTL) is a subset of CTL*.
=See also=
*Linear temporal logic
=References=
#
#
#|
|