New abstract.
authorEugen Sawin <sawine@me73.com>
Sun, 10 Jul 2011 00:42:42 +0200
changeset 337a38b7f20ebc
parent 32 e9bb32d8cecc
child 34 2b7dd89210c7
New abstract.
paper/src/paper.tex
     1.1 --- a/paper/src/paper.tex	Sun Jul 10 00:35:46 2011 +0200
     1.2 +++ b/paper/src/paper.tex	Sun Jul 10 00:42:42 2011 +0200
     1.3 @@ -78,7 +78,7 @@
     1.4  %\itshape
     1.5  %\renewcommand\abstractname{Abstract} 
     1.6  \begin{abstract}
     1.7 -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.8 +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.
     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