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. 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". 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 are minimal sets of operators. All CTL formulas can be transformed to use only those operators. This is useful in model checking. One minimal set of operators is: {true, ∨, ¬, EG, EU, EX}. Some of the transformations used for temporal operators are: EFφ == E[trueU(φ)] ( because Fφ == [trueU(φ)] ) AXφ == ¬EX(¬φ) AGφ == ¬EF(¬φ) == ¬ E[trueU(¬φ)] AFφ == A[trueUφ] == ¬EG(¬φ) A[φUψ] == ¬( E[(¬ψ)U¬(φ∨ψ)] ∨ EG(¬ψ) ) Semantics of CTL Definition CTL formulae are interpreted over transition system. 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 language of . Then the relation of semantic entailment is defined recursively 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