Fixed paper header and satisfication.
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: