1.1 --- a/paper/src/paper.tex	Thu Jun 30 20:45:45 2011 +0200
     1.2 +++ b/paper/src/paper.tex	Fri Jul 08 14:53:15 2011 +0200
     1.3 @@ -66,14 +66,7 @@
     1.4  %\itshape
     1.5  %\renewcommand\abstractname{Abstract} 
     1.6  \begin{abstract}
     1.7 -Over the past two decades, temporal logic has become a very basic tool for spec-
     1.8 -ifying properties of reactive systems. For finite-state systems, it is possible to use
     1.9 -techniques based on B\"uchi automata to verify if a system meets its specifications.
    1.10 -This is done by synthesizing an automaton which generates all possible models of
    1.11 -the given specification and then verifying if the given system refines this most gen-
    1.12 -eral automaton. In these notes, we present a self-contained introduction to the basic
    1.13 -techniques used for this automated verification. We also describe some recent space-
    1.14 -efficient techniques which work on-the-fly.
    1.15 +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 is an introductory to the synthesisation techniques of automata and space-efficient on-the-fly verification methods for reactive systems. 
    1.16  \end{abstract}
    1.17  %\normalfont
    1.18  \newpage
    1.19 @@ -313,7 +306,7 @@
    1.20  \item $S = \mathbb{AT_\varphi}$
    1.21  \item $S_0 = \{A \in \mathbb{AT_\varphi} \mid \varphi \in A\}$
    1.22  %\item $(A, P, B) \in \Delta$ for $A, B \in \mathbb{AT_\varphi}$ and $P = A \cap Voc(\varphi) \iff (X \psi \in A \iff \psi \in B)$
    1.23 -\item $\Delta = \{(A, P, \mathbb{B}) \mid A, \mathbb{B} \in \mathbb{AT_\varphi}, P = A \cap Voc(\varphi), X \psi \in A \iff \psi \in \mathbb{B}\}$
    1.24 +\item $\Delta = \{(A, P, B) \mid A, B \in \mathbb{AT_\varphi}, P = A \cap Voc(\varphi), X \psi \in A \iff \psi \in B\}$
    1.25  %\item $\forall{i \in \N, i < k = |\mathbb{U}_{FL(\varphi)}|}: F_i = \{A \in \mathbb{AT}_\varphi \mid \psi U \chi \notin A$ or $\chi \in A\}$
    1.26  \item $F_i = \{A \in \mathbb{AT}_\varphi \mid \psi U \chi = \mathbb{U}_{\varphi_i}, \psi U \chi \notin A$ or $\chi \in A\}$ and therefore $k = |\mathbb{U}_{\varphi}|$
    1.27  %Let $A, B \in \mathbb{AT}$ and $P \subseteq Voc(\varphi)$. Then $(A, P, B) \in \Delta$ iff the following holds: