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