1.1 --- a/paper/src/paper.tex	Tue Jul 12 13:43:09 2011 +0200
     1.2 +++ b/paper/src/paper.tex	Tue Jul 12 16:06:35 2011 +0200
     1.3 @@ -102,7 +102,7 @@
     1.4  
     1.5  The fifth section interweaves automata theory and modal logics for the formalisation of the automata constructions, i.e., we construct automata depicting the program design and the specified properties. Based on this constructions, we apply the methods presented in the model checking section. The last section is a short excursion into the practical considerations of automated verification. For a successful application of automated verification, we consider ways of reducing the complexity of the automata-theoretic approach.
     1.6  
     1.7 -The formal frame of this text is mostly based on Madhavan Mukund's \cite{ref:ltl&büchi} and Moshe Y. Vardi's \cite{ref:handbook} works. We will conclude this paper with a discussion of \cite{ref:ltl&büchi}.
     1.8 +The formal frame of this text is mostly based on Madhavan Mukund's \cite{ref:ltl&büchi} and Moshe Y. Vardi's \cite{ref:handbook} work. We will conclude this paper with a discussion of \cite{ref:ltl&büchi}.
     1.9  
    1.10  \section{$\omega$-regular languages}
    1.11  For the formalisation of non-terminating, reactive systems, we need to get familiar with the concept of infinity. When a system is persistently active, the conceptual model of its input becomes an infinite structure, and likewise the description of its computational path. We want to settle this infinite structures within a formal corset.