Content deleted Content added
m Replacing deprecated latex syntax mw:Extension:Math/Roadmap |
→Definition: typo |
||
Line 68:
===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|
Then the relation of semantic [[entailment]] <math>(\mathcal{M}, s \models \phi)</math> is defined recursively on <math>\phi</math>:
| |||