1.1 --- a/paper/comments.txt	Fri Jul 08 14:54:53 2011 +0200
     1.2 +++ b/paper/comments.txt	Sat Jul 09 03:48:35 2011 +0200
     1.3 @@ -7,8 +7,9 @@
     1.4  - no introduction to omega-regular languages
     1.5  - short introduction to LTL semantics
     1.6  - no automata complement construction
     1.7 +
     1.8  - error on page 5: there must not be a state g in G along r
     1.9 -
    1.10 +- error on page 12: V : S -> 2^P
    1.11  
    1.12  graphs:
    1.13  

     2.1 --- a/paper/src/paper.tex	Fri Jul 08 14:54:53 2011 +0200
     2.2 +++ b/paper/src/paper.tex	Sat Jul 09 03:48:35 2011 +0200
     2.3 @@ -51,6 +51,7 @@
     2.4  \newtheorem*{def:satisfiability}{Satisfiability}
     2.5  \newtheorem*{def:fs closure}{Fischer-Ladner closure}
     2.6  \newtheorem*{def:atoms}{Atoms}
     2.7 +\newtheorem*{def:rep function}{Representation function}
     2.8  
     2.9  \theoremstyle{plain}
    2.10  \newtheorem{prop:vocabulary sat}{Proposition}[section]
    2.11 @@ -66,7 +67,7 @@
    2.12  %\itshape
    2.13  %\renewcommand\abstractname{Abstract} 
    2.14  \begin{abstract}
    2.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. 
    2.16 +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 provides an introduction to the construction techniques of automata and space-efficient on-the-fly verification methods for reactive systems. 
    2.17  \end{abstract}
    2.18  %\normalfont
    2.19  \newpage
    2.20 @@ -225,7 +226,7 @@
    2.21  \item $\Box \varphi \equiv \neg \Diamond \neg \varphi$
    2.22  \end{itemize}
    2.23  \end{multicols}
    2.24 -From the derivations for operators $\Diamond$, \emph{read diamond}, and $\Box$, \emph{read box}, it follows:
    2.25 +\noindent From the derivations for operators $\Diamond$, \emph{read diamond}, and $\Box$, \emph{read box}, it follows:
    2.26  \begin{multicols}{2}
    2.27  \begin{itemize}
    2.28  \item $\M,i \models \Diamond \varphi$ iff $\exists{k \geq i}: \M,k \models \varphi$
    2.29 @@ -233,15 +234,20 @@
    2.30  \end{itemize}
    2.31  \end{multicols}
    2.32  
    2.33 -With the additional derived connectives we get the following $L_{LTL}(\Prop)$-formulae productions:
    2.34 +\noindent With the additional derived connectives we get the following $L_{LTL}(\Prop)$-formulae productions:
    2.35  \[\varphi ::= p \in \Prop \,|\, \neg \varphi \,|\, \varphi \lor \varphi \,|\, \varphi \land \varphi \,|\, X \varphi \,|\, \varphi U \varphi \,|\, \varphi \rightarrow \varphi \,|\, \varphi \leftrightarrow \varphi \,|\, \Diamond \varphi \,|\, \Box \varphi\]
    2.36  
    2.37  \section{Automata construction}
    2.38 -Before applying the automata-theoretic verification methods, we need to construct an automaton for a given specification formula $\varphi$. For that, we treat the model $\M = (\F, V)$ for an LTL-formula $\varphi$ as an infinite word over the finite alphabet $2^{Voc(\varphi)}$. 
    2.39 +Before applying the automata-theoretic verification methods, we need to construct the automaton for a given specification formula $\varphi$ and for the program $P$ in test.
    2.40  
    2.41 +\subsection{Specification automata}
    2.42 +For the construction of an automaton $\A_\varphi$ for an LTL-formula $\varphi$, we treat the model $\M = (\F, V)$ for an LTL-formula $\varphi$ as an infinite word over the finite alphabet $2^{Voc(\varphi)}$. 
    2.43 +
    2.44 +\begin{def:rep function}
    2.45  We define the \emph{representation function} $rep: \M \to 2^\Prop$, which returns an infinite word representing the model $\M_\varphi = (\F, V_\varphi)$ over the ordered image $V_\varphi^\rightarrow(\N)$ of its validation function, i.e., $rep(\M_\varphi) = (V_\varphi(0), V_\varphi(1), ...)$. Additionaly, we provide the \emph{inverted representation function} $rep^{-1}: 2^\Prop \to \M$, which compiles an infinite word to the corresponding model, i.e., $rep^{-1}(V_\varphi^\rightarrow(\N)) = \M_\varphi$.
    2.46  \[Mod(\varphi) = \{rep(\M_\varphi) \mid \M_\varphi = (\F, V_\varphi) \land \M_\varphi,0 \models \varphi\}\]
    2.47  $Mod(\varphi)$ is the set of all infinite words, which represent models for $\varphi$.
    2.48 +\end{def:rep function}
    2.49  
    2.50  \begin{def:fs closure}
    2.51  Let $\varphi$ be an LTL-formula, then the \emph{Fischer-Ladner closure} $FL(\varphi)$ of $\varphi$ is the smallest set of formulae such that following holds:
    2.52 @@ -297,10 +303,26 @@
    2.53  From theorem \ref{thm:model language} follows $Mod(\varphi) = L(\A_\varphi)$
    2.54  \end{cor:mod=model language}
    2.55  
    2.56 +\subsection{Program automata}
    2.57 +In the next step, we model a given program $P$ as automaton $\A_P$. A program is a structure $P = (S_P, s_0, R, V)$, where $S$ is the set of possible states of the program, $s_0$ the initial state, $R : S \times \Prop \times S$ the transition relation and $V : S \to 2^\Prop$ a valuation function. A \emph{computation} of $P$ is a run $\rho = (V(s_0), V(s_1), ...)$. 
    2.58 +
    2.59 +We construct automaton $\A_P = (\Sigma, S, S_0, \Delta, F)$, with:
    2.60 +\begin{itemize}
    2.61 +\begin{multicols}{2}
    2.62 +\item $\Sigma = 2^\Prop$
    2.63 +\item $S = S_P$
    2.64 +\item $S_0 = s_0$
    2.65 +\item $F = S$
    2.66 +\end{multicols}
    2.67 +\item $\Delta = \{(s, V(s), s') \mid \exists{a \in \Prop}: (s, a, s') \in R\}$
    2.68 +\end{itemize}
    2.69 +From $F = S$ follows that each run of $\A_P$ is accepting, therefore is $L_\omega(\A_P)$ the set of all computations of $P$.
    2.70 +
    2.71 +
    2.72  \section{Model checking}
    2.73 -For effective automata-theoretic verification of a reactive program we model the program as a non-deterministic B\"uchi automaton $P = (\Sigma, S, S_0, \Delta, F)$. Let $\rho$ be a run of $P$, we define:
    2.74 +For effective automata-theoretic verification of reactive programs, we model the program as a non-deterministic B\"uchi automaton $P = (\Sigma, S, S_0, \Delta, F)$. Let $\rho$ be a run of $P$, we define:
    2.75  \[Mod(P) = \{rep^{-1}(\rho) \mid \rho \text{ is a run of } P\}\]
    2.76 -The essence of model checking lies within the test for emptyness of the intersection between the recognised language of the automaton for the program in test and the recognised language of the automaton for its negated specification:
    2.77 +The essence of model checking lies within the test for emptyness of the intersection between the recognised language of the program automaton and the recognised language of the automaton for its negated specification:
    2.78  \[L(\A_P) \cap L(\A_{\neg \varphi}) = \emptyset\]
    2.79  From corollary \ref{cor:mod=model language} follows:
    2.80  \[L(\A_P) \cap L(\A_{\neg \varphi}) = \emptyset \iff Mod(P) \cap Mod(\neg \varphi) = \emptyset\]