Computation tree logic: Difference between revisions

Revision as of 14:17, 1 July 2017

Revision as of 09:39, 19 February 2018

Line 70:

: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 by [[structural induction]]recursively on <math>\phi</math>:

# <math>\Big( (\mathcal{M}, s) \models \top \Big) \Leftrightarrow \Big( (\mathcal{M}, s) \not\models \bot \Big)</math>

# <math>\Big( (\mathcal{M}, s) \models p \Big) \Leftrightarrow \Big( p \in L(s) \Big)</math>