\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

techniques based on B\"uchi automata to verify if a system meets its specifications.

This is done by synthesizing an automaton which generates all possible models of

the given specification and then verifying if the given system refines this most gen-

eral automaton. In these notes, we present a self-contained introduction to the basic

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}.

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)}.

3rd Edition, Elsevier, Amsterdam, 2007.

\end{thebibliography}

\end{document}