Added some automata definitions.
1.1 --- a/paper/src/paper.tex Tue Jun 14 01:36:04 2011 +0200
1.2 +++ b/paper/src/paper.tex Wed Jun 22 20:06:27 2011 +0200
1.3 @@ -5,6 +5,7 @@
1.4 \usepackage{typearea}
1.5 \usepackage{algorithm}
1.6 \usepackage{algorithmic}
1.7 +%\usepackage{fullpage}
1.8 %\usepackage[T1]{fontenc}
1.9 %\usepackage{arev}
1.10
1.11 @@ -29,7 +30,9 @@
1.12 \newtheorem*{def:regular languages closure}{Regular closure}
1.13 \newtheorem*{def:omega regular languages}{$\omega$-regular languages}
1.14 \newtheorem*{def:omega regular languages closure}{$\omega$-regular closure}
1.15 -
1.16 +\newtheorem*{def:buechi automata}{Automata}
1.17 +\newtheorem*{def:automata runs}{Runs}
1.18 +\newtheorem*{def:automata acceptance}{Acceptance}
1.19 \begin{document}
1.20
1.21 \maketitle
1.22 @@ -83,7 +86,7 @@
1.23
1.24 \section{$\omega$-regular languages}
1.25 \begin{def:finite words}
1.26 -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.27 +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.28 \end{def:finite words}
1.29
1.30 \begin{def:regular languages}
1.31 @@ -107,7 +110,7 @@
1.32 \end{def:regular languages closure}
1.33
1.34 \begin{def:infinite words}
1.35 -$\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$, view the word as a function $w : \mathbb{N}_0 \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.36 +$\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 : \mathbb{N}_0 \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.37 \end{def:infinite words}
1.38
1.39 \begin{def:omega regular languages}
1.40 @@ -124,7 +127,24 @@
1.41
1.42
1.43 \section{B\"uchi automata}
1.44 -Automata are good.
1.45 +\begin{def:buechi automata}
1.46 +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.47 +
1.48 +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.49 +
1.50 +Within this text \emph{automata/automaton} will refer to non-deterministic B\"uchi automata/automaton, unless otherwise noted.
1.51 +\end{def:buechi automata}
1.52 +
1.53 +\begin{def:automata runs}
1.54 +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 : \mathbb{N}_0 \to S$, where $\rho(i) = s_i$ denotes the state at the $i^{th}$ sequence position.
1.55 +\end{def:automata runs}
1.56 +
1.57 +\begin{def:automata acceptance}
1.58 +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 \mathbb{N}_0}: \rho(n) = s\}$, where $\exists^\omega$ denotes the existential quantifier for infinitely many occurances, i.e., $s$ occurs infinitely often in $\rho$.
1.59 +
1.60 +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.61 +\end{def:automata acceptance}
1.62 +
1.63 \section{Linear temporal logic}
1.64
1.65 \section{Model checking}