diff -r f8e63d191537 -r eb8dd8159786 paper/src/paper.tex
--- a/paper/src/paper.tex	Fri May 27 22:52:44 2011 +0200
+++ b/paper/src/paper.tex	Sat May 28 00:48:18 2011 +0200
@@ -1,13 +1,25 @@
-\documentclass{article}
-\usepackage{amsmath}
-\title{Verification of Reactive Systems}
-\author{Eugen Sawin\\ 
-  Foundations of Artificial Intelligence\\ 
-  Department of Computer Science\\ 
-  University of Freiburg}
+\documentclass[10pt, a4paper, onecolumn]{article}
+%\usepackage[top=0cm, bottom=0cm, left=0cm, right=0cm]{geometry}
+%\usepackage[ngerman]{babel}
+\usepackage{graphicx}
+%\usepackage[latin1]{inputenc}
+\usepackage{amsmath, amsthm, amssymb}
+\usepackage{typearea}
+\usepackage{algorithm}
+\usepackage{algorithmic}
+%\pagestyle{empty}
+
+\renewcommand{\familydefault}{\sfdefault}
+\title{\textbf{Verification of Reactive Systems}}
+\author{Eugen Sawin\\   
+  University of Freiburg, Germany\\\\
+  \texttt{sawine@informatik.uni-freiburg.de}}
 \date{May, 2011}
 \begin{document}
 \maketitle
+
+%\itshape
+%\renewcommand\abstractname{Abstract} 
 \begin{abstract}
 Over the past two decades, temporal logic has become a very basic tool for spec-
 ifying properties of reactive systems. For finite-state systems, it is possible to use
@@ -18,13 +30,53 @@
 techniques used for this automated verification. We also describe some recent space-
 efficient techniques which work on-the-fly.
 \end{abstract}
+%\normalfont
+
+\section{Introduction}
+Program verification is a fundamental area of study in computer science. The broad goal
+is to verify whether a program is “correct”—i.e., whether the implementation of a program
+meets its specification. This is, in general, too ambitious a goal and several assumptions
+have to be made in order to render the problem tractable. In these lectures, we will focus
+on the verification of finite-state reactive programs. For specifying properties of programs,
+we use linear time temporal logic.
+
+What is a reactive program? The general pattern along which a conventional program
+executes is the following: it accepts an input, performs some computation, and yields an
+output. Thus, such a program can be viewed as an abstract function from an input domain
+to an output domain whose behaviour consists of a transformation from initial states to
+final states.
+
+In contrast, a reactive program is not expected to terminate. As the name suggests, such
+systems “react” to their environment on a continuous basis, responding appropriately to
+each input. Examples of such systems include operating systems, schedulers, discrete-event
+controllers etc. (Often, reactive systems are complex distributed programs, so concurrency
+also has to be taken into account. We will not stress on this aspect in these lectures—we
+take the view that a run of a distributed system can be represented as a sequence, by
+arbitrarily interleaving concurrent actions.)
+
+To specify the behaviour of a reactive system, we need a mechanism for talking about
+the way the system evolves along potentially infinite computations. Temporal logic 
+has become a well-established formalism for this purpose. Many varieties of temporal logic
+have been defined in the past twenty years—we focus on propositional linear time temporal
+logic (LTL).
+
+There is an intimate connection between models of LTL formulas and languages of
+infinite words—the models of an LTL formula constitute an ω-regular language over an
+appropriate alphabet. As a result, the satisfiability problem for LTL reduces to checking
+for emptiness of ω-regular languages. This connection was first explicitly pointed out in.
+
 \section{$\omega$-regular Languages}
 \section{Linear Temporal Logic}
 \section{B\"uchi Automata}
+Automata are good.
 \section{Model Checking}
 \begin{thebibliography}{99}
-\bibitem{ref:ltl&büchi} Madhavan Mukund {\em Linear-Time Temporal Logic and B\"uchi Automata}
-\bibitem{ref:handbook} Patrick Blackburn, Frank Wolter and Johan Van Benthem {\em Handbook of Modal Logic (Studies in Logic and Practical Reasoning)}
+\bibitem{ref:ltl&büchi} Madhavan Mukund: {\em Linear-Time Temporal Logic and B\"uchi Automata}.
+Winter School on Logic and Computer Science, Indian Statistical Institute, Calcutta, 1997.
 
+\bibitem{ref:handbook} 
+Patrick Blackburn, Frank Wolter and Johan Van Benthem: 
+{\em Handbook of Modal Logic (Studies in Logic and Practical Reasoning)}.
+Elsevier, Amsterdam, 3rd Edition, 2007.
 \end{thebibliography}
 \end{document}