Syntax of CTL
The language of well formed formulas for CTL is generated by the following grammar:
where ranges over a set of atomic formulas. 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 logics.
Read more about this topic: Computation Tree Logic