Computation tree logic: Difference between revisions

Revision as of 13:07, 6 March 2023

Revision as of 17:50, 15 March 2023

Line 50:

**''φ'' '''W''' ''ψ'' – '''W'''eak 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 operatoroperators must always be grouped in twopairs: one path operator followed by a state operator. See the examples below. [[CTL*]] is strictly more expressive than CTL.

===Minimal set of operators===

Line 69:

===Definition===

CTL formulae are interpreted over [[transition system]]s. A transition system is a triple <math>\mathcal{M}=(S,{\rightarrow},L)</math>, where <math>S</math> is a set of states, <math>{\rightarrow} \subseteq S \times S</math> is a transition relation, assumed to be serial, i.e. every state has at least one successor, and <math>L</math> is a labelling function, assigning propositional letters to states. Let <math>\mathcal{M}=(S,\rightarrow,L)</math> be such a transition model, with <math>s \in S</math>, and <math>\phi \in F</math>, where <math>F</math> is the set of [[well-formed formula]]s over the [[Formal language|language]] of <math>\mathcal{M}</math>.

:with <math>s \in S, \phi \in F</math> where F is the set of [[Well formed formula|wffs]] over the [[Regular Language|language]] of <math>\mathcal{M}</math>.

Then the relation of semantic [[entailment]] <math>(\mathcal{M}, s \models \phi)</math> is defined recursively on <math>\phi</math>: