1.1 --- a/paper/src/paper.tex Tue Jun 28 00:16:13 2011 +0200
1.2 +++ b/paper/src/paper.tex Tue Jun 28 14:45:02 2011 +0200
1.3 @@ -5,6 +5,7 @@
1.4 \usepackage{typearea}
1.5 \usepackage{algorithm}
1.6 \usepackage{algorithmic}
1.7 +\usepackage{multicol}
1.8 %\usepackage{fullpage}
1.9 %\usepackage[T1]{fontenc}
1.10 %\usepackage{arev}
1.11 @@ -23,7 +24,7 @@
1.12 }
1.13 \date{\textsc{\hfill}}
1.14
1.15 -\theoremstyle{definition} %plain, definition, remark
1.16 +\theoremstyle{definition} %plain, definition, remark, proposition, proof, corrolary
1.17 \newtheorem*{def:finite words}{Finite words}
1.18 \newtheorem*{def:infinite words}{Infinite words}
1.19 \newtheorem*{def:regular languages}{Regular languages}
1.20 @@ -35,7 +36,9 @@
1.21 \newtheorem*{def:automata acceptance}{Acceptance}
1.22 \newtheorem*{def:vocabulary}{Vocabulary}
1.23
1.24 +\theoremstyle{proposition}
1.25 \newtheorem{prop:vocabulary sat}{Proposition}
1.26 +
1.27 \begin{document}
1.28
1.29 \maketitle
1.30 @@ -94,15 +97,18 @@
1.31
1.32 \begin{def:regular languages}
1.33 The class of regular languages is defined recursively over an alphabet $\Sigma$:
1.34 +\begin{multicols}{2}
1.35 \begin{itemize}
1.36 \item $\emptyset$ is regular
1.37 \item $\{\varepsilon\}$ is regular
1.38 \item $\forall_{a \in \Sigma}:\{a\}$ is regular
1.39 \end{itemize}
1.40 +\end{multicols}
1.41 \end{def:regular languages}
1.42
1.43 \begin{def:regular languages closure}
1.44 Let $L_{R_1}, L_{R_2} \in \Sigma^*$ be regular. The class of regular languages is closed under following operations:
1.45 +\begin{multicols}{2}
1.46 \begin{itemize}
1.47 \item $L_{R_1}^*$
1.48 \item $L_{R_1} \circ L_{R_2}$
1.49 @@ -110,6 +116,7 @@
1.50 \item $L_{R_1} \cap L_{R_2}$
1.51 \item $\overline{L}_{R_1}$ and therefore $L_{R_1} - L_{R_2}$
1.52 \end{itemize}
1.53 +\end{multicols}
1.54 \end{def:regular languages closure}
1.55
1.56 \begin{def:infinite words}
1.57 @@ -131,7 +138,7 @@
1.58
1.59 \section{B\"uchi automata}
1.60 \begin{def:buechi automata}
1.61 -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.62 +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.63
1.64 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.65
1.66 @@ -145,7 +152,7 @@
1.67 \begin{def:automata acceptance}
1.68 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.69
1.70 -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.71 +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.72 \end{def:automata acceptance}
1.73
1.74 \section{Linear temporal logic}
1.75 @@ -159,7 +166,7 @@
1.76 LTL is interpreted over \emph{computation paths}, where a computation corrensponds to a model over a \emph{Kripke-frame} constructed by the order of natural numbers.
1.77
1.78 \subsection*{Semantics}
1.79 -A \emph{model} is a function $M: \mathbb{N}_0 \to 2^P$ over \emph{frame} $F$. The frame constitutes a linear order over $\mathbb{N}_0$, which corresponds to the linear temporal progression from \emph{now/before} to \emph{later}. Therefore $M(i)$ assigns a set of \emph{positive atomic propositions} to each state of time instant $i$. Intuitively we say $p \in P$ is \emph{true} at time instant $i$, iff $p \in M(i)$.
1.80 +A \emph{model} is a function $M: \mathbb{N}_0 \to 2^P$ over \emph{frame} $F$. The frame constitutes a linear order over $\mathbb{N}_0$, which corresponds to the linear progression of time from the \emph{present/past} into the \emph{future}. Therefore $M(i)$ assigns a set of \emph{positive atomic propositions} to each state of time instant $i$. Intuitively we say $p \in P$ is \emph{true} at time instant $i$ iff $p \in M(i)$.
1.81
1.82 A model $M$ \emph{satisfies} an LTL-formula $\varphi$ at time instant $i$ is denoted by $M,i \models \varphi$. Satisfaction of a formula $\varphi$ is defined inductively over the structure of $\varphi$:
1.83 \begin{itemize}
1.84 @@ -172,6 +179,7 @@
1.85
1.86 \begin{def:vocabulary}
1.87 Let $\varphi$ be a LTL-formula over atomic propositions $P$, we define the \emph{vocabulary} $Voc(\varphi)$ of $\varphi$ inductively:
1.88 +\begin{multicols}{2}
1.89 \begin{itemize}
1.90 \item $Voc(p) = \{p\}$ for $p \in P$
1.91 \item $Voc(\neg \varphi) = Voc(\varphi)$
1.92 @@ -179,16 +187,33 @@
1.93 \item $Voc(X \varphi) = Voc(\varphi)$
1.94 \item $Voc(\varphi U \psi) = Voc(\varphi) \cup Voc(\psi)$
1.95 \end{itemize}
1.96 +\end{multicols}
1.97 +
1.98 Let $M$ be a model and $\varphi$ a LTL-formula, we define model $M_{Voc(\varphi)}$:
1.99 -\[\forall{i \in \mathbb{N}}: M_{Voc(\varphi)} = M(i) \cap Voc(\varphi)\]
1.100 +\[\forall{i \in \mathbb{N}_0}: M_{Voc(\varphi)} = M(i) \cap Voc(\varphi)\]
1.101 \end{def:vocabulary}
1.102
1.103 \begin{prop:vocabulary sat}
1.104 Let $M$ be a model and $\varphi$ a LTL-formula, then following holds:
1.105 -\[\forall{i \in \mathbb{N}}: M,i \models \varphi \iff M_{Voc(\varphi)},i \models \varphi\]
1.106 +\[\forall{i \in \mathbb{N}_0}: M,i \models \varphi \iff M_{Voc(\varphi)},i \models \varphi\]
1.107 \end{prop:vocabulary sat}
1.108
1.109 +\subsection*{Derived connectives}
1.110 +For a more convenient description of system specifications we present some derived symbols to be used in LTL-formulae. At first we introduce the notion of \emph{truth} and \emph{falsity} using constants $\top$ and $\bot$. Then we expand our set of connectives with the Boolean \emph{and}, \emph{implication} and \emph{equivalence}. And at last we derive the commonly used modal operators \emph{eventually} and \emph{henceforth}. Let $\varphi$ and $\psi$ be $L_{LTL}(P)$-formulae:
1.111 +\begin{multicols}{2}
1.112 +\begin{itemize}
1.113 +\item $\top \equiv p \lor \neg p$ for $p \in P$
1.114 +\item $\bot \equiv \neg \top$
1.115 +\item $\varphi \land \psi \equiv \neg (\neg \varphi \lor \neg \psi)$
1.116 +\item $\varphi \rightarrow \psi \equiv \neg \varphi \lor \psi$
1.117 +\item $\varphi \leftrightarrow \psi \equiv (\varphi \rightarrow \psi) \land (\psi \rightarrow \varphi)$
1.118 +\item $\Diamond \varphi \equiv \top U \varphi$
1.119 +\item $\Box \varphi \equiv \neg \Diamond \neg \varphi$
1.120 +\end{itemize}
1.121 +\end{multicols}
1.122 +
1.123 \section{Model checking}
1.124 +
1.125 \begin{thebibliography}{99}
1.126 \bibitem{ref:ltl&büchi}
1.127 \uppercase{M{\footnotesize adhavan} M{\footnotesize ukund}.}