1.1 --- a/paper/src/paper.tex	Tue Jul 12 16:06:35 2011 +0200
     1.2 +++ b/paper/src/paper.tex	Tue Jul 12 17:39:08 2011 +0200
     1.3 @@ -94,7 +94,7 @@
     1.4  
     1.5  Compared to hardware design, the highly dynamic properties of software components confront us with another state space explosion. Concurrent system designs increase the complexity of verification by some orders of magnitude; and concurrent applications have started to dominate recent software solutions, because we are closing the physical limits for single-core processor frequencies.
     1.6  
     1.7 -Again, the industry is facing a \emph{validation crisis} \cite{ref:automated verification} and formal verification methods are in high demand. Deductive, computer-supported verification techniques are an interesting digression, but may not be applicable in the validation of software programs of high complexity. Theories for algorithmic verification have existed for decades and recent successful applications have demonstrated their practical value.
     1.8 +Again, the industry is facing a \emph{validation crisis} \cite{ref:automated verification} and formal verification methods are in high demand. Deductive, computer-supported verification techniques are an interesting digression, but may not be applicable in the validation of software systems of high complexity. Theories for algorithmic verification have existed for decades and recent successful applications have demonstrated their practical value.
     1.9  
    1.10  In this text, we provide an introduction to formal verification by means of algorithmic methods. Such an algorithmic approach is the base for automated verification procedures. We will concentrate on the validation of reactive programs, without any loss of the general applicability of the presented methods. Reactive systems are, in contrast to terminating programs, continuous processes. Once initiated, a reactive system persists in an active state, where it reacts to concurrent inputs with appropriate actions. Examples of reactive systems are monitoring processes, schedulers and even whole operating systems.
    1.11  
    1.12 @@ -173,14 +173,16 @@
    1.13  
    1.14  The run $\rho$ is \emph{accepting} iff $inf(\rho) \cap F \neq \emptyset$, i.e., there exists an \emph{accepting state} which occurs infinitely often in the run $\rho$. The automaton $\A$ \emph{accepts} an input word $w$, iff there exists a run $\rho$ of $\A$ on $w$, such that $\rho$ is \emph{accepting}. 
    1.15  
    1.16 -The language $L_\omega(\A)$ recognised by automaton $\A$ is the set of all infinite words accepted by $\A$. A language $L$ is \emph{B\"uchi-recognisable} iff there is an automaton $\A$ with $L = L_\omega(\A)$.
    1.17 +The language $L_\omega(\A)$ recognised by automaton $\A$ is the set of all infinite words accepted by $\A$. A language $L$ is \emph{B\"uchi-recognisable} iff there is an automaton $\A$ with $L = L_\omega(\A)$. The class of B\"uchi-recognisable languages corresponds to the class of $\omega$-regular languages.
    1.18  \end{def:automata acceptance}
    1.19  
    1.20 -Given all legal computations of an automaton, we have defined the acceptance condition. A computation is accepting, if it passes through an accepting state infinitely times. Since the set of states $S$ is finite, there must be a state $s \in S$, which occurs infinitely often within an infinite run; but it is not necessary, that $s$ is an accepting state, $F$ can be even an empty set.
    1.21 +Given all legal computations of an automaton, we have defined the acceptance condition. A computation is accepting, if it passes through an accepting state infinitely times. Since the set of states $S$ is finite, there must be a state $s \in S$, which occurs infinitely often within an infinite run; but it is not necessary, that $s$ is an accepting state; notice that $F$ can be an empty set.
    1.22  
    1.23  \subsection{Generalised B\"uchi automata}
    1.24 +In the following two sections, we will introduce the modal logic used for the specification of system properties and automata construction on such specifications. To provide a more convenient link between linear temporal logic and B\"uchi automata, we introduce a slightly different formalisation of automata with an extended acceptance condition.
    1.25 +
    1.26  \begin{def:general automata}
    1.27 -A \emph{generalised B\"uchi automaton} is a tuple $\A = (\Sigma, S, S_0, \Delta, \{F_i\})$ for $i \in \N$, where the \emph{acceppting states} $F_i$ are composed within a finite set with $F_i \subseteq S$.
    1.28 +A \emph{generalised B\"uchi automaton} is a tuple $\A = (\Sigma, S, S_0, \Delta, \{F_i\}_{i < k})$ for $i \in \N$, where the \emph{acceppting states} $F_i$ are composed within a finite set with $F_i \subseteq S$.
    1.29  \end{def:general automata}
    1.30  
    1.31  \begin{def:general acceptance}
    1.32 @@ -191,9 +193,13 @@
    1.33  Let $\A = (\Sigma, S, S_0, \Delta, \{F_i\}_{i < k})$ be a \emph{generalised automaton} and let $\A_i = (\Sigma, S, S_0, \Delta, F_i)$ be \emph{non-deterministic automata}, then following equivalance condition holds:
    1.34  \[L_\omega(\A) = \bigcap_{i < k} L_\omega(\A_i)\]
    1.35  \end{prop:general equiv}
    1.36 -\noindent Intuitively follows the equivalance of the language recognition abilities of general and non-deterministic B\"uchi automata.
    1.37 +\noindent The equivalance of the language recognition abilities of general and non-deterministic B\"uchi automata follows intuitively.
    1.38  
    1.39  \section{Linear temporal logic}
    1.40 +Nothing escapes time, but time has successfully escaped its formalisation until the rise of the modal logics in the second half of the 20th century \cite{ref:handbook}. All arts and sciences interpret time in some way; where historians prefer the past tense, do science-fiction novels live in the future. Physics knows many time arrows, one of which constitutes the thermodynamic arrow of time, which happens to be the one we perceive by remembering the past and not the future. We compensate our inability to control the direction of time, by the use of rigorous language constructs when reasoning about temporal events.
    1.41 +
    1.42 +When natural language fails in providing unambiguousness, we have to resort to formal languages. To handle time, we use \emph{propositional logic} as the base and extend it by some more or less modal connectives.
    1.43 +
    1.44  \subsection{Syntax}
    1.45  Let $\Prop$ be the countable set of \emph{atomic propositions}. The \emph{alphabet} of the language $L_{LTL}(\Prop)$ is $\Prop \cup \{\neg, \lor, \X, \U\}$. We define the $L_{LTL}(\Prop)$-\emph{formulae} $\varphi$ using following productions:
    1.46  \[\varphi ::= p \in \Prop \,|\, \neg \varphi \,|\, \varphi \lor \varphi \,|\, \X \varphi \,|\, \varphi \U \varphi\]
    1.47 @@ -530,6 +536,6 @@
    1.48  \uppercase{P{\footnotesize atrick} B{\footnotesize lackburn}, 
    1.49  F{\footnotesize rank} W{\footnotesize olter and} J{\footnotesize ohan van} B{\footnotesize enthem}.}
    1.50  {\em Handbook of Modal Logic (Studies in Logic and Practical Reasoning)}.
    1.51 -3rd Edition, Elsevier, Amsterdam, P. 975-989, 2007.
    1.52 +3rd Edition, Elsevier, Amsterdam, Chapter 11 P. 655-720 and Chapter 17 P. 975-989, 2007.
    1.53  \end{thebibliography}
    1.54  \end{document}