diff -r 5e8cacfd8396 -r 1c25f1de63a6 paper/src/paper.tex
--- a/paper/src/paper.tex	Sat Jul 09 15:48:37 2011 +0200
+++ b/paper/src/paper.tex	Sat Jul 09 21:14:09 2011 +0200
@@ -49,7 +49,7 @@
 \newtheorem*{def:frames}{Frames}
 \newtheorem*{def:models}{Models}
 \newtheorem*{def:satisfiability}{Satisfiability}
-\newtheorem*{def:fs closure}{Fischer-Ladner closure}
+\newtheorem*{def:fs closure}{Closure}
 \newtheorem*{def:atoms}{Atoms}
 \newtheorem*{def:rep function}{Representation function}
 
@@ -62,6 +62,7 @@
 \newtheorem{thm:model language}{Theorem}[section]
 \newtheorem{cor:mod=model language}{Corollary}[thm:model language]
 \newtheorem{cor:mod=program language}[cor:mod=model language]{Corollary}
+\newtheorem{thm:model checking}{Theorem}[section]
 
 \begin{document}
 \maketitle
@@ -252,30 +253,30 @@
 \end{def:rep function}
 
 \begin{def:fs closure}
-Let $\varphi$ be an LTL-formula, then the \emph{Fischer-Ladner closure} $FL(\varphi)$ of $\varphi$ is the smallest set of formulae such that following holds:
+Let $\varphi$ be an LTL-formula, then the \emph{Fischer-Ladner closure} $CL(\varphi)$ of $\varphi$ is the smallest set of formulae such that following holds:
 %\begin{multicols}{2}
 \begin{itemize}
-\item $\varphi \in FL(\varphi)$
-\item $\neg \psi \in FL(\varphi) \implies \psi \in FL(\varphi)$
-\item $\psi \in FL(\varphi) \implies \neg \psi \in FL(\varphi)$
-\item $\psi \lor \chi \in FL(\varphi) \implies \psi, \chi \in FL(\varphi)$
-\item $X \psi \in FL(\varphi) \implies \psi \in FL(\varphi)$
-\item $\psi U \chi \in FL(\varphi) \implies \psi, \chi, X(\psi U \chi) \in FL(\varphi)$
+\item $\varphi \in CL(\varphi)$
+\item $\neg \psi \in CL(\varphi) \implies \psi \in CL(\varphi)$
+\item $\psi \in CL(\varphi) \implies \neg \psi \in CL(\varphi)$
+\item $\psi \lor \chi \in CL(\varphi) \implies \psi, \chi \in CL(\varphi)$
+\item $X \psi \in CL(\varphi) \implies \psi \in CL(\varphi)$
+\item $\psi U \chi \in CL(\varphi) \implies \psi, \chi, X(\psi U \chi) \in CL(\varphi)$
 \end{itemize}
 %\end{multicols}
 \end{def:fs closure}
 
-\noindent Let $FL(\varphi)$ be the closure of formula $\varphi$, we define a subset with the \emph{until}-formulae of the closure $\mathbb{U}_\varphi \subseteq FL(\varphi)$ where:
-\[\mathbb{U}_\varphi = \{\psi U \chi \in FL(\varphi)\} \text{ and } \mathbb{U}_{\varphi_i} \text{ denotes the $i^{th}$ element of } \mathbb{U_\varphi}\]
+\noindent Let $CL(\varphi)$ be the closure of formula $\varphi$, we define a subset with the \emph{until}-formulae of the closure $\mathbb{U}_\varphi \subseteq CL(\varphi)$ where:
+\[\mathbb{U}_\varphi = \{\psi U \chi \in CL(\varphi)\} \text{ and } \mathbb{U}_{\varphi_i} \text{ denotes the $i^{th}$ element of } \mathbb{U_\varphi}\]
 
 \begin{def:atoms}
-Let $\varphi$ be a formula and $FL(\varphi)$ its closure. $A \subseteq FL(\varphi)$ is an \emph{atom} if following holds:
+Let $\varphi$ be a formula and $CL(\varphi)$ its closure. $A \subseteq CL(\varphi)$ is an \emph{atom} if following holds:
 \begin{itemize}
-\item $\forall{\psi \in FL(\varphi)}: \psi \in A \iff \neg \psi \notin A$
-\item $\forall{\psi \lor \chi \in FL(\varphi)}: \psi \lor \chi \in A \iff \psi \in A$ or $\chi \in A$ 
-\item $\forall{\psi U \chi \in FL(\varphi)}: \psi U \chi \in A \iff \chi \in A$ or $\psi, X(\psi U \chi) \in A$ 
+\item $\forall{\psi \in CL(\varphi)}: \psi \in A \iff \neg \psi \notin A$
+\item $\forall{\psi \lor \chi \in CL(\varphi)}: \psi \lor \chi \in A \iff \psi \in A$ or $\chi \in A$ 
+\item $\forall{\psi U \chi \in CL(\varphi)}: \psi U \chi \in A \iff \chi \in A$ or $\psi, X(\psi U \chi) \in A$ 
 \end{itemize}
-We define the set of all atoms of formula $\varphi$ with $\mathbb{AT}_\varphi = \{A \subseteq FL({\varphi}) \mid A \text{ is an atom}\}$.
+We define the set of all atoms of formula $\varphi$ with $\mathbb{AT}_\varphi = \{A \subseteq CL({\varphi}) \mid A \text{ is an atom}\}$.
 \end{def:atoms}
 
 \noindent Now that we have the required ingredients, we begin with the construction of automaton $\A_\varphi$ for formula $\varphi$. Let $\A_\varphi = (\Sigma, S, S_0, \Delta, \{F_i\}_{i < k})$ with:
@@ -285,7 +286,7 @@
 \item $S_0 = \{A \in \mathbb{AT_\varphi} \mid \varphi \in A\}$
 %\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)$
 \item $\Delta = \{(A, P, B) \mid A, B \in \mathbb{AT_\varphi}, P = A \cap Voc(\varphi), X \psi \in A \iff \psi \in B\}$
-%\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\}$
+%\item $\forall{i \in \N, i < k = |\mathbb{U}_{CL(\varphi)}|}: F_i = \{A \in \mathbb{AT}_\varphi \mid \psi U \chi \notin A$ or $\chi \in A\}$
 \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}|$
 %Let $A, B \in \mathbb{AT}$ and $P \subseteq Voc(\varphi)$. Then $(A, P, B) \in \Delta$ iff the following holds:
 %$P = A \cap Voc(\varphi)$ and For all $X \psi \in CL(\varphi): X \psi \in A$ iff $\psi \in B$.
@@ -336,11 +337,23 @@
 \section{Model checking}
 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$. 
 
-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:
+Given a program $P$ and specification $\varphi$, the verification problem is the following: \emph{does every run of P satisfy $\varphi$?} To show this we use the previously introduced automata constructions and reduce the problem to $L_\omega(\A_P) \subseteq L_\omega(\A_\varphi)$, i.e., all runs accepted by $\A_P$ are also accepted by $\A_\varphi$. By this problem definition, we clearly have to explore the whole state space of $\A_\varphi$ for each run of $\A_P$. This prevents efficient on-demand constructions. Therefore we rephrase the problem with the contrapositive definition $L_\omega(\A_P) \cap \overline{L_\omega(\A_\varphi)} = \emptyset$, where $\overline{L_\omega(\A_\varphi)} = \Sigma^\omega - L_\omega(\A_\varphi) = L_\omega(\A_{\neg \varphi})$ \cite{ref:alternating verification}.
+
+In conclusion, 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:
 \[L_\omega(\A_P) \cap L_\omega(\A_{\neg \varphi}) = \emptyset\]
+
+\begin{thm:model checking}
+\label{thm:model checking}
+Let $P$ be a finite-state program and $\A_P$ its automaton, let $\varphi$ be an LTL-formula and $\A_\varphi$ its automaton. P satisfies $\varphi$ iff $L_\omega(\A_P) \cap L_\omega(\A_{\neg \varphi}) = \emptyset$.
+\end{thm:model checking}
+
 From corollary \ref{cor:mod=model language} and \ref{cor:mod=program language} follows:
 \[L_\omega(\A_P) \cap L_\omega(\A_{\neg \varphi}) = \emptyset \iff Mod(P) \cap Mod(\neg \varphi) = \emptyset\]
 
+\subsection{Complexity}
+Let the size $|P|$ of a program $P = (S, s_0, R, V)$ be proportional to the sum of its structural components, i.e., $|P| = |S| + |R|$. The size $|\varphi|$ is the length of the formula string. The asymptotical complexity of the presented automata-theoretic verification method is in time $O(|P| \cdot 2^{O(|\varphi|)})$\cite{ref:concurrent checking}. 
+
+The size of $\varphi$ is usually short \cite{ref:concurrent checking}, so the exponential growth by it is reasonable. Generally, the number of states is at least exponential in the size of its description by means of a programming language, meaning that despite that the upper bound is polynomial in the size of the program, in practice, we are facing exponential growth in complexity \cite{ref:handbook}.
 
 \section{On-the-fly methods}
 
@@ -350,17 +363,16 @@
 {\em Linear-Time Temporal Logic and B\"uchi Automata}.
 Winter School on Logic and Computer Science, Indian Statistical Institute, Calcutta, 1997.
 
-\bibitem{ref:handbook} 
-\uppercase{P{\footnotesize atrick} B{\footnotesize lackburn}, 
-F{\footnotesize rank} W{\footnotesize olter and} J{\footnotesize ohan van} B{\footnotesize enthem}.}
-{\em Handbook of Modal Logic (Studies in Logic and Practical Reasoning)}.
-3rd Edition, Elsevier, Amsterdam, 2007.
-
 \bibitem{ref:alternating verification} 
 \uppercase{M{\footnotesize oshe} Y. V{\footnotesize ardi}.}
 {\em Alternating Automata and Program Verification}.
 Computer Science Today, Volume 1000 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, 1995.
 
+\bibitem{ref:concurrent checking}
+\uppercase{O{\footnotesize rna} L{\footnotesize ichtenstein and} A{\footnotesize mir} P{\footnotesize nueli}.}
+{\em Checking that finite state concurrent programs satisfy their linear specification}.
+Proceeding 12th ACM Symposium on Principles of Programming Languages, New York, 1985.
+
 \bibitem{ref:infpaths}
 \uppercase{P{\footnotesize ierre} W{\footnotesize olper}, 
 M{\footnotesize oshe} Y. V{\footnotesize ardi and}
@@ -368,5 +380,10 @@
 {\em Reasoning about Infinite Computation Paths}.
 In Proceedings of the 24th IEEE FOCS, 1983.
 
+\bibitem{ref:handbook} 
+\uppercase{P{\footnotesize atrick} B{\footnotesize lackburn}, 
+F{\footnotesize rank} W{\footnotesize olter and} J{\footnotesize ohan van} B{\footnotesize enthem}.}
+{\em Handbook of Modal Logic (Studies in Logic and Practical Reasoning)}.
+3rd Edition, Elsevier, Amsterdam, 2007.
 \end{thebibliography}
 \end{document}