1.1 --- a/paper/src/paper.tex	Fri May 27 22:52:44 2011 +0200
     1.2 +++ b/paper/src/paper.tex	Sat May 28 00:48:18 2011 +0200
     1.3 @@ -1,13 +1,25 @@
     1.4 -\documentclass{article}
     1.5 -\usepackage{amsmath}
     1.6 -\title{Verification of Reactive Systems}
     1.7 -\author{Eugen Sawin\\ 
     1.8 -  Foundations of Artificial Intelligence\\ 
     1.9 -  Department of Computer Science\\ 
    1.10 -  University of Freiburg}
    1.11 +\documentclass[10pt, a4paper, onecolumn]{article}
    1.12 +%\usepackage[top=0cm, bottom=0cm, left=0cm, right=0cm]{geometry}
    1.13 +%\usepackage[ngerman]{babel}
    1.14 +\usepackage{graphicx}
    1.15 +%\usepackage[latin1]{inputenc}
    1.16 +\usepackage{amsmath, amsthm, amssymb}
    1.17 +\usepackage{typearea}
    1.18 +\usepackage{algorithm}
    1.19 +\usepackage{algorithmic}
    1.20 +%\pagestyle{empty}
    1.21 +
    1.22 +\renewcommand{\familydefault}{\sfdefault}
    1.23 +\title{\textbf{Verification of Reactive Systems}}
    1.24 +\author{Eugen Sawin\\   
    1.25 +  University of Freiburg, Germany\\\\
    1.26 +  \texttt{sawine@informatik.uni-freiburg.de}}
    1.27  \date{May, 2011}
    1.28  \begin{document}
    1.29  \maketitle
    1.30 +
    1.31 +%\itshape
    1.32 +%\renewcommand\abstractname{Abstract} 
    1.33  \begin{abstract}
    1.34  Over the past two decades, temporal logic has become a very basic tool for spec-
    1.35  ifying properties of reactive systems. For finite-state systems, it is possible to use
    1.36 @@ -18,13 +30,53 @@
    1.37  techniques used for this automated verification. We also describe some recent space-
    1.38  efficient techniques which work on-the-fly.
    1.39  \end{abstract}
    1.40 +%\normalfont
    1.41 +
    1.42 +\section{Introduction}
    1.43 +Program verification is a fundamental area of study in computer science. The broad goal
    1.44 +is to verify whether a program is “correct”—i.e., whether the implementation of a program
    1.45 +meets its specification. This is, in general, too ambitious a goal and several assumptions
    1.46 +have to be made in order to render the problem tractable. In these lectures, we will focus
    1.47 +on the verification of finite-state reactive programs. For specifying properties of programs,
    1.48 +we use linear time temporal logic.
    1.49 +
    1.50 +What is a reactive program? The general pattern along which a conventional program
    1.51 +executes is the following: it accepts an input, performs some computation, and yields an
    1.52 +output. Thus, such a program can be viewed as an abstract function from an input domain
    1.53 +to an output domain whose behaviour consists of a transformation from initial states to
    1.54 +final states.
    1.55 +
    1.56 +In contrast, a reactive program is not expected to terminate. As the name suggests, such
    1.57 +systems “react” to their environment on a continuous basis, responding appropriately to
    1.58 +each input. Examples of such systems include operating systems, schedulers, discrete-event
    1.59 +controllers etc. (Often, reactive systems are complex distributed programs, so concurrency
    1.60 +also has to be taken into account. We will not stress on this aspect in these lectures—we
    1.61 +take the view that a run of a distributed system can be represented as a sequence, by
    1.62 +arbitrarily interleaving concurrent actions.)
    1.63 +
    1.64 +To specify the behaviour of a reactive system, we need a mechanism for talking about
    1.65 +the way the system evolves along potentially infinite computations. Temporal logic 
    1.66 +has become a well-established formalism for this purpose. Many varieties of temporal logic
    1.67 +have been defined in the past twenty years—we focus on propositional linear time temporal
    1.68 +logic (LTL).
    1.69 +
    1.70 +There is an intimate connection between models of LTL formulas and languages of
    1.71 +infinite words—the models of an LTL formula constitute an ω-regular language over an
    1.72 +appropriate alphabet. As a result, the satisfiability problem for LTL reduces to checking
    1.73 +for emptiness of ω-regular languages. This connection was first explicitly pointed out in.
    1.74 +
    1.75  \section{$\omega$-regular Languages}
    1.76  \section{Linear Temporal Logic}
    1.77  \section{B\"uchi Automata}
    1.78 +Automata are good.
    1.79  \section{Model Checking}
    1.80  \begin{thebibliography}{99}
    1.81 -\bibitem{ref:ltl&büchi} Madhavan Mukund {\em Linear-Time Temporal Logic and B\"uchi Automata}
    1.82 -\bibitem{ref:handbook} Patrick Blackburn, Frank Wolter and Johan Van Benthem {\em Handbook of Modal Logic (Studies in Logic and Practical Reasoning)}
    1.83 +\bibitem{ref:ltl&büchi} Madhavan Mukund: {\em Linear-Time Temporal Logic and B\"uchi Automata}.
    1.84 +Winter School on Logic and Computer Science, Indian Statistical Institute, Calcutta, 1997.
    1.85  
    1.86 +\bibitem{ref:handbook} 
    1.87 +Patrick Blackburn, Frank Wolter and Johan Van Benthem: 
    1.88 +{\em Handbook of Modal Logic (Studies in Logic and Practical Reasoning)}.
    1.89 +Elsevier, Amsterdam, 3rd Edition, 2007.
    1.90  \end{thebibliography}
    1.91  \end{document}