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