1.1 --- a/paper/src/paper.tex	Fri Jul 15 22:26:36 2011 +0200
     1.2 +++ b/paper/src/paper.tex	Fri Jul 15 23:37:27 2011 +0200
     1.3 @@ -287,7 +287,8 @@
     1.4  \end{def:models}
     1.5  
     1.6  \subsubsection{Example}
     1.7 -Figure \ref{fig:model} shows a model over $\Prop = \{p_0, p_1, p_2\}$ with $V = \{(s_0, \{p_0\}), (s_1, \{p_0, p_2\}),$ $(s_2, \{p_1\}), ...\}$, where each time instant $i$ is represented by a circle, the accessibility relations via the arrows and the image of the valuation function as sets within the circles.
     1.8 +\label{ex:model}
     1.9 +Figure \ref{fig:model} shows a model $\M_1$ over $\Prop = \{p_0, p_1, p_2\}$ with $V = \{(s_0, \{p_0\}), (s_1, \{p_0, p_2\}),$ $(s_2, \{p_1\})\} \cup \{(s_i, \{p_1\}) \mid i > 2\}$, where each time instant $i$ is represented by a circle, the accessibility relations via the arrows and the image of the valuation function as sets within the circles.
    1.10  
    1.11  \begin{figure}[h]
    1.12  \centering
    1.13 @@ -299,7 +300,7 @@
    1.14  \path (s_1) [late options={label=below:$s_1$}];
    1.15  \node[state] (s_2) [right of= s_1] {$\{p_1\}$};
    1.16  \path (s_2) [late options={label=below:$s_2$}];
    1.17 -\node[state] (s_i) [right of= s_2] {$...$};
    1.18 +\node[state] (s_i) [right of= s_2] {$\{p_1\}$};
    1.19  \path (s_i) [late options={label=below:$s_i$}];
    1.20  \path[->] 
    1.21  (s_0) edge node {$R$} (s_1) 
    1.22 @@ -307,10 +308,9 @@
    1.23  \path[dashed,->] 
    1.24  (s_2) edge node {$R$} (s_i); 
    1.25  \end{tikzpicture}
    1.26 -\caption{Model example}
    1.27 +\caption{Example model $\M_1$}
    1.28  \label{fig:model}
    1.29  \end{figure}
    1.30 -
    1.31  %
    1.32  \begin{def:satisfiability}
    1.33  A model $\M = (\F, V)$ \emph{satisfies} a formula $\varphi$ at time instant $i$ is denoted by $\M,i \models \varphi$. Satisfiability of a formula $\varphi$ is defined inductively over the structure of $\varphi$:
    1.34 @@ -355,7 +355,7 @@
    1.35  \label{sec:derived connectives}
    1.36  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.37  
    1.38 -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.39 +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 \emph{two-state semantics}.
    1.40  
    1.41  Let $\varphi$ and $\psi$ be $L_{LTL}(\Prop)$-formulae:
    1.42  \begin{multicols}{2}
    1.43 @@ -381,6 +381,17 @@
    1.44  \noindent With the additional derived connectives we get the following $L_{LTL}(\Prop)$-formulae productions:
    1.45  \[\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\]
    1.46  
    1.47 +\subsection{Examples}
    1.48 +Based on the examples in \cite{ref:ltl&büchi}, we provide following formulae:
    1.49 +\begin{itemize}
    1.50 +\item $\varphi = \Diamond \Box p_1$, i.e., eventually $p_1$ becomes a stable property
    1.51 +\item $\psi = \Diamond p_2$, i.e., $p_2$ is eventually $true$
    1.52 +\item $\chi = p_0 \lor p_1$, i.e., it always holds that either $p_0$ or $p_1$ are $true$
    1.53 +\item $\xi = p_0\U p_1$, meaning $p_0$ holds until $p_1$ is $true$
    1.54 +\end{itemize}
    1.55 +It happens so, that the model $\M_1$, from our previous Example \ref{ex:model}, satisfies all these formulae:
    1.56 +$\M_1,i \models \varphi$, $\M_1,i \models \psi$, $\M_1,i \models \chi$, $\M_1,i \models \xi$.
    1.57 +
    1.58  \section{Automata construction}
    1.59  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.60  
    1.61 @@ -389,7 +400,7 @@
    1.62  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.63  
    1.64  \begin{def:rep function}
    1.65 -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), ...)$. Additionally, 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$.
    1.66 +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), ...)$. 
    1.67  \[Mod(\varphi) = \{rep(\M_\varphi) \mid \M_\varphi = (\F, V_\varphi) \land \M_\varphi,0 \models \varphi\}\]
    1.68  $Mod(\varphi)$ is the set of all infinite words, which represent models for $\varphi$.
    1.69  \end{def:rep function}
    1.70 @@ -517,7 +528,7 @@
    1.71  \[\forall{i \in \N}: \M,i \models \varphi \iff \M,i \models b \text{ or } \M,i+1 \models a \land \X(\varphi)\]
    1.72  In this example, we construct the specification automaton incrementally for each time instant; the states are constructed from the union of the current-state and next-state requirements $\{b\} \cup \{a, \X(\varphi)\}$.
    1.73  
    1.74 -Let us formalise the notion of the incremental automaton construction based on the idea of the two-state semantics.
    1.75 +Let us capture the notion of the incremental automaton construction based on the idea of the two-state semantics.
    1.76  
    1.77  \begin{def:positive formulae}
    1.78  Let $\Prop$ be a set of atomic propositions and let $\overline{\Prop} = \{\neg p \mid p \in \Prop\}$. We define the set of LTL-formulae in \emph{positive form}:
    1.79 @@ -595,34 +606,36 @@
    1.80  \subsection{On-the-fly construction}
    1.81  The sequential description of the program design makes it trivial to incrementally construct the program automaton state by state. The more difficult part is the construction of the partial specification automaton on-the-fly. 
    1.82  
    1.83 -To archive this, we begin with a set of states built by applying $\dnf(\varphi)$. In the next step we determine a state within the current set of states, which is consistent with the program automaton. We use this state to expand its successor states. Now, we analyse the expanded state space for cycles. If no cycles are detected, we repeat this procedure, while there are still consistent states left. 
    1.84 +To archive this, we begin with a set of states built by applying $\dnf(\varphi)$. In the next step we determine a state within the current set of states, which is consistent with the program automaton. We use this state $S$ to expand its successor states by applying $dnf(\bigwedge snext(S))$. Now, we analyse the expanded state space for cycles. If no cycles are detected, we repeat this procedure, while there are still consistent states left. 
    1.85  
    1.86 -When the procedure terminates, we check whether the specification automaton was fully built. If that is the case, we have explored the whole state space of both automata and have not found any cycles, i.e., the program does satisfy the specification. Otherwise, the procedure was prematurely aborted by a cycle detection, i.e., the program does satisfy the \emph{negated} specification and therefore does \emph{not} meet the specification properties. 
    1.87 +When the procedure terminates and we have explored the whole state space of both automata without registered cycles, the program does satisfy the specification. Otherwise, the procedure was prematurely aborted by a cycle detection, i.e., the program does satisfy the \emph{negated} specification and therefore does \emph{not} meet the specification properties. 
    1.88  
    1.89 -\begin{algorithm}
    1.90 -\caption{expand: $\Phi^+ \times 2^Q \to 2^Q$}
    1.91 -\label{alg:expand}
    1.92 -\begin{algorithmic}
    1.93 -\REQUIRE $Node : node, NodeSet: set\, of\, nodes$
    1.94 -\STATE $ExpandedNodes = \dnf(\bigwedge snext(Node)) - NodeSet$
    1.95 -\RETURN $ExpandedNodes$
    1.96 -\end{algorithmic}
    1.97 -\end{algorithm}
    1.98 +Given formula length $n = |\varphi|$, the described algorithm runs in $2^{O(n^2)}$ time \cite{ref:ltl&büchi}, some optimisations can reduce it to $2^{O(n)}$ \cite{ref:on-the-fly verification}.
    1.99  
   1.100 -\begin{algorithm}
   1.101 -\caption{verify: $\A \times L_{LTL}(\Prop) \to Boolean$}
   1.102 -\label{alg:create}
   1.103 -\begin{algorithmic}
   1.104 -\REQUIRE $\A_P: automaton, \varphi: formula$
   1.105 -\STATE $S = \dnf(\varphi)$
   1.106 +%\begin{algorithm}
   1.107 +%\caption{expand: $\Phi^+ \times 2^Q \to 2^Q$}
   1.108 +%\label{alg:expand}
   1.109 +%\begin{algorithmic}
   1.110 +%\REQUIRE $Node : node, NodeSet: set\, of\, nodes$
   1.111 +%\STATE $ExpandedNodes = \dnf(\bigwedge snext(Node)) - NodeSet$
   1.112 +%\RETURN $ExpandedNodes$
   1.113 +%\end{algorithmic}
   1.114 +%\end{algorithm}
   1.115 +
   1.116 +%\begin{algorithm}
   1.117 +%\caption{verify: $\A \times L_{LTL}(\Prop) \to Boolean$}
   1.118 +%\label{alg:create}
   1.119 +%\begin{algorithmic}
   1.120 +%\REQUIRE $\A_P: automaton, \varphi: formula$
   1.121 +%\STATE $S = \dnf(\varphi)$
   1.122  %\WHILE {$Mod(\bigvee_{s \in S} \bigwedge s) \cap Mod(\A_P) = \emptyset$}
   1.123 -\WHILE {$consistent(S, \A_P) \neq \emptyset \land \neg cycle(S, \A_P)$}
   1.124 -\STATE $Node \in consistent(S, \A_P)$
   1.125 -\STATE $S = S \cup expand(Node, S)$
   1.126 -\ENDWHILE
   1.127 -\RETURN $\neg complete(S, \varphi)$
   1.128 -\end{algorithmic}
   1.129 -\end{algorithm}
   1.130 +%\WHILE {$consistent(S, \A_P) \neq \emptyset \land \neg cycle(S, \A_P)$}
   1.131 +%\STATE $Node \in consistent(S, \A_P)$
   1.132 +%\STATE $S = S \cup expand(Node, S)$
   1.133 +%\ENDWHILE
   1.134 +%\RETURN $\neg complete(S, \varphi)$
   1.135 +%\end{algorithmic}
   1.136 +%\end{algorithm}
   1.137  
   1.138  \section*{Discussion}
   1.139  \emph{Linear-Time Temporal Logic and B\"uchi Automata} \cite{ref:ltl&büchi} is an in-depth introduction to automated verification. It delivers the core concepts of model checking in a comprehensible way. The formal proofs are clean and well absorbable. The referenced material effectively fills the gaps, when looking for more detailed explanations, e.g. about the on-the-fly method. Some few, but good examples support the substantiation of the theoretic material. The introduction section provides a good overview of the text structure and the basic theory behind most concepts used.