# HG changeset patch
# User Eugen Sawin <sawine@me73.com>
# Date 1312025374 -7200
# Node ID a58b1c34b2d84260dfcc5969d41cb50ad6314ae8
# Parent  33e7afb3f40263a4c3b4754735512fe5d0bfddfc
Fixed paper header and satisfication.

diff -r 33e7afb3f402 -r a58b1c34b2d8 paper/src/paper.tex
--- a/paper/src/paper.tex	Wed Jul 27 11:24:57 2011 +0200
+++ b/paper/src/paper.tex	Sat Jul 30 13:29:34 2011 +0200
@@ -1,5 +1,4 @@
-\documentclass{beamer}
-%\documentclass[a4paper, pagesize, DIV=calc, smallheadings]{article}  
+\documentclass[a4paper, pagesize, DIV=calc, smallheadings]{article}  
 \usepackage{graphicx}
 %\usepackage[latin1]{inputenc}
 \usepackage{amsmath, amsthm, amssymb, amsfonts, verbatim}
@@ -10,7 +9,7 @@
 \usepackage{tikz}
 \usetikzlibrary{automata}
 \usepackage{sidecap}
-\usepackage{wrapfig}
+%\usepackage{wrapfig}
 \usepackage{subfig}
 %\usepackage{fullpage}
 %\usepackage{a4wide}
@@ -62,7 +61,7 @@
 \newtheorem*{def:vocabulary}{Vocabulary}
 \newtheorem*{def:frames}{Frames}
 \newtheorem*{def:models}{Models}
-\newtheorem*{def:satisfiability}{Satisfiability}
+\newtheorem*{def:satisfication}{Satisfication}
 \newtheorem*{def:fs closure}{Closure}
 \newtheorem*{def:atoms}{Atoms}
 \newtheorem*{def:rep function}{Representation function}
@@ -312,8 +311,8 @@
 \label{fig:model}
 \end{figure}
 %
-\begin{def:satisfiability}
-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$:
+\begin{def:satisfication}
+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$:
 \begin{itemize}
 \item $\M,i \models p$ for $p \in \Prop \iff p \in V(i)$
 \item $\M,i \models \neg \varphi \iff$ not $\M,i \models \varphi$
@@ -321,11 +320,11 @@
 \item $\M,i \models \X \varphi \iff \M,i+1 \models \varphi$
 \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$
 \end{itemize}
-\end{def:satisfiability}
+\end{def:satisfication}
 %
 \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$.
 
-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.
+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.
 
 \begin{def:vocabulary}
 Let $\varphi$ be an LTL-formula over atomic propositions $\Prop$, we define the \emph{vocabulary} $Voc(\varphi)$ of $\varphi$ inductively:
@@ -521,7 +520,7 @@
 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.
 
 \subsection{Two-state semantics}
-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$.
+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$.
 
 \subsubsection{Example}
 Let $\varphi = a \U b$. We apply the two-state semantics on $\varphi$ and it follows: