1.1 --- a/paper/src/paper.tex Thu Jun 30 18:00:04 2011 +0200
1.2 +++ b/paper/src/paper.tex Thu Jun 30 19:08:30 2011 +0200
1.3 @@ -33,7 +33,7 @@
1.4 }
1.5 \date{\textsc{\hfill}}
1.6
1.7 -\theoremstyle{definition} %plain, definition, remark, proof, corrolary
1.8 +\theoremstyle{definition} %plain, definition, remark, proof, corollary
1.9 \newtheorem*{def:finite words}{Finite words}
1.10 \newtheorem*{def:infinite words}{Infinite words}
1.11 \newtheorem*{def:regular languages}{Regular languages}
1.12 @@ -58,6 +58,7 @@
1.13
1.14 \theoremstyle{plain}
1.15 \newtheorem{thm:model language}{Theorem}[section]
1.16 +\newtheorem{cor:mod=model language}{Corollary}[thm:model language]
1.17
1.18 \begin{document}
1.19 \maketitle
1.20 @@ -111,7 +112,7 @@
1.21
1.22 \section{$\omega$-regular languages}
1.23 \begin{def:finite words}
1.24 -Let $\Sigma$ be a non-empty set of symbols, called the alphabet. $\Sigma^*$ is the set of all \emph{finite} words over $\Sigma$. A \emph{finite} word $w \in \Sigma^*$ is a \emph{finite} sequence $v_0,...,v_{n-1}$ of symbols from alphabet $\Sigma$ with length $n = |w|$. $\varepsilon$ denotes the empty word with length $|\varepsilon| = 0$.
1.25 +Let $\Sigma$ be a non-empty set of symbols, called the alphabet. $\Sigma^*$ is the set of all \emph{finite} words over $\Sigma$. A \emph{finite} word $w \in \Sigma^*$ is a \emph{finite} sequence $(v_0,...,v_{n-1})$ of symbols from alphabet $\Sigma$ with length $n = |w|$. $\varepsilon$ denotes the empty word with length $|\varepsilon| = 0$.
1.26 \end{def:finite words}
1.27
1.28 \begin{def:regular languages}
1.29 @@ -139,7 +140,7 @@
1.30 \end{def:regular languages closure}
1.31
1.32 \begin{def:infinite words}
1.33 -$\Sigma^\omega$ is the set of all \emph{infinite} words over $\Sigma$. An \emph{infinite} word $w \in \Sigma^\omega$ is an \emph{infinite} sequence $v_0,...,v_\infty$ with length $\infty$. To address the elements of the infinite sequence $w$, we view the word as a function $w : \N \to \Sigma$ with $w(i) = v_i$; thus $w(i)$ denotes the symbol at sequence position $i$ of word $w$; another notation used for $w(i)$ is $w_i$.
1.34 +$\Sigma^\omega$ is the set of all \emph{infinite} words over $\Sigma$. An \emph{infinite} word $w \in \Sigma^\omega$ is an \emph{infinite} sequence $(v_0,...,v_\infty)$ with length $\infty$. To address the elements of the infinite sequence $w$, we view the word as a function $w : \N \to \Sigma$ with $w(i) = v_i$; thus $w(i)$ denotes the symbol at sequence position $i$ of word $w$; another notation used for $w(i)$ is $w_i$.
1.35 \end{def:infinite words}
1.36
1.37 \begin{def:omega regular languages}
1.38 @@ -164,7 +165,7 @@
1.39 \end{def:buechi automata}
1.40
1.41 \begin{def:automata runs}
1.42 -Let $\A = (\Sigma, S, S_0, \Delta, F)$ be an automaton, a run $\rho$ of $\A$ on an infinite word $w = a_0,a_1,...$ over alphabet $\Sigma$ is a sequence $\rho = s_0,s_1,...$, where $s_0 \in S_0$ and $(s_i, a_i, s_{i+1}) \in \Delta$, for all $i \geq 0$. Again we may view the run sequence as a function $\rho : \N \to S$, where $\rho(i) = s_i$ denotes the state at the $i^{th}$ sequence position.
1.43 +Let $\A = (\Sigma, S, S_0, \Delta, F)$ be an automaton, a run $\rho$ of $\A$ on an infinite word $w = (a_0,a_1,...)$ over alphabet $\Sigma$ is a sequence $\rho = (s_0,s_1,...)$, where $s_0 \in S_0$ and $(s_i, a_i, s_{i+1}) \in \Delta$, for all $i \geq 0$. Again we may view the run sequence as a function $\rho : \N \to S$, where $\rho(i) = s_i$ denotes the state at the $i^{th}$ sequence position.
1.44 \end{def:automata runs}
1.45
1.46 \begin{def:automata acceptance}
1.47 @@ -273,7 +274,9 @@
1.48 \[\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.49
1.50 \section{Automata construction}
1.51 -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)}$. 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.52 +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)}$.
1.53 +
1.54 +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$.
1.55 \[Mod(\varphi) = \{rep(\M_\varphi) \mid \M_\varphi = (\F, V_\varphi) \land \M_\varphi,0 \models \varphi\}\]
1.56 $Mod(\varphi)$ is the set of all infinite words, which represent models for $\varphi$.
1.57
1.58 @@ -318,6 +321,7 @@
1.59 \end{itemize}
1.60
1.61 \begin{thm:model language}
1.62 +\label{thm:model language}
1.63 Let $\M_\varphi = (\F, V_\varphi)$ be a model and $rep(\M_\varphi)$ its infinite representation word, then following holds:
1.64 \[rep(\M_\varphi) \in L(\A_\varphi) \iff \M_\varphi,0 \models \varphi\]
1.65 \end{thm:model language}
1.66 @@ -325,10 +329,18 @@
1.67 \begin{proof}
1.68 For the eloberate proof, consult \cite{ref:ltl&büchi}.
1.69 \end{proof}
1.70 -
1.71 +\begin{cor:mod=model language}
1.72 +\label{cor:mod=model language}
1.73 +From theorem \ref{thm:model language} follows $Mod(\varphi) = L(\A_\varphi)$
1.74 +\end{cor:mod=model language}
1.75
1.76 \section{Model checking}
1.77 -
1.78 +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:
1.79 +\[Mod(P) = \{rep^{-1}(\rho) \mid \rho \text{ is a run of } P\}\]
1.80 +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:
1.81 +\[L(\A_P) \cap L(\A_{\neg \varphi}) = \emptyset\]
1.82 +From corollary \ref{cor:mod=model language} follows:
1.83 +\[L(\A_P) \cap L(\A_{\neg \varphi}) = \emptyset \iff Mod(P) \cap Mod(\neg \varphi) = \emptyset\]
1.84
1.85 \section{On-the-fly methods}
1.86