diff -r 68fff3a1453e -r 8a3d0605adf5 paper/src/paper.tex
--- a/paper/src/paper.tex	Tue Jun 28 00:16:13 2011 +0200
+++ b/paper/src/paper.tex	Tue Jun 28 14:45:02 2011 +0200
@@ -5,6 +5,7 @@
 \usepackage{typearea}
 \usepackage{algorithm}
 \usepackage{algorithmic}
+\usepackage{multicol}
 %\usepackage{fullpage}
 %\usepackage[T1]{fontenc}
 %\usepackage{arev}
@@ -23,7 +24,7 @@
 }
 \date{\textsc{\hfill}}
 
-\theoremstyle{definition} %plain, definition, remark
+\theoremstyle{definition} %plain, definition, remark, proposition, proof, corrolary
 \newtheorem*{def:finite words}{Finite words}
 \newtheorem*{def:infinite words}{Infinite words}
 \newtheorem*{def:regular languages}{Regular languages}
@@ -35,7 +36,9 @@
 \newtheorem*{def:automata acceptance}{Acceptance}
 \newtheorem*{def:vocabulary}{Vocabulary}
 
+\theoremstyle{proposition}
 \newtheorem{prop:vocabulary sat}{Proposition}
+
 \begin{document}
 
 \maketitle
@@ -94,15 +97,18 @@
 
 \begin{def:regular languages}
 The class of regular languages is defined recursively over an alphabet $\Sigma$:
+\begin{multicols}{2}
 \begin{itemize}
 \item $\emptyset$ is regular
 \item $\{\varepsilon\}$ is regular
 \item $\forall_{a \in \Sigma}:\{a\}$ is regular
 \end{itemize}
+\end{multicols}
 \end{def:regular languages}
 
 \begin{def:regular languages closure}
 Let $L_{R_1}, L_{R_2} \in \Sigma^*$ be regular. The class of regular languages is closed under following operations:
+\begin{multicols}{2}
 \begin{itemize}
 \item $L_{R_1}^*$
 \item $L_{R_1} \circ L_{R_2}$
@@ -110,6 +116,7 @@
 \item $L_{R_1} \cap L_{R_2}$
 \item $\overline{L}_{R_1}$ and therefore $L_{R_1} - L_{R_2}$
 \end{itemize}
+\end{multicols}
 \end{def:regular languages closure}
 
 \begin{def:infinite words}
@@ -131,7 +138,7 @@
 
 \section{B\"uchi automata}
 \begin{def:buechi automata}
-A non-deterministic B\"uchi automaton is a tuple $A = (\Sigma, S, S_0, \Delta, F)$, where $\Sigma$ is a finite non-empty \emph{alphabet}, $S$ is a finite non-empty set of \emph{states}, $S_0 \subseteq S$ is the set of \emph{initial states}, $F \subseteq S$ is the set of \emph{accepting states} and $\Delta: S \times \Sigma \times S$ is a \emph{transition relation}. When suitable we will use the arrow notation for the transitions, where $s \xrightarrow{a} s' \iff (s, a, s') \in \Delta$.
+A non-deterministic B\"uchi automaton is a tuple $A = (\Sigma, S, S_0, \Delta, F)$, where $\Sigma$ is a finite non-empty \emph{alphabet}, $S$ is a finite non-empty set of \emph{states}, $S_0 \subseteq S$ is the set of \emph{initial states}, $F \subseteq S$ is the set of \emph{accepting states} and $\Delta: S \times \Sigma \times S$ is a \emph{transition relation}. When suitable we will use the arrow notation for the transitions, where $s \xrightarrow{a} s'$ iff $(s, a, s') \in \Delta$.
 
 A deterministic B\"uchi automaton is a specialisation where the \emph{transition relation} $\Delta$ is a \emph{transition function} $\delta: S \times \Sigma \to S$ and the set $S_0$ of \emph{initial states} contains only a single state $s_0$.
 
@@ -145,7 +152,7 @@
 \begin{def:automata acceptance}
 Let $A = (\Sigma, S, S_0, \Delta, F)$ be an automaton and let $\rho$ be a run of $A$, we define $inf(\rho) = \{s \in S \mid \exists^\omega{n \in \mathbb{N}_0}: \rho(n) = s\}$, where $\exists^\omega$ denotes the existential quantifier for infinitely many occurances, i.e., $s$ occurs infinitely often in $\rho$.
 
-The run $\rho$ is \emph{accepting}, iff $inf(\rho) \cap F \neq \emptyset$, i.e., there exists an \emph{accepting state} which occurs infinitely often in the run $\rho$. The automaton $A$ \emph{accepts} an input word $w$, iff there exists a run $\rho$ of $A$ on $w$, such that $\rho$ is \emph{accepting}. The language $L_\omega(A)$ recognised by automaton $A$ is the set of all infinite words accepted by $A$.
+The run $\rho$ is \emph{accepting} iff $inf(\rho) \cap F \neq \emptyset$, i.e., there exists an \emph{accepting state} which occurs infinitely often in the run $\rho$. The automaton $A$ \emph{accepts} an input word $w$, iff there exists a run $\rho$ of $A$ on $w$, such that $\rho$ is \emph{accepting}. The language $L_\omega(A)$ recognised by automaton $A$ is the set of all infinite words accepted by $A$.
 \end{def:automata acceptance}
 
 \section{Linear temporal logic}
@@ -159,7 +166,7 @@
 LTL is interpreted over \emph{computation paths}, where a computation corrensponds to a model over a \emph{Kripke-frame} constructed by the order of natural numbers.
 
 \subsection*{Semantics}
-A \emph{model} is a function $M: \mathbb{N}_0 \to 2^P$ over \emph{frame} $F$. The frame constitutes a linear order over $\mathbb{N}_0$, which corresponds to the linear temporal progression from \emph{now/before} to \emph{later}. Therefore $M(i)$ assigns a set of \emph{positive atomic propositions} to each state of time instant $i$. Intuitively we say $p \in P$ is \emph{true} at time instant $i$, iff $p \in M(i)$.
+A \emph{model} is a function $M: \mathbb{N}_0 \to 2^P$ over \emph{frame} $F$. The frame constitutes a linear order over $\mathbb{N}_0$, which corresponds to the linear progression of time from the \emph{present/past} into the \emph{future}. Therefore $M(i)$ assigns a set of \emph{positive atomic propositions} to each state of time instant $i$. Intuitively we say $p \in P$ is \emph{true} at time instant $i$ iff $p \in M(i)$.
 
 A model $M$ \emph{satisfies} an LTL-formula $\varphi$ at time instant $i$ is denoted by $M,i \models \varphi$. Satisfaction of a formula $\varphi$ is defined inductively over the structure of $\varphi$:
 \begin{itemize}
@@ -172,6 +179,7 @@
 
 \begin{def:vocabulary}
 Let $\varphi$ be a LTL-formula over atomic propositions $P$, we define the \emph{vocabulary} $Voc(\varphi)$ of $\varphi$ inductively:
+\begin{multicols}{2}
 \begin{itemize}
 \item $Voc(p) = \{p\}$ for $p \in P$
 \item $Voc(\neg \varphi) = Voc(\varphi)$
@@ -179,16 +187,33 @@
 \item $Voc(X \varphi) = Voc(\varphi)$
 \item $Voc(\varphi U \psi) = Voc(\varphi) \cup Voc(\psi)$
 \end{itemize}
+\end{multicols}
+
 Let $M$ be a model and $\varphi$ a LTL-formula, we define model $M_{Voc(\varphi)}$:
-\[\forall{i \in \mathbb{N}}: M_{Voc(\varphi)} = M(i) \cap Voc(\varphi)\]
+\[\forall{i \in \mathbb{N}_0}: M_{Voc(\varphi)} = M(i) \cap Voc(\varphi)\]
 \end{def:vocabulary}
 
 \begin{prop:vocabulary sat}
 Let $M$ be a model and $\varphi$ a LTL-formula, then following holds:
-\[\forall{i \in \mathbb{N}}: M,i \models \varphi \iff M_{Voc(\varphi)},i \models \varphi\] 
+\[\forall{i \in \mathbb{N}_0}: M,i \models \varphi \iff M_{Voc(\varphi)},i \models \varphi\] 
 \end{prop:vocabulary sat}
 
+\subsection*{Derived connectives}
+For a more convenient description of system specifications we present some derived symbols to be used in LTL-formulae. At first we introduce the notion of \emph{truth} and \emph{falsity} using constants $\top$ and $\bot$. Then we expand our set of connectives with the Boolean \emph{and}, \emph{implication} and \emph{equivalence}. And at last we derive the commonly used modal operators \emph{eventually} and \emph{henceforth}. Let $\varphi$ and $\psi$ be $L_{LTL}(P)$-formulae:
+\begin{multicols}{2}
+\begin{itemize}
+\item $\top \equiv p \lor \neg p$ for $p \in P$
+\item $\bot \equiv \neg \top$
+\item $\varphi \land \psi \equiv \neg (\neg \varphi \lor \neg \psi)$
+\item $\varphi \rightarrow \psi \equiv \neg \varphi \lor \psi$
+\item $\varphi \leftrightarrow \psi \equiv (\varphi \rightarrow \psi) \land (\psi \rightarrow \varphi)$
+\item $\Diamond \varphi \equiv \top U \varphi$
+\item $\Box \varphi \equiv \neg \Diamond \neg \varphi$
+\end{itemize}
+\end{multicols}
+
 \section{Model checking}
+
 \begin{thebibliography}{99}
 \bibitem{ref:ltl&büchi} 
 \uppercase{M{\footnotesize adhavan} M{\footnotesize ukund}.}