Begin with model checking.
authorEugen Sawin <sawine@me73.com>
Thu, 30 Jun 2011 20:45:45 +0200
changeset 25636403068f28
parent 24 1d28f5f04efd
child 26 1fbb8602afee
Begin with model checking.
paper/src/paper.tex
     1.1 --- a/paper/src/paper.tex	Thu Jun 30 19:08:30 2011 +0200
     1.2 +++ b/paper/src/paper.tex	Thu Jun 30 20:45:45 2011 +0200
     1.3 @@ -314,7 +314,7 @@
     1.4  \item $S_0 = \{A \in \mathbb{AT_\varphi} \mid \varphi \in A\}$
     1.5  %\item $(A, P, B) \in \Delta$ for $A, B \in \mathbb{AT_\varphi}$ and $P = A \cap Voc(\varphi) \iff (X \psi \in A \iff \psi \in B)$
     1.6  \item $\Delta = \{(A, P, \mathbb{B}) \mid A, \mathbb{B} \in \mathbb{AT_\varphi}, P = A \cap Voc(\varphi), X \psi \in A \iff \psi \in \mathbb{B}\}$
     1.7 -\item $\forall{i \in \N, i < k = |\mathbb{U}_{FL(\varphi)}|}: F_i = \{A \in \mathbb{AT}_\varphi \mid \psi U \chi \notin A$ or $\chi \in A\}$
     1.8 +%\item $\forall{i \in \N, i < k = |\mathbb{U}_{FL(\varphi)}|}: F_i = \{A \in \mathbb{AT}_\varphi \mid \psi U \chi \notin A$ or $\chi \in A\}$
     1.9  \item $F_i = \{A \in \mathbb{AT}_\varphi \mid \psi U \chi = \mathbb{U}_{\varphi_i}, \psi U \chi \notin A$ or $\chi \in A\}$ and therefore $k = |\mathbb{U}_{\varphi}|$
    1.10  %Let $A, B \in \mathbb{AT}$ and $P \subseteq Voc(\varphi)$. Then $(A, P, B) \in \Delta$ iff the following holds:
    1.11  %$P = A \cap Voc(\varphi)$ and For all $X \psi \in CL(\varphi): X \psi \in A$ iff $\psi \in B$.