Initial.
authorEugen Sawin <sawine@me73.com>
Fri, 27 May 2011 20:54:16 +0200
changeset 0a18cfd9a0c87
child 1 f8e63d191537
Initial.
paper/makefile
paper/src/paper.tex
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/paper/makefile	Fri May 27 20:54:16 2011 +0200
     1.3 @@ -0,0 +1,5 @@
     1.4 +paper: 
     1.5 +	pdflatex -output-directory=out -aux-directory=out src/paper.tex
     1.6 +
     1.7 +clean:
     1.8 +	rm -rf out/*
     1.9 \ No newline at end of file
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/paper/src/paper.tex	Fri May 27 20:54:16 2011 +0200
     2.3 @@ -0,0 +1,30 @@
     2.4 +\documentclass{article}
     2.5 +\usepackage{amsmath}
     2.6 +\title{Verification of Reactive Systems}
     2.7 +\author{Eugen Sawin\\ 
     2.8 +  Foundations of Artificial Intelligence\\ 
     2.9 +  Department of Computer Science\\ 
    2.10 +  University of Freiburg}
    2.11 +\date{\today}
    2.12 +\begin{document}
    2.13 +\maketitle
    2.14 +\begin{abstract}
    2.15 +Over the past two decades, temporal logic has become a very basic tool for spec-
    2.16 +ifying properties of reactive systems. For finite-state systems, it is possible to use
    2.17 +techniques based on B\"uchi automata to verify if a system meets its specifications.
    2.18 +This is done by synthesizing an automaton which generates all possible models of
    2.19 +the given specification and then verifying if the given system refines this most gen-
    2.20 +eral automaton. In these notes, we present a self-contained introduction to the basic
    2.21 +techniques used for this automated verification. We also describe some recent space-
    2.22 +efficient techniques which work on-the-fly.
    2.23 +\end{abstract}
    2.24 +\section{$\omega$-regular Languages}
    2.25 +\section{Linear Temporal Logic}
    2.26 +\section{B\"uchi Automata}
    2.27 +\section{Model Checking}
    2.28 +\begin{thebibliography}{99}
    2.29 +\bibitem{ref:ltl&büchi} Madhavan Mukund {\em Linear-Time Temporal Logic and B\"uchi Automata}
    2.30 +\bibitem{ref:handbook} Patrick Blackburn, Frank Wolter and Johan Van Benthem {\em Handbook of Modal Logic (Studies in Logic and Practical Reasoning)}
    2.31 +
    2.32 +\end{thebibliography}
    2.33 +\end{document}