# HG changeset patch
# User Eugen Sawin <sawine@me73.com>
# Date 1306522456 -7200
# Node ID a18cfd9a0c87f4afd6d0a59c0f125345ab033290

Initial.

diff -r 000000000000 -r a18cfd9a0c87 paper/makefile
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/makefile	Fri May 27 20:54:16 2011 +0200
@@ -0,0 +1,5 @@
+paper: 
+	pdflatex -output-directory=out -aux-directory=out src/paper.tex
+
+clean:
+	rm -rf out/*
\ No newline at end of file
diff -r 000000000000 -r a18cfd9a0c87 paper/src/paper.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/src/paper.tex	Fri May 27 20:54:16 2011 +0200
@@ -0,0 +1,30 @@
+\documentclass{article}
+\usepackage{amsmath}
+\title{Verification of Reactive Systems}
+\author{Eugen Sawin\\ 
+  Foundations of Artificial Intelligence\\ 
+  Department of Computer Science\\ 
+  University of Freiburg}
+\date{\today}
+\begin{document}
+\maketitle
+\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}
+\section{$\omega$-regular Languages}
+\section{Linear Temporal Logic}
+\section{B\"uchi Automata}
+\section{Model Checking}
+\begin{thebibliography}{99}
+\bibitem{ref:ltl&büchi} Madhavan Mukund {\em Linear-Time Temporal Logic and B\"uchi Automata}
+\bibitem{ref:handbook} Patrick Blackburn, Frank Wolter and Johan Van Benthem {\em Handbook of Modal Logic (Studies in Logic and Practical Reasoning)}
+
+\end{thebibliography}
+\end{document}