# HG changeset patch
# User Eugen Sawin <sawine@me73.com>
# Date 1310251362 -7200
# Node ID 7a38b7f20ebce1e94d2dd0105e1ffcfae561c173
# Parent  e9bb32d8ceccac442a49c2a26e4f24c376313df8
New abstract.

diff -r e9bb32d8cecc -r 7a38b7f20ebc paper/src/paper.tex
--- a/paper/src/paper.tex	Sun Jul 10 00:35:46 2011 +0200
+++ b/paper/src/paper.tex	Sun Jul 10 00:42:42 2011 +0200
@@ -78,7 +78,7 @@
 %\itshape
 %\renewcommand\abstractname{Abstract} 
 \begin{abstract}
-Algorithmic verification is a successful application of automated temporal reasoning based on automata-theoretic model checking. We use the power of modal logics for the characterisation of computational properties. The verification of reactive systems provides a correctness proof for the program design with respect to such properties. The methods used are a composition of automata theory, graph theory and modal logics. This introductory text describes such automata theoretic constructions and a space-efficient on-the-fly verification method for reactive systems.
+Algorithmic verification is a successful application of automated temporal reasoning based on automata-theoretic model checking. We use the power of modal logics to specify computational properties. The verification of reactive systems provides a correctness proof for the program design with respect to such properties. The methods used are a composition of automata theory, graph theory and modal logics. This text is an introduction to such automata theoretic constructions and space-efficient on-the-fly verification methods for reactive systems.
 %Algorithmic verification of reactive systems is based on automata-theoretic model checking. Linear temporal logic accommodates the capability for the characterisation of program specifications. For formulae composed in linear temporal logic, it is possible to construct B\"uchi automata constituting the model space of the specification. The verification of reactive systems is composed of such constructions and intersections of the program and specification automata. This paper provides an introduction to the construction techniques of such automata and space-efficient on-the-fly verification methods for reactive systems. 
 \end{abstract}
 %\normalfont