# HG changeset patch # User Eugen Sawin # Date 1310479595 -7200 # Node ID 4db52c868b94d30af649eea5fc82410d24d4be6c # Parent 7b80e38fb6e8007742fee6219fd13a572ef2d4b3 Some free text. diff -r 7b80e38fb6e8 -r 4db52c868b94 paper/src/paper.tex --- a/paper/src/paper.tex Tue Jul 12 13:43:09 2011 +0200 +++ b/paper/src/paper.tex Tue Jul 12 16:06:35 2011 +0200 @@ -102,7 +102,7 @@ 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. -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}. +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}. \section{$\omega$-regular languages} 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.