1.1 --- a/paper/src/paper.tex	Mon Jul 11 03:04:11 2011 +0200
     1.2 +++ b/paper/src/paper.tex	Mon Jul 11 16:25:01 2011 +0200
     1.3 @@ -30,10 +30,10 @@
     1.4  \tiny{Draft}
     1.5  }}
     1.6  \author{
     1.7 -\uppercase{{\small{E}\scriptsize{UGEN} \small{S}\scriptsize{AWIN}}\thanks{\lowercase{\scriptsize{\texttt{sawine@informatik.uni-freiburg.de}}}}\\
     1.8 -{\em \small{U}\scriptsize{NIVERSITY OF} \small{F}\scriptsize{REIBURG}}\thanks{\tiny{Computer Science Department, Research Group for Foundations of Artificial Intelligence}}\\
     1.9 +\uppercase{{\small{E}\scriptsize{UGEN} \small{S}\scriptsize{AWIN}}}\thanks{\texttt{sawine@informatik.uni-freiburg.de}}\\
    1.10 +\uppercase{{\em \small{U}\scriptsize{NIVERSITY OF} \small{F}\scriptsize{REIBURG}}}\thanks{Computer Science Department, Research Group for Foundations of Artificial Intelligence}\\
    1.11  %{\em \small{C}\scriptsize{omputer} \small{S}\scriptsize{cience} \small{D}\scriptsize{epartment}}\\
    1.12 -{\em \small{G}\scriptsize{ERMANY}}}\\
    1.13 +\uppercase{{\em \small{G}\scriptsize{ERMANY}}}\\
    1.14  %\texttt{\footnotesize{sawine@informatik.uni-freiburg.de}}
    1.15  }
    1.16  \date{\textsc{\hfill}}
    1.17 @@ -300,7 +300,7 @@
    1.18  We define the set of all atoms of formula $\varphi$ with $\mathbb{AT}_\varphi = \{A \subseteq CL({\varphi}) \mid A \text{ is an atom}\}$.
    1.19  \end{def:atoms}
    1.20  
    1.21 -\noindent Now that we have the required ingredients, we begin with the construction of automaton $\A_\varphi$ for formula $\varphi$. Let $\A_\varphi = (\Sigma, S, S_0, \Delta, \{F_i\}_{i < k})$ with:
    1.22 +\noindent Now that we have the required ingredients, we begin with the construction of automaton $\A_\varphi$ for formula $\varphi$. Let $\A_\varphi = (\Sigma, S, S_0, \Delta, \{F_i\})$ with:
    1.23  \begin{itemize}
    1.24  \item $\Sigma = 2^{Voc(\varphi)}$
    1.25  \item $S = \mathbb{AT_\varphi}$
    1.26 @@ -308,7 +308,7 @@
    1.27  %\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.28  \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.29  %\item $\forall{i \in \N, i < k = |\mathbb{U}_{CL(\varphi)}|}: F_i = \{A \in \mathbb{AT}_\varphi \mid \psi \U \chi \notin A$ or $\chi \in A\}$
    1.30 -\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 \leq |\mathbb{U}_{\varphi}|$
    1.31 +\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\}$
    1.32  %Let $A, B \in \mathbb{AT}$ and $P \subseteq Voc(\varphi)$. Then $(A, P, B) \in \Delta$ iff the following holds:
    1.33  %$P = A \cap Voc(\varphi)$ and For all $\X \psi \in CL(\varphi): \X \psi \in A$ iff $\psi \in B$.
    1.34  \end{itemize}
    1.35 @@ -369,7 +369,7 @@
    1.36  Let $P$ be a finite-state program and $\A_P$ its automaton, let $\varphi$ be an LTL-formula and $\A_\varphi$ its automaton. P satisfies $\varphi$ iff $L_\omega(\A_P) \cap L_\omega(\A_{\neg \varphi}) = \emptyset$.
    1.37  \end{thm:model checking}
    1.38  
    1.39 -From Corollary \ref{cor:mod=model language} and \ref{cor:mod=program language} follows:
    1.40 +\noindent From Corollary \ref{cor:mod=model language} and \ref{cor:mod=program language} follows:
    1.41  \[L_\omega(\A_P) \cap L_\omega(\A_{\neg \varphi}) = \emptyset \iff Mod(P) \cap Mod(\neg \varphi) = \emptyset\]
    1.42  
    1.43  \subsection{Complexity}
    1.44 @@ -383,6 +383,16 @@
    1.45  
    1.46  A more space-efficient strategy is the on-the-fly construction of the automaton during a depth-first search, short DFS. The DFS explores the product states of both automata incrementally, testing for cycles in each iteration. If the program does not satisfy a formula, an accepting cycle will occur and lead to termination of the search. In the case of a valid program, i.e., the program does meet the specification, no cycles will occur. In the latter case, such a strategy would inevitably explore the whole state space of the automata.
    1.47  
    1.48 +\subsection{Two-state semantics}
    1.49 +For the successful incremental construction of automata, we provide a new interpretation for the infinite computation paths. By applying temporal reasoning, we separate the computation paths in two states, incrementally for each time instant. The two states resemble the satisfiability requirements for any time instant $i$ and its successor $i+1$.
    1.50 +
    1.51 +\subsubsection{Example}
    1.52 +Let $\varphi = a \U b$. We apply the two-state semantics on $\varphi$ and it follows:
    1.53 +\[\forall{i \in \N}: \M,i \models \varphi \iff \M,i \models b \text{ or } \M,i+1 \models a \land \X(\varphi)\]
    1.54 +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.55 +
    1.56 +Let us formalise the notion of the incremental automaton construction based on the idea of the two-state semantics.
    1.57 +
    1.58  \begin{def:positive formulae}
    1.59  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.60  \[\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.61 @@ -405,10 +415,11 @@
    1.62  &\dnf(\varphi \V \psi) &=  &\, \dnf(\varphi \land \psi) \cup \dnf(\psi \land \X(\varphi \V \psi))\\
    1.63  \end{align*}
    1.64  \end{def:dnf}
    1.65 +\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.66  
    1.67  \begin{lem:dnf}
    1.68 -Let $\Phi^+$ be the set of formulae in positive form then following holds:
    1.69 -\[\forall{\varphi \in \Phi^+}: \varphi \iff \bigvee_{D \in \dnf(\varphi)} \bigwedge D\]
    1.70 +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.71 +\[\forall{\varphi \in \Phi^+}: \M_\varphi,0 \models \varphi \iff \M_\varphi,0 \models \bigvee_{D \in \dnf(\varphi)} \bigwedge D\]
    1.72  \end{lem:dnf}
    1.73  
    1.74  \begin{def:consq}