1.1 --- a/paper/src/paper.tex	Mon Jul 11 16:25:01 2011 +0200
     1.2 +++ b/paper/src/paper.tex	Tue Jul 12 02:49:15 2011 +0200
     1.3 @@ -82,13 +82,23 @@
     1.4  %\itshape
     1.5  %\renewcommand\abstractname{Abstract} 
     1.6  \begin{abstract}
     1.7 -Algorithmic verification is a successful application of automated temporal reasoning based on automata-theoretic model checking. We use the power of modal logics to specify computational properties. System verification provides a correctness proof for the program design with respect to such properties. The methods used are a composition of automata theory, graph theory and modal logics. This text is an introduction to such automata theoretic constructions and space-efficient on-the-fly verification methods for reactive systems.
     1.8 +Algorithmic verification is an application of automated temporal reasoning based on automata-theoretic model checking. We use the power of modal logics to specify computational properties. System verification provides a correctness proof for the program design with respect to such properties. The methods used are a composition of automata theory, graph theory and modal logics. This text is an introduction to such automata theoretic constructions and space-efficient on-the-fly verification methods for reactive systems.
     1.9  %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 such automata and space-efficient on-the-fly verification methods for reactive systems. 
    1.10  \end{abstract}
    1.11  %\normalfont
    1.12  \newpage
    1.13  \section{Introduction}
    1.14 +The rapid digital evolution of semi-conductor design has changed the way of development in the industry. Exponential growth in processing frequencies has massive implications on the complexity of chip-design. When a considerable portion of the development cycles is dedicated to design validation, an increasingly high effort is invested in the realisation of efficient verification methods.
    1.15  
    1.16 +The computer hardware industry has adapted to the rise of complexity by the application of automated design verification. Another natural consequence was the preference of standard non-specialised hardware solutions accompanied by software realisation of the required functionality. Software systems have penetrated all industries, and increasingly so in high-demand and safety-critical application areas. Software programs provide high-demand server infrastructures for the internet, control our air traffic and protect our lifes in car accidents. When handling such critical systems, it becomes inevitable to verify the correctness of such software solutions. 
    1.17 +
    1.18 +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 begun to dominate recent software solutions, because we are closing the physical limits for single-core processor frequencies.
    1.19 +
    1.20 +Again, the industry is facing a \emph{validation crisis} \cite{ref:automated verification} and formal verification methods are in demand. Deductive, manual and 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.21 +
    1.22 +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.
    1.23 +
    1.24 +The first three sections will define the preliminaries for the automata-theoretic constructions. At first, we provide the notion of reasoning about infinite computational paths within formal language theory. Then we tackle those infinite structures with the help of automata theory, which shall build the framework of the formal verification theory. Next we introduce the reader to modal logics, in particular to linear temporal logic. Linear temporal logic is the language we use to talk about program properties, i.e., the propgram specification language. The fifth section interweaves automata theory and modal logics for the formalisation of program and specification automata construction. Based on this construction we apply the methods presented in the model checking section. The last section is a short excursion into the practical considerations of automated verification.
    1.25  
    1.26  \section{$\omega$-regular languages}
    1.27  \begin{def:finite words}
    1.28 @@ -228,9 +238,10 @@
    1.29  \end{prop:vocabulary sat}
    1.30  %
    1.31  \subsection{Derived connectives}
    1.32 +\label{sec:derived connectives}
    1.33  For a more convenient description of system specifications, we present some derived symbols to be used in LTL-formulae. At first, we introduce the notion of \emph{truth} and \emph{falsity} using constants $\top$ and $\bot$. Then we expand our set of connectives with the Boolean \emph{and}, \emph{implication} and \emph{equivalence}. And at last we derive the commonly used modal operators \emph{eventually} and \emph{henceforth}. 
    1.34  
    1.35 -In anticipation of section \ref{sec:on-the-fly methods}, we extend our logic's syntax with the binary connective $\V$, which will become useful in the interpretation known as the \emph{two-state semantics}.
    1.36 +In anticipation of section \ref{sec:on-the-fly methods}, we extend our logic's syntax with the binary connective $\V$, the dual of $\U$, which will become useful in the interpretation known as the \emph{two-state semantics}.
    1.37  
    1.38  Let $\varphi$ and $\psi$ be $L_{LTL}(\Prop)$-formulae:
    1.39  \begin{multicols}{2}
    1.40 @@ -242,7 +253,7 @@
    1.41  \item $\varphi \leftrightarrow \psi \equiv (\varphi \rightarrow \psi) \land (\psi \rightarrow \varphi)$
    1.42  \item $\Diamond \varphi \equiv \top \U \varphi$
    1.43  \item $\Box \varphi \equiv \neg \Diamond \neg \varphi$
    1.44 -\item $\varphi \V \psi \equiv \neg(\neg \varphi \U \psi)$
    1.45 +\item $\varphi \V \psi \equiv \neg(\neg \varphi \U \neg \psi)$
    1.46  \end{itemize}
    1.47  \end{multicols}
    1.48  \noindent From the derivations for operators $\Diamond$, \emph{read diamond}, and $\Box$, \emph{read box}, it follows:
    1.49 @@ -260,6 +271,7 @@
    1.50  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.
    1.51  
    1.52  \subsection{Specification automata}
    1.53 +\label{sec:specification automata}
    1.54  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)}$. 
    1.55  
    1.56  \begin{def:rep function}
    1.57 @@ -398,6 +410,8 @@
    1.58  \[\Phi^+ = \Prop \cup \overline{\Prop} \cup \{\top, \bot\} \cup \{\varphi \lor \psi, \varphi \land \psi, \X\varphi, \varphi \U \psi, \varphi \V \psi \mid \varphi, \psi \in \Phi^+\} \]
    1.59  \end{def:positive formulae}
    1.60  
    1.61 +The positive form of a formula contains only negations at the level of atomic propositions. This is the reason for the introduction of the dual $\V$ in \ref{sec:derived connectives}; to provide a way of shifting the negation of $\U$-formulae inwards by the substitution with its contrapositive form. 
    1.62 +
    1.63  \begin{def:next}
    1.64  Let $\Phi$ be a set of LTL-formulae, we define:
    1.65  \[next(\Phi) = \{ \X\varphi \mid \X\varphi \in \Phi\} \text{ and } snext(\Phi) = \{ \varphi \mid \X\varphi \in \Phi\}\]
    1.66 @@ -412,10 +426,10 @@
    1.67  &\dnf(\varphi \lor \psi) &=  &\, \dnf(\varphi) \cup \dnf(\psi)\\
    1.68  &\dnf(\varphi \land \psi) &=  &\, \{C \cup D \mid C \in \dnf(\varphi), D \in \dnf(\psi), C \cup D \text{ is consistent}\}\\
    1.69  &\dnf(\varphi \U \psi) &=  &\, \dnf(\varphi \land \X(\varphi \U \psi)) \cup \dnf(\psi)\\
    1.70 -&\dnf(\varphi \V \psi) &=  &\, \dnf(\varphi \land \psi) \cup \dnf(\psi \land \X(\varphi \V \psi))\\
    1.71 +&\dnf(\varphi \V \psi) &=  &\, \dnf(\varphi \land \psi) \cup \dnf(\psi \land \X(\varphi \V \psi))
    1.72  \end{align*}
    1.73  \end{def:dnf}
    1.74 -\noindent The disjunctive normal form provides the framework for the automata state construction over the two-state semantics. The modal connectives $\U$ and $\V$ are interpreted as disjunctions over the path of computation.
    1.75 +\noindent The disjunctive normal form provides the partitioning for the automata state construction over the two-state semantics. The modal connectives $\U$ and $\V$ are interpreted as disjunctions over the path of computation.
    1.76  
    1.77  \begin{lem:dnf}
    1.78  Let $\Phi^+$ be the set of formulae in positive form and let $\M_\varphi$ be a model over the vocabulary of $\varphi$ then following holds:
    1.79 @@ -430,7 +444,7 @@
    1.80  \item $C \subseteq \consq(C)$
    1.81  \item $\top \in \consq(C)$, if $\top \in CL(\varphi)$
    1.82  \end{multicols}
    1.83 -\vspace{-1.1em}
    1.84 +\vspace{-1em}
    1.85  \item $\psi \lor \chi \in \consq(C)$, if $\psi \lor \chi \in CL(\varphi)$ and $\psi \in \consq(C) \lor \chi \in \consq(C)$
    1.86  \item $\psi \land \chi \in \consq(C)$, if $\psi \land \chi \in CL(\varphi)$ and $\psi, \chi \in \consq(C)$
    1.87  \item $\psi \U \chi \in \consq(C)$, if $\psi \U \chi \in CL(\varphi)$ and $\psi, \X(\psi \U \chi) \in \consq(C) \lor \chi \in \consq(C)$
    1.88 @@ -462,6 +476,11 @@
    1.89  \end{itemize}
    1.90  \end{def:partial automata}
    1.91  
    1.92 +\noindent The soundness and completeness proofs are provided in \cite{ref:ltl&büchi}; the equivalance of the partial automata and the specification automata as defined in \ref{sec:specification automata} follows from the proofs.  
    1.93 +
    1.94 +\subsection{On-the-fly construction}
    1.95 +
    1.96 +
    1.97  \begin{thebibliography}{99}
    1.98  \bibitem{ref:ltl&büchi} 
    1.99  \uppercase{M{\footnotesize adhavan} M{\footnotesize ukund}.}
   1.100 @@ -473,6 +492,11 @@
   1.101  {\em Alternating Automata and Program Verification}.
   1.102  Computer Science Today, Volume 1000 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, 1995.
   1.103  
   1.104 +\bibitem{ref:on-the-fly verification} 
   1.105 +\uppercase{R{\footnotesize ob} G{\footnotesize erth,}  D{\footnotesize oron} P{\footnotesize eled,} M{\footnotesize oshe} Y. V{\footnotesize ardi and} P{\footnotesize ierre} W{\footnotesize olper}.}
   1.106 +{\em Simple On-the-fly Automatic Verification of Linear Temporal Logic}.
   1.107 +Proceeding IFIO/WG6.1 Symposium on Protocol Specification, Testing and Verification, Warsaw, 1995.
   1.108 +
   1.109  \bibitem{ref:concurrent checking}
   1.110  \uppercase{O{\footnotesize rna} L{\footnotesize ichtenstein and} A{\footnotesize mir} P{\footnotesize nueli}.}
   1.111  {\em Checking that finite state concurrent programs satisfy their linear specification}.