1.1 --- a/paper/src/paper.tex	Sun May 29 19:36:23 2011 +0200
     1.2 +++ b/paper/src/paper.tex	Tue May 31 03:48:36 2011 +0200
     1.3 @@ -1,4 +1,4 @@
     1.4 -\documentclass[ a4paper, pagesize, DIV=calc, smallheadings]{article}  
     1.5 +\documentclass[a4paper, pagesize, DIV=calc, smallheadings]{article}  
     1.6  \usepackage{graphicx}
     1.7  %\usepackage[latin1]{inputenc}
     1.8  \usepackage{amsmath, amsthm, amssymb}
     1.9 @@ -8,12 +8,25 @@
    1.10  %\usepackage[T1]{fontenc}
    1.11  %\usepackage{arev}
    1.12  
    1.13 -\pagestyle{headings}
    1.14 +%\pagestyle{headings}
    1.15  \renewcommand{\familydefault}{\sfdefault}
    1.16 -\title{\textbf{\uppercase{\Large{A}\large{lgorithmic} \Large{V}\large{erification of} \Large{R}\large{eactive} \Large{S}\large{ystems}}}}
    1.17 -\author{\uppercase{\small{E}\scriptsize{UGEN} \small{S}\scriptsize{AWIN}\\
    1.18 -\textsc{\em{\small{U}\scriptsize{NIVERSITY OF} \small{F}\scriptsize{REIBURG,} \small{G}\scriptsize{ERMANY}}}}}
    1.19 +\title{\uppercase{\textbf{\Large{A}\large{lgorithmic} \Large{V}\large{erification of} \Large{R}\large{eactive} \Large{S}\large{ystems}}\\
    1.20 +\tiny{Draft}
    1.21 +}}
    1.22 +\author{
    1.23 +\uppercase{{\small{E}\scriptsize{UGEN} \small{S}\scriptsize{AWIN}}\\
    1.24 +{\em \small{U}\scriptsize{NIVERSITY OF} \small{F}\scriptsize{REIBURG}}\\
    1.25 +%{\em \small{C}\scriptsize{omputer} \small{S}\scriptsize{cience} \small{D}\scriptsize{epartment}}\\
    1.26 +{\em \small{G}\scriptsize{ERMANY}}}\\
    1.27 +%\texttt{\footnotesize{sawine@informatik.uni-freiburg.de}}
    1.28 +}
    1.29  \date{\textsc{\hfill}}
    1.30 +
    1.31 +\theoremstyle{definition} %plain, definition, remark
    1.32 +\newtheorem*{def:finite words}{Finite words}
    1.33 +\newtheorem*{def:infinite words}{Infinite words}
    1.34 +\newtheorem*{def:omega regular languages}{$\omega$-regular languages}
    1.35 +
    1.36  \begin{document}
    1.37  
    1.38  \maketitle
    1.39 @@ -66,6 +79,24 @@
    1.40  for emptiness of ω-regular languages. This connection was first explicitly pointed out in.
    1.41  
    1.42  \section{$\omega$-regular Languages}
    1.43 +\begin{def:finite words}
    1.44 +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.45 +\end{def:finite words}
    1.46 +
    1.47 +\begin{def:infinite words}
    1.48 +$\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.49 +\end{def:infinite words}
    1.50 +
    1.51 +\begin{def:omega regular languages}
    1.52 +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.53 +\begin{itemize}
    1.54 +\item $L = L_R^\omega$
    1.55 +\item $L = L_R \circ L_{\omega_1}$
    1.56 +\item $L = L_{\omega_1} \cup L_{\omega_2}$
    1.57 +\end{itemize}
    1.58 +\end{def:omega regular languages}
    1.59 +
    1.60 +
    1.61  \section{B\"uchi Automata}
    1.62  Automata are good.
    1.63  \section{Linear Temporal Logic}
    1.64 @@ -82,5 +113,13 @@
    1.65  F{\footnotesize rank} W{\footnotesize olter and} J{\footnotesize ohan van} B{\footnotesize enthem}.}
    1.66  {\em Handbook of Modal Logic (Studies in Logic and Practical Reasoning)}.
    1.67  3rd Edition, Elsevier, Amsterdam, 2007.
    1.68 +
    1.69 +\bibitem{ref:infpaths}
    1.70 +\uppercase{P{\footnotesize ierre} W{\footnotesize olper}, 
    1.71 +M{\footnotesize oshe} Y. V{\footnotesize ardi and}
    1.72 +A. P{\footnotesize rasad} S{\footnotesize istla}.}
    1.73 +{\em Reasoning about Infinite Computation Paths}.
    1.74 +In Proceedings of the 24th IEEE FOCS, 1983.
    1.75 +
    1.76  \end{thebibliography}
    1.77  \end{document}