1.1 --- a/paper/src/paper.tex	Tue Jun 28 14:45:02 2011 +0200
     1.2 +++ b/paper/src/paper.tex	Tue Jun 28 14:49:59 2011 +0200
     1.3 @@ -211,6 +211,11 @@
     1.4  \item $\Box \varphi \equiv \neg \Diamond \neg \varphi$
     1.5  \end{itemize}
     1.6  \end{multicols}
     1.7 +From the derivations for operators $\Diamond$, \emph{read diamond}, and $\Box$, \emph{read box}, it follows:
     1.8 +\begin{itemize}
     1.9 +\item $M,i \models \Diamond \varphi$ iff $\exists{k \geq i}: M,k \models \varphi$
    1.10 +\item $M,i \models \Box \varphi$ iff $\forall{k \geq i}: M,k \models \varphi$
    1.11 +\end{itemize}
    1.12  
    1.13  \section{Model checking}
    1.14