Computational tree logic
Encyclopedia
Computation tree logic (CTL) is a branching-time logic
, meaning that its model of time is a tree-like structure in which the future is not determined; there are different paths in the future, any one of which might be an actual path that is realised. It is used in formal verification
of software or hardware artifacts, typically by software applications known as model checkers which determine if a given artifact possesses safety or liveness properties. For example, CTL can specify that when some initial condition is satisfied (e.g., all program variables are positive or no cars on a highway straddle two lanes), then all possible executions of a program avoid some undesirable condition (e.g., dividing a number by zero or two cars colliding on a highway). In this example, the safety property could be verified by a model checker that explores all possible transitions out of program states satisfying the initial condition and ensures that all such executions satisfy the property. Computation tree logic is in a class of temporal logic
s that include linear temporal logic
(LTL). Although there are properties expressible in only one of CTL and LTL, all properties expressible in either logic can also be expressed in CTL*.
of well formed formulas for CTL is generated by the following grammar
:
where
ranges over a set of atomic formula
s. Not all of these connectives are needed – for example,
comprises a complete set of connectives, and the others can be defined using them.
For example, the following is a well-formed CTL formula:
The following is not a well-formed CTL formula:
The problem with this string is that
can occur only when paired with an 
or an 
. It uses atomic propositions as its building blocks to make statements about the states of a system. CTL then combines these propositions into formulas using logical operators and temporal logic
s.
are the usual ones:
and 
. Along with these operators CTL formulas can also make use of the boolean constants true
and false
.
In CTL*, the temporal operators can be freely mixed. In CTL, the operator must always be grouped in two: one path operator followed by a state operator. See the examples below. CTL* is strictly more expressive than CTL.
. One minimal set of operators is: {false,
, EG, EU, EX}.
Some of the transformation used for temporal operator are:
, where 
is a set of states, 
is a transition relation, assumed to be serial, i.e. every state has at least one successor, and 
is a labelling function, assigning propositional letters to states. Let 
be such a transition model
Then the relation of semantic entailment
is defined by Structural Induction
on
:
they are assertions about the nature of the infinitely deep computation tree rooted at the given state
.
and 
are said to be semantically equivalent if any state in any model which satisfies one also satisfies the other.
This is denoted
It can be seen that A and E are duals, being universal and existential computation path quantifiers respectively:
.
Furthermore so are G and F.
Hence an instance of De Morgan's Laws can be formulated in CTL:
It can be shown using such identities that a subset of the CTL temporal connectives is adequate if it contains
, at least one of 
and at least one of 
and the boolean connectives.
The important equivalences below are called the expansion laws; they allow to unfold the verification of a CTL connective towards its successors in time.
(ATL).
Computation tree logic (CTL) and Linear temporal logic
(LTL) are both a subset of CTL*. CTL and LTL
are not equivalent and they have a common subset, which is a proper subset of both CTL and LTL.
Mathematical logic
Mathematical logic is a subfield of mathematics with close connections to foundations of mathematics, theoretical computer science and philosophical logic. The field includes both the mathematical study of logic and the applications of formal logic to other areas of mathematics...
, meaning that its model of time is a tree-like structure in which the future is not determined; there are different paths in the future, any one of which might be an actual path that is realised. It is used in formal verification
Formal verification
In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal methods of mathematics .- Usage :Formal verification can be...
of software or hardware artifacts, typically by software applications known as model checkers which determine if a given artifact possesses safety or liveness properties. For example, CTL can specify that when some initial condition is satisfied (e.g., all program variables are positive or no cars on a highway straddle two lanes), then all possible executions of a program avoid some undesirable condition (e.g., dividing a number by zero or two cars colliding on a highway). In this example, the safety property could be verified by a model checker that explores all possible transitions out of program states satisfying the initial condition and ensures that all such executions satisfy the property. Computation tree logic is in a class of temporal logic
Temporal logic
In logic, the term temporal logic is used to describe any system of rules and symbolism for representing, and reasoning about, propositions qualified in terms of time. In a temporal logic we can then express statements like "I am always hungry", "I will eventually be hungry", or "I will be hungry...
s that include linear temporal logic
Linear temporal logic
In logic, Linear temporal logic is a modal temporal logic with modalities referring to time. In LTL, one can encode formulae about the future of paths such as that a condition will eventually be true, that a condition will be true until another fact becomes true, etc. It is a fragment of the more...
(LTL). Although there are properties expressible in only one of CTL and LTL, all properties expressible in either logic can also be expressed in CTL*.
Syntax of CTL
The languageRegular language
In theoretical computer science and formal language theory, a regular language is a formal language that can be expressed using regular expression....
of well formed formulas for CTL is generated by the following grammar
Context-free grammar
In formal language theory, a context-free grammar is a formal grammar in which every production rule is of the formwhere V is a single nonterminal symbol, and w is a string of terminals and/or nonterminals ....
:
where
ranges over a set of atomic formulaAtomic formula
In mathematical logic, an atomic formula is a formula with no deeper propositional structure, that is, a formula that contains no logical connectives or equivalently a formula that has no strict subformulas. Atoms are thus the simplest well-formed formulas of the logic...
s. Not all of these connectives are needed – for example,
comprises a complete set of connectives, and the others can be defined using them.
means 'along All paths' (Inevitably)
means 'along at least (there Exists) one path' (possibly)
For example, the following is a well-formed CTL formula:
The following is not a well-formed CTL formula:
The problem with this string is that
can occur only when paired with an or an . It uses atomic propositions as its building blocks to make statements about the states of a system. CTL then combines these propositions into formulas using logical operators and temporal logicTemporal logic
In logic, the term temporal logic is used to describe any system of rules and symbolism for representing, and reasoning about, propositions qualified in terms of time. In a temporal logic we can then express statements like "I am always hungry", "I will eventually be hungry", or "I will be hungry...
s.
Logical operators
The logical operatorsLogical connective
In logic, a logical connective is a symbol or word used to connect two or more sentences in a grammatically valid way, such that the compound sentence produced has a truth value dependent on the respective truth values of the original sentences.Each logical connective can be expressed as a...
are the usual ones:
and . Along with these operators CTL formulas can also make use of the boolean constants trueTrue
True may refer to:* Truth, the state of being in accord with fact or reality-Music:* True , 1996* True , 2002* True , 1983** "True"...
and false
False
False or falsehood may refer to:*False *Lie or falsehood, a type of deception in the form of an untruthful statement*Falsity or falsehood, in law, deceitfulness by one party that results in damage to another...
.
Temporal operators
The temporal operators are the following:- Quantifiers over 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.
- A
- Path-specific quantifiers
- X
– Next: 
has to hold at the next state (this operator is sometimes noted N instead of X). - G
– Globally: 
has to hold on the entire subsequent path. - F
– Finally: 
eventually has to hold (somewhere on the subsequent path). 
U 
– Until: 
has to hold at least 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".
- X
In CTL*, the temporal operators can be freely mixed. In CTL, the operator must always be grouped in two: one path operator followed by a state operator. See the examples below. CTL* is strictly more expressive than CTL.
Minimal set of operators
In CTL there is a minimal set of operators. All CTL formulas can be transformed to use only those operators. This is useful in model checkingModel checking
In computer science, model checking refers to the following problem:Given a model of a system, test automatically whether this model meets a given specification....
. One minimal set of operators is: {false,
, EG, EU, EX}.Some of the transformation used for temporal operator are:
- EF
E[trueU(
[trueU(
)] ( because F
)] ) - AX
EX(
) - AG
EF(
) 
E[trueU(
)] - AF
A[trueU
] 
EG(
) - A[
U
] 
( E[(
)U
(
)] 
EG(
) )
Definition
CTL formulae are interpreted over Transition Systems. A transition system is a triple, where is a set of states, is a transition relation, assumed to be serial, i.e. every state has at least one successor, and is a labelling function, assigning propositional letters to states. Let be such a transition model
- with
where F is the set of wffs over the LanguageRegular languageIn theoretical computer science and formal language theory, a regular language is a formal language that can be expressed using regular expression....
of
.
Then the relation of semantic entailment
Entailment
In logic, entailment is a relation between a set of sentences and a sentence. Let Γ be a set of one or more sentences; let S1 be the conjunction of the elements of Γ, and let S2 be a sentence: then, Γ entails S2 if and only if S1 and not-S2 are logically inconsistent...
is defined by Structural InductionStructural induction
Structural induction is a proof method that is used in mathematical logic , computer science, graph theory, and some other mathematical fields. It is a generalization of mathematical induction...
on
:
Characterisation of CTL
Rules 10–15 above refer to computation paths in models and are what ultimately characterise the "Computation Tree";they are assertions about the nature of the infinitely deep computation tree rooted at the given state
.Semantic equivalences
The formulae and are said to be semantically equivalent if any state in any model which satisfies one also satisfies the other.This is denoted
It can be seen that A and E are duals, being universal and existential computation path quantifiers respectively:
.Furthermore so are G and F.
Hence an instance of De Morgan's Laws can be formulated in CTL:
It can be shown using such identities that a subset of the CTL temporal connectives is adequate if it contains
, at least one of and at least one of and the boolean connectives.The important equivalences below are called the expansion laws; they allow to unfold the verification of a CTL connective towards its successors in time.
Examples
Let "P" mean "I like chocolate" and Q mean "It's warm outside."- AG.P
- "I will like chocolate from now on, no matter what happens."
- EF.P
- "It's possible I may like chocolate some day, at least for one day."
- AF.EG.P
- "It's always possible (AF) that I will suddenly start liking chocolate for the rest of time." (Note: not just the rest of my life, since my life is finite, while G is infinite).
- EG.AF.P
- "This is a critical time in my life. Depending on what happens next (E), it's possible that for the rest of time (G), there will always be some time in the future (AF) when I will like chocolate. However, if the wrong thing happens next, then all bets are off and there's no guarantee about whether I'll ever like chocolate."
- A(PUQ)
- "From now until it's warm outside, I will like chocolate every single day. Once it's warm outside, all bets are off as to whether I'll like chocolate anymore. Oh, and it's guaranteed to be warm outside eventually, even if only for a single day."
- E((EX.P)U(AG.Q))
- "It's possible that: there will eventually come a time when it will be warm forever (AG.Q) and that before that time there will always be some way to get me to like chocolate the next day (EX.P)."
Relations with other logics
Computation tree logic (CTL) is a subset of CTL* as well as of the modal µ calculus. CTL is also a fragment of Alur, Henzinger and Kupferman's Alternating-time Temporal LogicAlternating-time Temporal Logic
In computer science, Alternating-time Temporal Logic, or ATL, is a branching-time temporal logic that naturally describes computations of multi-agent system and multiplayer games.. It offers selective quantification over program-paths that are possible outcomes of games...
(ATL).
Computation tree logic (CTL) and Linear temporal logic
Linear temporal logic
In logic, Linear temporal logic is a modal temporal logic with modalities referring to time. In LTL, one can encode formulae about the future of paths such as that a condition will eventually be true, that a condition will be true until another fact becomes true, etc. It is a fragment of the more...
(LTL) are both a subset of CTL*. CTL and LTL
Linear temporal logic
In logic, Linear temporal logic is a modal temporal logic with modalities referring to time. In LTL, one can encode formulae about the future of paths such as that a condition will eventually be true, that a condition will be true until another fact becomes true, etc. It is a fragment of the more...
are not equivalent and they have a common subset, which is a proper subset of both CTL and LTL.
- FG.P exists in LTL but not in CTL.
- AG(P
((EX.Q)
(EX¬Q))) exists in CTL but not in LTL.