Started with automata construction.
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