1.1 --- a/paper/src/paper.tex	Sat Jul 09 03:48:35 2011 +0200
     1.2 +++ b/paper/src/paper.tex	Sat Jul 09 15:48:37 2011 +0200
     1.3 @@ -56,10 +56,12 @@
     1.4  \theoremstyle{plain}
     1.5  \newtheorem{prop:vocabulary sat}{Proposition}[section]
     1.6  \newtheorem{prop:general equiv}{Proposition}[section]
     1.7 +\newtheorem{prop:computation set=language}{Proposition}[section]
     1.8  
     1.9  \theoremstyle{plain}
    1.10  \newtheorem{thm:model language}{Theorem}[section]
    1.11  \newtheorem{cor:mod=model language}{Corollary}[thm:model language]
    1.12 +\newtheorem{cor:mod=program language}[cor:mod=model language]{Corollary}
    1.13  
    1.14  \begin{document}
    1.15  \maketitle
    1.16 @@ -151,7 +153,7 @@
    1.17  
    1.18  \begin{prop:general equiv}
    1.19  Let $\A = (\Sigma, S, S_0, \Delta, \{F_i\}_{i < k})$ be a \emph{generalised automaton} and let $\A_i = (\Sigma, S, S_0, \Delta, F_i)$ be \emph{non-deterministic automata}, then following equivalance condition holds:
    1.20 -\[L(\A) = \bigcap_{i < k} L(\A_i)\]
    1.21 +\[L_\omega(\A) = \bigcap_{i < k} L_\omega(\A_i)\]
    1.22  \end{prop:general equiv}
    1.23  \noindent Intuitively follows the equivalance of the language recognition abilities of general and non-deterministic B\"uchi automata.
    1.24  
    1.25 @@ -292,7 +294,7 @@
    1.26  \begin{thm:model language}
    1.27  \label{thm:model language}
    1.28  Let $\M_\varphi = (\F, V_\varphi)$ be a model and $rep(\M_\varphi)$ its infinite representation word, then following holds:
    1.29 -\[rep(\M_\varphi) \in L(\A_\varphi) \iff \M_\varphi,0 \models \varphi\]
    1.30 +\[rep(\M_\varphi) \in L_\omega(\A_\varphi) \iff \M_\varphi,0 \models \varphi\]
    1.31  \end{thm:model language}
    1.32  \noindent
    1.33  \begin{proof}
    1.34 @@ -300,7 +302,7 @@
    1.35  \end{proof}
    1.36  \begin{cor:mod=model language}
    1.37  \label{cor:mod=model language}
    1.38 -From theorem \ref{thm:model language} follows $Mod(\varphi) = L(\A_\varphi)$
    1.39 +From theorem \ref{thm:model language} follows $Mod(\varphi) = L_\omega(\A_\varphi)$.
    1.40  \end{cor:mod=model language}
    1.41  
    1.42  \subsection{Program automata}
    1.43 @@ -311,21 +313,34 @@
    1.44  \begin{multicols}{2}
    1.45  \item $\Sigma = 2^\Prop$
    1.46  \item $S = S_P$
    1.47 -\item $S_0 = s_0$
    1.48 +\item $S_0 = \{s_0\}$
    1.49  \item $F = S$
    1.50  \end{multicols}
    1.51  \item $\Delta = \{(s, V(s), s') \mid \exists{a \in \Prop}: (s, a, s') \in R\}$
    1.52  \end{itemize}
    1.53 -From $F = S$ follows that each run of $\A_P$ is accepting, therefore is $L_\omega(\A_P)$ the set of all computations of $P$.
    1.54 +In practical verification of programs, the specification covers only the properties of a system, which are vital to the program's correctness, where our program description contains all details of all possible execution paths. Let $\varphi$ be the specification formula, we can reduce the state exploration to the vocabulary of $\varphi$ by the reduction of the transition relation to $\Delta = \{(s, A, s') \mid \exists{a \in \Prop}: (s, a, s') \in R \land A = V(s) \cap Voc(\varphi)\}$.
    1.55  
    1.56 +\begin{prop:computation set=language}
    1.57 +\label{prop:computation set=language}
    1.58 +Let $\A_P = (\Sigma, S, S_0, \Delta, F)$, for $F = S$ it follows that each run of $\A_P$ is accepting, therefore is $L_\omega(\A_P)$ the set of all computations of $P$.
    1.59 +\[L_\omega(\A_P) = \{\rho \mid \rho \text{ is a run of } \A_P\}\]
    1.60 +\end{prop:computation set=language}
    1.61 +
    1.62 + We can view each run of $\A_P$, i.e., each computation of $P$, as a representation of model $\M_\rho = (\F, V)$, where $\F$ is a frame and $V$ the program's valuation function. In analogy to the specification, we define:
    1.63 +\[Mod(P) = \{\rho \mid \rho \text{ is a computation of } P\}\]
    1.64 +\begin{cor:mod=program language}
    1.65 +\label{cor:mod=program language}
    1.66 +From theorem \ref{thm:model language} and proposition \ref{prop:computation set=language} follows $Mod(P) = L_\omega(\A_P)$.
    1.67 +\end{cor:mod=program language}
    1.68  
    1.69  \section{Model checking}
    1.70 -For effective automata-theoretic verification of reactive programs, we model the program as a non-deterministic B\"uchi automaton $P = (\Sigma, S, S_0, \Delta, F)$. Let $\rho$ be a run of $P$, we define:
    1.71 -\[Mod(P) = \{rep^{-1}(\rho) \mid \rho \text{ is a run of } P\}\]
    1.72 +For effective automata-theoretic verification of reactive programs, we have modelled the program as a non-deterministic B\"uchi automaton $\A_P$ and the specification formula $\varphi$ as automaton $\A_\varphi$. 
    1.73 +
    1.74  The essence of model checking lies within the test for emptyness of the intersection between the recognised language of the program automaton and the recognised language of the automaton for its negated specification:
    1.75 -\[L(\A_P) \cap L(\A_{\neg \varphi}) = \emptyset\]
    1.76 -From corollary \ref{cor:mod=model language} follows:
    1.77 -\[L(\A_P) \cap L(\A_{\neg \varphi}) = \emptyset \iff Mod(P) \cap Mod(\neg \varphi) = \emptyset\]
    1.78 +\[L_\omega(\A_P) \cap L_\omega(\A_{\neg \varphi}) = \emptyset\]
    1.79 +From corollary \ref{cor:mod=model language} and \ref{cor:mod=program language} follows:
    1.80 +\[L_\omega(\A_P) \cap L_\omega(\A_{\neg \varphi}) = \emptyset \iff Mod(P) \cap Mod(\neg \varphi) = \emptyset\]
    1.81 +
    1.82  
    1.83  \section{On-the-fly methods}
    1.84