# HG changeset patch
# User Eugen Sawin <sawine@me73.com>
# Date 1309392383 -7200
# Node ID 5af4e417875e30e3b259acba4b1bcf97d5bac47a
# Parent  3402f14d907a0e0d4a76ca2bba7b34effc06ce6b
Started with automata construction.

diff -r 3402f14d907a -r 5af4e417875e paper/src/paper.tex
--- a/paper/src/paper.tex	Wed Jun 29 18:56:22 2011 +0200
+++ b/paper/src/paper.tex	Thu Jun 30 02:06:23 2011 +0200
@@ -41,13 +41,16 @@
 \newtheorem*{def:buechi automata}{Automata}
 \newtheorem*{def:automata runs}{Runs}
 \newtheorem*{def:automata acceptance}{Acceptance}
+\newtheorem*{def:general automata}{Generalised automata}
+\newtheorem*{def:general acceptance}{Acceptance}
 \newtheorem*{def:vocabulary}{Vocabulary}
 \newtheorem*{def:frames}{Frames}
 \newtheorem*{def:models}{Models}
 \newtheorem*{def:satisfiability}{Satisfiability}
 
 \theoremstyle{proposition}
-\newtheorem{prop:vocabulary sat}{Proposition}
+\newtheorem{prop:vocabulary sat}{Proposition}[section]
+\newtheorem{prop:general equiv}{Proposition}[section]
 
 \begin{document}
 \maketitle
@@ -148,7 +151,7 @@
 \begin{def:buechi automata}
 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$.
 
-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$.
+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$.
 
 Within this text \emph{automaton} will refer to the non-deterministic B\"uchi automaton, unless otherwise noted. 
 \end{def:buechi automata}
@@ -160,9 +163,26 @@
 \begin{def:automata acceptance}
 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$.
 
-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$.
+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$. A language $L$ is \emph{B\"uchi-recognisable} iff there is an automaton $A$ with $L = L_\omega(A)$.
 \end{def:automata acceptance}
 
+\subsection{Generalised B\"uchi automata}
+\begin{def:general automata}
+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$.
+\end{def:general automata}
+
+\begin{def:general acceptance}
+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$. 
+\end{def:general acceptance}
+
+\begin{prop:general equiv}
+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:
+\[L(A) = \bigcap_{i < k} L(A_i)\]
+\end{prop:general equiv}
+\noindent Intuitively follows the equivalance of the language recognition abilities of general and non-deterministic B\"uchi automata.
+
 \section{Linear temporal logic}
 \subsection{Syntax}
 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:
@@ -206,13 +226,16 @@
 \end{itemize}
 \end{multicols}
 %
-\noindent Let $\M$ be a model and $\varphi$ a LTL-formula, we define model $\M_{Voc(\varphi)}$:
-\[\forall{i \in \N}: \M_{Voc(\varphi)} = \M(i) \cap Voc(\varphi)\]
+\noindent Let $\M = (\F, V)$ be a model and $\varphi$ a LTL-formula, we define model $\M_{Voc(\varphi)} = (\F, V_{Voc(\varphi)})$ with:
+\[\forall{i \in \N}: V_{Voc(\varphi)}(i) = V(i) \cap Voc(\varphi)\]
+Henceforth, we will abbreviate $\M_{Voc(\varphi)}$ and $V_{Voc(\varphi)}$ with $\M_\varphi$ and $V_\varphi$ accordingly. 
+%\noindent Let $\M$ be a model and $\varphi$ a LTL-formula, we define model $\M_{Voc(\varphi)}$:
+%\[\forall{i \in \N}: \M_{Voc(\varphi)} = \M(i) \cap Voc(\varphi)\]
 \end{def:vocabulary}
 %
 \begin{prop:vocabulary sat}
 Let $\M$ be a model and $\varphi$ a LTL-formula, then following holds:
-\[\forall{i \in \N}: \M,i \models \varphi \iff \M_{Voc(\varphi)},i \models \varphi\] 
+\[\forall{i \in \N}: \M,i \models \varphi \iff \M_\varphi,i \models \varphi\] 
 \end{prop:vocabulary sat}
 %
 \subsection{Derived connectives}
@@ -241,6 +264,12 @@
 With the additional derived connectives we get the following $L_{LTL}(\Prop)$-formulae productions:
 \[\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\]
 
+\section{Automata construction}
+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)$.
+\[Mod(\varphi) = \{V_\varphi^\rightarrow(\N) \mid \M_\varphi = (\F, V_\varphi) \land \M_\varphi,0 \models \varphi\}\]
+$Mod(\varphi)$ is the set of all infinite words, which represent models for $\varphi$.
+
+
 \section{Model checking}