1.1 --- a/paper/src/paper.tex Tue Jun 28 14:49:59 2011 +0200
1.2 +++ b/paper/src/paper.tex Tue Jun 28 22:03:45 2011 +0200
1.3 @@ -9,14 +9,15 @@
1.4 %\usepackage{fullpage}
1.5 %\usepackage[T1]{fontenc}
1.6 %\usepackage{arev}
1.7 -
1.8 %\pagestyle{headings}
1.9 \renewcommand{\familydefault}{\sfdefault}
1.10 +\newcommand{\M}{\mathcal{M}}
1.11 +\newcommand{\N}{\mathbb{N}_0}
1.12 \title{\uppercase{\textbf{\Large{A}\large{lgorithmic} \Large{V}\large{erification of} \Large{R}\large{eactive} \Large{S}\large{ystems}}\\
1.13 \tiny{Draft}
1.14 }}
1.15 \author{
1.16 -\uppercase{{\small{E}\scriptsize{UGEN} \small{S}\scriptsize{AWIN}}\\
1.17 +\uppercase{{\small{E}\scriptsize{UGEN} \small{S}\scriptsize{AWIN}}\thanks{\texttt{sawine@informatik.uni-freiburg.de}}\\
1.18 {\em \small{U}\scriptsize{NIVERSITY OF} \small{F}\scriptsize{REIBURG}}\\
1.19 %{\em \small{C}\scriptsize{omputer} \small{S}\scriptsize{cience} \small{D}\scriptsize{epartment}}\\
1.20 {\em \small{G}\scriptsize{ERMANY}}}\\
1.21 @@ -40,7 +41,6 @@
1.22 \newtheorem{prop:vocabulary sat}{Proposition}
1.23
1.24 \begin{document}
1.25 -
1.26 \maketitle
1.27 \thispagestyle{empty}
1.28 %\itshape
1.29 @@ -120,7 +120,7 @@
1.30 \end{def:regular languages closure}
1.31
1.32 \begin{def:infinite words}
1.33 -$\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.34 +$\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 : \N \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.35 \end{def:infinite words}
1.36
1.37 \begin{def:omega regular languages}
1.38 @@ -135,7 +135,6 @@
1.39 \end{itemize}
1.40 \end{def:omega regular languages closure}
1.41
1.42 -
1.43 \section{B\"uchi automata}
1.44 \begin{def:buechi automata}
1.45 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.46 @@ -146,19 +145,19 @@
1.47 \end{def:buechi automata}
1.48
1.49 \begin{def:automata runs}
1.50 -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.51 +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 : \N \to S$, where $\rho(i) = s_i$ denotes the state at the $i^{th}$ sequence position.
1.52 \end{def:automata runs}
1.53
1.54 \begin{def:automata acceptance}
1.55 -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.56 +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.57
1.58 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.59 \end{def:automata acceptance}
1.60
1.61 \section{Linear temporal logic}
1.62 \subsection*{Sytnax}
1.63 -Let $P$ be the countable set of \emph{atomic propositions}. The \emph{alphabet} of the language $L_{LTL}(P)$ is $P \cup \{\neg, \lor, X, U\}$. We define the $L_{LTL}(P)$-\emph{formulae} $\varphi$ using following productions:
1.64 -\[\varphi ::= p \in P \,|\, \neg \varphi \,|\, \varphi \lor \varphi \,|\, X \varphi \,|\, \varphi U \varphi\]
1.65 +Let $\mathcal{P}$ be the countable set of \emph{atomic propositions}. The \emph{alphabet} of the language $L_{LTL}(\mathcal{P})$ is $\mathcal{P} \cup \{\neg, \lor, X, U\}$. We define the $L_{LTL}(\mathcal{P})$-\emph{formulae} $\varphi$ using following productions:
1.66 +\[\varphi ::= p \in \mathcal{P} \,|\, \neg \varphi \,|\, \varphi \lor \varphi \,|\, X \varphi \,|\, \varphi U \varphi\]
1.67
1.68 \subsection*{Interpretation}
1.69 The intuition should go as follows: $\neg$ and $\lor$ correspond to the Boolean \emph{negation} and \emph{disjunction}, the unary temporal operator $X$ reads as \emph{next} and the binary temporal operator $U$ reads as \emph{until}.
1.70 @@ -166,43 +165,45 @@
1.71 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.72
1.73 \subsection*{Semantics}
1.74 -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.75 +A \emph{model} is a function $\M: \N \to 2^\mathcal{P}$ over \emph{frame} $\mathcal{F}$. The frame constitutes a linear order over $\N$, 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 \mathcal{P}$ is \emph{true} at time instant $i$ iff $p \in \M(i)$.
1.76
1.77 -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.78 +A model $\M$ \emph{satisfies} an LTL-formula $\varphi$ at time instant $i$ is denoted by $\M,i \models \varphi$. Satisfiability of a formula $\varphi$ is defined inductively over the structure of $\varphi$:
1.79 \begin{itemize}
1.80 -\item $M,i \models p$ for $p \in P$ iff $p \in M(i)$
1.81 -\item $M,i \models \neg \varphi$ iff not $M,i \models \varphi$
1.82 -\item $M,i \models \varphi \lor \psi$ iff $M,i \models \varphi$ or $M,i \models \psi$
1.83 -\item $M,i \models X \varphi$ iff $M,i+1 \models \varphi$
1.84 -\item $M,i \models \varphi U \psi$ iff $\exists{k \geq i}: M,k \models \psi$ and $\forall{i \leq j < k}: M,j \models\varphi$
1.85 +\item $\M,i \models p$ for $p \in \mathcal{P}$ iff $p \in \M(i)$
1.86 +\item $\M,i \models \neg \varphi$ iff not $\M,i \models \varphi$
1.87 +\item $\M,i \models \varphi \lor \psi$ iff $\M,i \models \varphi$ or $\M,i \models \psi$
1.88 +\item $\M,i \models X \varphi$ iff $\M,i+1 \models \varphi$
1.89 +\item $\M,i \models \varphi U \psi$ iff $\exists{k \geq i}: \M,k \models \psi$ and $\forall{i \leq j < k}: \M,j \models\varphi$
1.90 \end{itemize}
1.91 -
1.92 +%
1.93 \begin{def:vocabulary}
1.94 -Let $\varphi$ be a LTL-formula over atomic propositions $P$, we define the \emph{vocabulary} $Voc(\varphi)$ of $\varphi$ inductively:
1.95 +Let $\varphi$ be a LTL-formula over atomic propositions $\mathcal{P}$, we define the \emph{vocabulary} $Voc(\varphi)$ of $\varphi$ inductively:
1.96 \begin{multicols}{2}
1.97 \begin{itemize}
1.98 -\item $Voc(p) = \{p\}$ for $p \in P$
1.99 +\item $Voc(p) = \{p\}$ for $p \in \mathcal{P}$
1.100 \item $Voc(\neg \varphi) = Voc(\varphi)$
1.101 \item $Voc(\varphi \lor \psi) = Voc(\varphi) \cup Voc(\psi)$
1.102 \item $Voc(X \varphi) = Voc(\varphi)$
1.103 \item $Voc(\varphi U \psi) = Voc(\varphi) \cup Voc(\psi)$
1.104 \end{itemize}
1.105 \end{multicols}
1.106 +%
1.107 +\noindent Let $\M$ be a model and $\varphi$ a LTL-formula, we define model $\M_{Voc(\varphi)}$:
1.108 +\[\forall{i \in \N}: \M_{Voc(\varphi)} = \M(i) \cap Voc(\varphi)\]
1.109 +\end{def:vocabulary}
1.110 +%
1.111 +\begin{prop:vocabulary sat}
1.112 +Let $\M$ be a model and $\varphi$ a LTL-formula, then following holds:
1.113 +\[\forall{i \in \N}: \M,i \models \varphi \iff \M_{Voc(\varphi)},i \models \varphi\]
1.114 +\end{prop:vocabulary sat}
1.115 +%
1.116 +\subsection*{Derived connectives}
1.117 +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}.
1.118
1.119 -Let $M$ be a model and $\varphi$ a LTL-formula, we define model $M_{Voc(\varphi)}$:
1.120 -\[\forall{i \in \mathbb{N}_0}: M_{Voc(\varphi)} = M(i) \cap Voc(\varphi)\]
1.121 -\end{def:vocabulary}
1.122 -
1.123 -\begin{prop:vocabulary sat}
1.124 -Let $M$ be a model and $\varphi$ a LTL-formula, then following holds:
1.125 -\[\forall{i \in \mathbb{N}_0}: M,i \models \varphi \iff M_{Voc(\varphi)},i \models \varphi\]
1.126 -\end{prop:vocabulary sat}
1.127 -
1.128 -\subsection*{Derived connectives}
1.129 -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.130 +Let $\varphi$ and $\psi$ be $L_{LTL}(\mathcal{P})$-formulae:
1.131 \begin{multicols}{2}
1.132 \begin{itemize}
1.133 -\item $\top \equiv p \lor \neg p$ for $p \in P$
1.134 +\item $\top \equiv p \lor \neg p$ for $p \in \mathcal{P}$
1.135 \item $\bot \equiv \neg \top$
1.136 \item $\varphi \land \psi \equiv \neg (\neg \varphi \lor \neg \psi)$
1.137 \item $\varphi \rightarrow \psi \equiv \neg \varphi \lor \psi$
1.138 @@ -212,11 +213,12 @@
1.139 \end{itemize}
1.140 \end{multicols}
1.141 From the derivations for operators $\Diamond$, \emph{read diamond}, and $\Box$, \emph{read box}, it follows:
1.142 +\begin{multicols}{2}
1.143 \begin{itemize}
1.144 -\item $M,i \models \Diamond \varphi$ iff $\exists{k \geq i}: M,k \models \varphi$
1.145 -\item $M,i \models \Box \varphi$ iff $\forall{k \geq i}: M,k \models \varphi$
1.146 +\item $\M,i \models \Diamond \varphi$ iff $\exists{k \geq i}: \M,k \models \varphi$
1.147 +\item $\M,i \models \Box \varphi$ iff $\forall{k \geq i}: \M,k \models \varphi$
1.148 \end{itemize}
1.149 -
1.150 +\end{multicols}
1.151 \section{Model checking}
1.152
1.153 \begin{thebibliography}{99}