1.1 --- a/paper/src/paper.tex	Wed Jul 27 11:24:57 2011 +0200
     1.2 +++ b/paper/src/paper.tex	Sat Jul 30 13:29:34 2011 +0200
     1.3 @@ -1,5 +1,4 @@
     1.4 -\documentclass{beamer}
     1.5 -%\documentclass[a4paper, pagesize, DIV=calc, smallheadings]{article}  
     1.6 +\documentclass[a4paper, pagesize, DIV=calc, smallheadings]{article}  
     1.7  \usepackage{graphicx}
     1.8  %\usepackage[latin1]{inputenc}
     1.9  \usepackage{amsmath, amsthm, amssymb, amsfonts, verbatim}
    1.10 @@ -10,7 +9,7 @@
    1.11  \usepackage{tikz}
    1.12  \usetikzlibrary{automata}
    1.13  \usepackage{sidecap}
    1.14 -\usepackage{wrapfig}
    1.15 +%\usepackage{wrapfig}
    1.16  \usepackage{subfig}
    1.17  %\usepackage{fullpage}
    1.18  %\usepackage{a4wide}
    1.19 @@ -62,7 +61,7 @@
    1.20  \newtheorem*{def:vocabulary}{Vocabulary}
    1.21  \newtheorem*{def:frames}{Frames}
    1.22  \newtheorem*{def:models}{Models}
    1.23 -\newtheorem*{def:satisfiability}{Satisfiability}
    1.24 +\newtheorem*{def:satisfication}{Satisfication}
    1.25  \newtheorem*{def:fs closure}{Closure}
    1.26  \newtheorem*{def:atoms}{Atoms}
    1.27  \newtheorem*{def:rep function}{Representation function}
    1.28 @@ -312,8 +311,8 @@
    1.29  \label{fig:model}
    1.30  \end{figure}
    1.31  %
    1.32 -\begin{def:satisfiability}
    1.33 -A model $\M = (\F, V)$ \emph{satisfies} a formula $\varphi$ at time instant $i$ is denoted by $\M,i \models \varphi$. Satisfiability of a formula $\varphi$ is defined inductively over the structure of $\varphi$:
    1.34 +\begin{def:satisfication}
    1.35 +A model $\M = (\F, V)$ \emph{satisfies} a formula $\varphi$ at time instant $i$ is denoted by $\M,i \models \varphi$. Satisfication of a formula $\varphi$ is defined inductively over the structure of $\varphi$:
    1.36  \begin{itemize}
    1.37  \item $\M,i \models p$ for $p \in \Prop \iff p \in V(i)$
    1.38  \item $\M,i \models \neg \varphi \iff$ not $\M,i \models \varphi$
    1.39 @@ -321,11 +320,11 @@
    1.40  \item $\M,i \models \X \varphi \iff \M,i+1 \models \varphi$
    1.41  \item $\M,i \models \varphi \U \psi \iff \exists{k \geq i}: \M,k \models \psi$ and $\forall{i \leq j < k}: \M,j \models\varphi$
    1.42  \end{itemize}
    1.43 -\end{def:satisfiability}
    1.44 +\end{def:satisfication}
    1.45  %
    1.46  \noindent From the strict linear order of the LTL-frame accessibility relation follows that an LTL-formula $\varphi$ is \emph{satisfiable}, iff there exists a model $\M$ with $\M,0 \models \varphi$.
    1.47  
    1.48 -We clearly see, that atomic propositions, which are not contained within the formula $\varphi$ are redundant to the the definition of the satisfiability. By defining the \emph{vocabulary} of a formula, we dispose such irrelevant atomic proposition from the alphabet.
    1.49 +We clearly see, that atomic propositions, which are not contained within the formula $\varphi$ are redundant to the the definition of the satisfication. By defining the \emph{vocabulary} of a formula, we dispose such irrelevant atomic proposition from the alphabet.
    1.50  
    1.51  \begin{def:vocabulary}
    1.52  Let $\varphi$ be an LTL-formula over atomic propositions $\Prop$, we define the \emph{vocabulary} $Voc(\varphi)$ of $\varphi$ inductively:
    1.53 @@ -521,7 +520,7 @@
    1.54  A more space-efficient strategy is the on-the-fly construction of the automaton during a depth-first search, short DFS. The DFS explores the product states of both automata incrementally, testing for cycles in each iteration. If the program does not satisfy a formula, an accepting cycle will occur and lead to termination of the search. In the case of a valid program, i.e., the program does meet the specification, no cycles will occur. In the latter case, such a strategy would inevitably explore the whole state space of the automata.
    1.55  
    1.56  \subsection{Two-state semantics}
    1.57 -A new interpretation for the infinite computation paths will help us in the incremental construction of automata. We separate the computation paths in two states by applying temporal reasoning; and we do so incrementally for each time instant. The two states resemble the satisfiability requirements for any time instant $i$ and its successor $i+1$.
    1.58 +A new interpretation for the infinite computation paths will help us in the incremental construction of automata. We separate the computation paths in two states by applying temporal reasoning; and we do so incrementally for each time instant. The two states resemble the satisfication requirements for any time instant $i$ and its successor $i+1$.
    1.59  
    1.60  \subsubsection{Example}
    1.61  Let $\varphi = a \U b$. We apply the two-state semantics on $\varphi$ and it follows: