1.1 --- a/paper/src/paper.tex	Tue May 31 03:48:36 2011 +0200
     1.2 +++ b/paper/src/paper.tex	Wed Jun 01 11:18:05 2011 +0200
     1.3 @@ -25,7 +25,10 @@
     1.4  \theoremstyle{definition} %plain, definition, remark
     1.5  \newtheorem*{def:finite words}{Finite words}
     1.6  \newtheorem*{def:infinite words}{Infinite words}
     1.7 +\newtheorem*{def:regular languages}{Regular languages}
     1.8 +\newtheorem*{def:regular languages closure}{Regular closure}
     1.9  \newtheorem*{def:omega regular languages}{$\omega$-regular languages}
    1.10 +\newtheorem*{def:omega regular languages closure}{$\omega$-regular closure}
    1.11  
    1.12  \begin{document}
    1.13  
    1.14 @@ -78,30 +81,51 @@
    1.15  appropriate alphabet. As a result, the satisfiability problem for LTL reduces to checking
    1.16  for emptiness of ω-regular languages. This connection was first explicitly pointed out in.
    1.17  
    1.18 -\section{$\omega$-regular Languages}
    1.19 +\section{$\omega$-regular languages}
    1.20  \begin{def:finite words}
    1.21 -Let $\Sigma$ be a non-empty set of symbols, the alphabet. $\Sigma^*$ is the set of all \emph{finite} words over $\Sigma$. A \emph{finite} word $w \in \Sigma^*$ is a \emph{finite} sequence $a_0,...,a_{n-1}$ of symbols from alphabet $\Sigma$ with length $n = |w|$. $\varepsilon$ denotes the empty word with length $|\varepsilon| = 0$.
    1.22 +Let $\Sigma$ be a non-empty set of symbols, the alphabet. $\Sigma^*$ is the set of all \emph{finite} words over $\Sigma$. A \emph{finite} word $w \in \Sigma^*$ is a \emph{finite} sequence $v_0...v_{n-1}$ of symbols from alphabet $\Sigma$ with length $n = |w|$. $\varepsilon$ denotes the empty word with length $|\varepsilon| = 0$.
    1.23  \end{def:finite words}
    1.24  
    1.25  \begin{def:infinite words}
    1.26 -$\Sigma^\omega$ is the set of all \emph{infinite} words over $\Sigma$. An \emph{infinite} word $w \in \Sigma^\omega$ is an \emph{infinite} sequence $a_0,...,a_\infty$ with length $\infty$. To address the elements of the infinite sequence $w$, view the word as a function $w : \mathbb{N}_0 \to \Sigma$ with $w(i) = a_i$, thus $w(i)$ denotes the symbol at sequence position $i$ of word $w$.
    1.27 +$\Sigma^\omega$ is the set of all \emph{infinite} words over $\Sigma$. An \emph{infinite} word $w \in \Sigma^\omega$ is an \emph{infinite} sequence $v_0...v_\infty$ with length $\infty$. To address the elements of the infinite sequence $w$, view the word as a function $w : \mathbb{N}_0 \to \Sigma$ with $w(i) = v_i$; thus $w(i)$ denotes the symbol at sequence position $i$ of word $w$, another notation used for $w(i)$ is $w_i$.
    1.28  \end{def:infinite words}
    1.29  
    1.30 +\begin{def:regular languages}
    1.31 +The class of regular languages is defined recursively over an alphabet $\Sigma$:
    1.32 +\begin{itemize}
    1.33 +\item $\emptyset$ is regular
    1.34 +\item $\{\varepsilon\}$ is regular
    1.35 +\item $\forall_{a \in \Sigma}:\{a\}$ is regular
    1.36 +\end{itemize}
    1.37 +\end{def:regular languages}
    1.38 +
    1.39 +\begin{def:regular languages closure}
    1.40 +Let $L_{R_1}, L_{R_2} \in \Sigma$ be regular. The class of regular languages is closed under following operations:
    1.41 +\begin{itemize}
    1.42 +\item $L_{R_1}^*$
    1.43 +\item $L_{R_1} \circ L_{R_2}$
    1.44 +\item $L_{R_1} \cup L_{R_2}$
    1.45 +\end{itemize}
    1.46 +\end{def:regular languages closure}
    1.47 +
    1.48  \begin{def:omega regular languages}
    1.49 -Set $L$ is an $\omega$-language over alphabet $\Sigma$ iff $L \subseteq \Sigma^\omega$. Let $L_R \subseteq \Sigma^*$ be a regular finite language and $L_{\omega_1}, L_{\omega_2} \subseteq \Sigma^\omega$ be $\omega$-regular languages. Set $L$ is an $\omega$-regular language iff $L$ is an $\omega$-language and any of the following conditions hold:
    1.50 -\begin{itemize}
    1.51 -\item $L = L_R^\omega$
    1.52 -\item $L = L_R \circ L_{\omega_1}$
    1.53 -\item $L = L_{\omega_1} \cup L_{\omega_2}$
    1.54 -\end{itemize}
    1.55 +Set $L$ is an $\omega$-language over alphabet $\Sigma$ iff $L \subseteq \Sigma^\omega$. Let $L_R \subseteq \Sigma^*$ be a non-empty regular finite language and $\varepsilon \notin L_R$. A set $L$ is $\omega$-regular iff $L$ is an $\omega$-language and $L = L_R^\omega$.
    1.56  \end{def:omega regular languages}
    1.57  
    1.58 +\begin{def:omega regular languages closure}
    1.59 +Let $L_{\omega_1}, L_{\omega_2} \subseteq \Sigma^\omega$ be $\omega$-regular languages. The class of $\omega$-regular languages is closed under following operations:
    1.60 +\begin{itemize}
    1.61 +\item $L_R \circ L_{\omega_1}$, but \emph{not} $L_{\omega_1} \circ L_R$
    1.62 +\item $L_{\omega_1} \cup L_{\omega_2}$, but only \emph{finitely} many times
    1.63 +\end{itemize}
    1.64 +\end{def:omega regular languages closure}
    1.65  
    1.66 -\section{B\"uchi Automata}
    1.67 +
    1.68 +\section{B\"uchi automata}
    1.69  Automata are good.
    1.70 -\section{Linear Temporal Logic}
    1.71 +\section{Linear temporal logic}
    1.72  
    1.73 -\section{Model Checking}
    1.74 +\section{Model checking}
    1.75  \begin{thebibliography}{99}
    1.76  \bibitem{ref:ltl&büchi} 
    1.77  \uppercase{M{\footnotesize adhavan} M{\footnotesize ukund}.}