The propositional branching-time logic CTL (Computational Temporal Logic) is historically the forerunner of . It has been introduced by Clarke and Emerson (1981) [66]. Only later, when the expressive limits of CTL became more known has been introduced by Emerson and Halpern (1986) [95] as a possible unifying framework for CTL and PLTL (cf. Emerson (1990) [92], P.1012).

The language is a proper subset of :

(6.21) |

This is caused by some syntactical constraints valid for (cf. figure 6.1).

(6.22) | |||

(6.23) | |||

(6.24) | |||

(6.25) | |||

(6.26) | |||

(6.27) | |||

(6.28) | |||

(6.29) | |||

(6.30) | |||

(6.31) | |||

(6.32) |

An alternative syntactic definition of CTL can be given as follows ( := Atomic Propositions = , SF := State Formulas, PF := Path Formulas):

- If then and in SF as well as
- If then in PF
- If then in SF
- Only (1) - (5) define the set of

Some other equivalences are the following ones. Having the temporal logical operators (always) and (eventually) one can define:

(6.33) | |||

(6.34) | |||

(6.35) | |||

(6.36) |

Gerd Doeben-Henisch 2010-03-03