1.1 --- a/paper/src/paper.tex	Sun Jul 10 00:02:03 2011 +0200
     1.2 +++ b/paper/src/paper.tex	Sun Jul 10 00:35:46 2011 +0200
     1.3 @@ -78,7 +78,8 @@
     1.4  %\itshape
     1.5  %\renewcommand\abstractname{Abstract} 
     1.6  \begin{abstract}
     1.7 -The 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 automata and space-efficient on-the-fly verification methods for reactive systems. 
     1.8 +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.
     1.9 +%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. 
    1.10  \end{abstract}
    1.11  %\normalfont
    1.12  \newpage