Content deleted Content added
→Definition: typo |
→Definition: minor spacing fix |
||
Line 67:
===Definition===
CTL formulae are interpreted over [[Transition system|Transition Systems]]. 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, \phi \in F</math> where F is the set of [[Well formed formula|wffs]] over the [[Regular Language|language]] of <math>\mathcal{M}</math>.
| |||