1.1 --- a/paper/src/paper.tex	Wed Jun 29 18:56:22 2011 +0200
     1.2 +++ b/paper/src/paper.tex	Thu Jun 30 02:06:23 2011 +0200
     1.3 @@ -41,13 +41,16 @@
     1.4  \newtheorem*{def:buechi automata}{Automata}
     1.5  \newtheorem*{def:automata runs}{Runs}
     1.6  \newtheorem*{def:automata acceptance}{Acceptance}
     1.7 +\newtheorem*{def:general automata}{Generalised automata}
     1.8 +\newtheorem*{def:general acceptance}{Acceptance}
     1.9  \newtheorem*{def:vocabulary}{Vocabulary}
    1.10  \newtheorem*{def:frames}{Frames}
    1.11  \newtheorem*{def:models}{Models}
    1.12  \newtheorem*{def:satisfiability}{Satisfiability}
    1.13  
    1.14  \theoremstyle{proposition}
    1.15 -\newtheorem{prop:vocabulary sat}{Proposition}
    1.16 +\newtheorem{prop:vocabulary sat}{Proposition}[section]
    1.17 +\newtheorem{prop:general equiv}{Proposition}[section]
    1.18  
    1.19  \begin{document}
    1.20  \maketitle
    1.21 @@ -148,7 +151,7 @@
    1.22  \begin{def:buechi automata}
    1.23  A non-deterministic B\"uchi automaton is a tuple $A = (\Sigma, S, S_0, \Delta, F)$, where $\Sigma$ is a finite non-empty \emph{alphabet}, $S$ is a finite non-empty set of \emph{states}, $S_0 \subseteq S$ is the set of \emph{initial states}, $F \subseteq S$ is the set of \emph{accepting states} and $\Delta: S \times \Sigma \times S$ is a \emph{transition relation}. When suitable we will use the arrow notation for the transitions, where $s \xrightarrow{a} s'$ iff $(s, a, s') \in \Delta$.
    1.24  
    1.25 -A deterministic B\"uchi automaton is a specialisation where the \emph{transition relation} $\Delta$ is a \emph{transition function} $\delta: S \times \Sigma \to S$ and the set $S_0$ of \emph{initial states} contains only a single state $s_0$.
    1.26 +A \emph{deterministic B\"uchi automaton} is a specialisation where the \emph{transition relation} $\Delta$ is a \emph{transition function} $\delta: S \times \Sigma \to S$ and the set $S_0$ of \emph{initial states} contains only a single state $s_0$.
    1.27  
    1.28  Within this text \emph{automaton} will refer to the non-deterministic B\"uchi automaton, unless otherwise noted. 
    1.29  \end{def:buechi automata}
    1.30 @@ -160,9 +163,26 @@
    1.31  \begin{def:automata acceptance}
    1.32  Let $A = (\Sigma, S, S_0, \Delta, F)$ be an automaton and let $\rho$ be a run of $A$, we define $inf(\rho) = \{s \in S \mid \exists^\omega{n \in \N}: \rho(n) = s\}$, where $\exists^\omega$ denotes the existential quantifier for infinitely many occurances, i.e., $s$ occurs infinitely often in $\rho$.
    1.33  
    1.34 -The run $\rho$ is \emph{accepting} iff $inf(\rho) \cap F \neq \emptyset$, i.e., there exists an \emph{accepting state} which occurs infinitely often in the run $\rho$. The automaton $A$ \emph{accepts} an input word $w$, iff there exists a run $\rho$ of $A$ on $w$, such that $\rho$ is \emph{accepting}. The language $L_\omega(A)$ recognised by automaton $A$ is the set of all infinite words accepted by $A$.
    1.35 +The run $\rho$ is \emph{accepting} iff $inf(\rho) \cap F \neq \emptyset$, i.e., there exists an \emph{accepting state} which occurs infinitely often in the run $\rho$. The automaton $A$ \emph{accepts} an input word $w$, iff there exists a run $\rho$ of $A$ on $w$, such that $\rho$ is \emph{accepting}. 
    1.36 +
    1.37 +The language $L_\omega(A)$ recognised by automaton $A$ is the set of all infinite words accepted by $A$. A language $L$ is \emph{B\"uchi-recognisable} iff there is an automaton $A$ with $L = L_\omega(A)$.
    1.38  \end{def:automata acceptance}
    1.39  
    1.40 +\subsection{Generalised B\"uchi automata}
    1.41 +\begin{def:general automata}
    1.42 +A \emph{generalised B\"uchi automaton} $A$ is a tuple $(\Sigma, S, S_0, \Delta, \{F_i\}_{i < k})$ for $i, k \in \N$, where the \emph{acceppting states} $F_i$ are composed within a finite set with $F_i \subseteq S$.
    1.43 +\end{def:general automata}
    1.44 +
    1.45 +\begin{def:general acceptance}
    1.46 +The acceptance condition is adjusted accordingly. A run $\rho$ of $A$ is \emph{accepting} iff $\forall{i < k}: inf(\rho) \cap F_i \neq \emptyset$. 
    1.47 +\end{def:general acceptance}
    1.48 +
    1.49 +\begin{prop:general equiv}
    1.50 +Let $A = (\Sigma, S, S_0, \Delta, \{F_i\}_{i < k})$ be a \emph{generalised automaton} and let $A_i = (\Sigma, S, S_0, \Delta, F_i)$ be \emph{non-deterministic automata}, then following equivalance condition holds:
    1.51 +\[L(A) = \bigcap_{i < k} L(A_i)\]
    1.52 +\end{prop:general equiv}
    1.53 +\noindent Intuitively follows the equivalance of the language recognition abilities of general and non-deterministic B\"uchi automata.
    1.54 +
    1.55  \section{Linear temporal logic}
    1.56  \subsection{Syntax}
    1.57  Let $\Prop$ be the countable set of \emph{atomic propositions}. The \emph{alphabet} of the language $L_{LTL}(\Prop)$ is $\Prop \cup \{\neg, \lor, X, U\}$. We define the $L_{LTL}(\Prop)$-\emph{formulae} $\varphi$ using following productions:
    1.58 @@ -206,13 +226,16 @@
    1.59  \end{itemize}
    1.60  \end{multicols}
    1.61  %
    1.62 -\noindent Let $\M$ be a model and $\varphi$ a LTL-formula, we define model $\M_{Voc(\varphi)}$:
    1.63 -\[\forall{i \in \N}: \M_{Voc(\varphi)} = \M(i) \cap Voc(\varphi)\]
    1.64 +\noindent Let $\M = (\F, V)$ be a model and $\varphi$ a LTL-formula, we define model $\M_{Voc(\varphi)} = (\F, V_{Voc(\varphi)})$ with:
    1.65 +\[\forall{i \in \N}: V_{Voc(\varphi)}(i) = V(i) \cap Voc(\varphi)\]
    1.66 +Henceforth, we will abbreviate $\M_{Voc(\varphi)}$ and $V_{Voc(\varphi)}$ with $\M_\varphi$ and $V_\varphi$ accordingly. 
    1.67 +%\noindent Let $\M$ be a model and $\varphi$ a LTL-formula, we define model $\M_{Voc(\varphi)}$:
    1.68 +%\[\forall{i \in \N}: \M_{Voc(\varphi)} = \M(i) \cap Voc(\varphi)\]
    1.69  \end{def:vocabulary}
    1.70  %
    1.71  \begin{prop:vocabulary sat}
    1.72  Let $\M$ be a model and $\varphi$ a LTL-formula, then following holds:
    1.73 -\[\forall{i \in \N}: \M,i \models \varphi \iff \M_{Voc(\varphi)},i \models \varphi\] 
    1.74 +\[\forall{i \in \N}: \M,i \models \varphi \iff \M_\varphi,i \models \varphi\] 
    1.75  \end{prop:vocabulary sat}
    1.76  %
    1.77  \subsection{Derived connectives}
    1.78 @@ -241,6 +264,12 @@
    1.79  With the additional derived connectives we get the following $L_{LTL}(\Prop)$-formulae productions:
    1.80  \[\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.81  
    1.82 +\section{Automata construction}
    1.83 +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 infinite word representing the model $\M_\varphi = (\F, V_\varphi)$ by the image of its validation function $V_\varphi^\rightarrow(\N)$.
    1.84 +\[Mod(\varphi) = \{V_\varphi^\rightarrow(\N) \mid \M_\varphi = (\F, V_\varphi) \land \M_\varphi,0 \models \varphi\}\]
    1.85 +$Mod(\varphi)$ is the set of all infinite words, which represent models for $\varphi$.
    1.86 +
    1.87 +
    1.88  \section{Model checking}
    1.89  
    1.90