1.1 --- a/paper/src/paper.tex Thu Jun 30 02:06:23 2011 +0200
1.2 +++ b/paper/src/paper.tex Thu Jun 30 17:35:02 2011 +0200
1.3 @@ -14,10 +14,12 @@
1.4 %\pagestyle{headings}
1.5
1.6 \renewcommand{\familydefault}{\sfdefault}
1.7 +\renewenvironment{proof}{{\bfseries Proof.}}{}
1.8 \newcommand{\M}{\mathcal{M}}
1.9 \newcommand{\N}{\mathbb{N}_0}
1.10 \newcommand{\F}{\mathcal{F}}
1.11 \newcommand{\Prop}{\mathcal{P}}
1.12 +\newcommand{\A}{\mathcal{A}}
1.13
1.14 \title{\uppercase{\textbf{\Large{A}\large{lgorithmic} \Large{V}\large{erification of} \Large{R}\large{eactive} \Large{S}\large{ystems}}\\
1.15 \tiny{Draft}
1.16 @@ -31,7 +33,7 @@
1.17 }
1.18 \date{\textsc{\hfill}}
1.19
1.20 -\theoremstyle{definition} %plain, definition, remark, proposition, proof, corrolary
1.21 +\theoremstyle{definition} %plain, definition, remark, proof, corrolary
1.22 \newtheorem*{def:finite words}{Finite words}
1.23 \newtheorem*{def:infinite words}{Infinite words}
1.24 \newtheorem*{def:regular languages}{Regular languages}
1.25 @@ -47,11 +49,16 @@
1.26 \newtheorem*{def:frames}{Frames}
1.27 \newtheorem*{def:models}{Models}
1.28 \newtheorem*{def:satisfiability}{Satisfiability}
1.29 +\newtheorem*{def:fs closure}{Fischer-Ladner closure}
1.30 +\newtheorem*{def:atoms}{Atoms}
1.31
1.32 -\theoremstyle{proposition}
1.33 +\theoremstyle{plain}
1.34 \newtheorem{prop:vocabulary sat}{Proposition}[section]
1.35 \newtheorem{prop:general equiv}{Proposition}[section]
1.36
1.37 +\theoremstyle{plain}
1.38 +\newtheorem{thm:model language}{Theorem}[section]
1.39 +
1.40 \begin{document}
1.41 \maketitle
1.42 \thispagestyle{empty}
1.43 @@ -149,37 +156,37 @@
1.44
1.45 \section{B\"uchi automata}
1.46 \begin{def:buechi automata}
1.47 -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.48 +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.49
1.50 -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.51 +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.52
1.53 Within this text \emph{automaton} will refer to the non-deterministic B\"uchi automaton, unless otherwise noted.
1.54 \end{def:buechi automata}
1.55
1.56 \begin{def:automata runs}
1.57 -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.58 +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.59 \end{def:automata runs}
1.60
1.61 \begin{def:automata acceptance}
1.62 -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.63 +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.64
1.65 -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.66 +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.67
1.68 -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.69 +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.70 \end{def:automata acceptance}
1.71
1.72 \subsection{Generalised B\"uchi automata}
1.73 \begin{def:general automata}
1.74 -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.75 +A \emph{generalised B\"uchi automaton} is a tuple $\A = (\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.76 \end{def:general automata}
1.77
1.78 \begin{def:general acceptance}
1.79 -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.80 +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.81 \end{def:general acceptance}
1.82
1.83 \begin{prop:general equiv}
1.84 -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.85 -\[L(A) = \bigcap_{i < k} L(A_i)\]
1.86 +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.87 +\[L(\A) = \bigcap_{i < k} L(\A_i)\]
1.88 \end{prop:general equiv}
1.89 \noindent Intuitively follows the equivalance of the language recognition abilities of general and non-deterministic B\"uchi automata.
1.90
1.91 @@ -195,27 +202,28 @@
1.92
1.93 \subsection{Semantics}
1.94 \begin{def:frames}
1.95 -A LTL-\emph{frame} is a tuple $\F = (S, R)$, where $S = \{s_i \mid i \in \N\}$ is the set of states and $R = \{(s_i, s_{i+1}) \mid i \in \N\}$ the set of accessibility relations. Hence $S$ is an isomorphism of $\N$ and $R$ an isomorphism of the strict linear order $(\N, <)$, which corresponds to the linear progression of discrete time.
1.96 +An LTL-\emph{frame} is a tuple $\F = (S, R)$, where $S = \{s_i \mid i \in \N\}$ is the set of states and $R = \{(s_i, s_{i+1}) \mid i \in \N\}$ the set of accessibility relations. Hence $S$ is an isomorphism of $\N$ and $R$ an isomorphism of the strict linear order $(\N, <)$, which corresponds to the linear progression of discrete time.
1.97 \end{def:frames}
1.98
1.99 \begin{def:models}
1.100 -A LTL-\emph{model} is a tuple $\M = (\F, V)$, where $\F$ is a \emph{frame} and $V: S \to 2^\Prop$ a \emph{valuation function}. Intuitively we say $p \in \Prop$ is \emph{true} at time instant $i$ iff $p \in V(i)$.
1.101 +An LTL-\emph{model} is a tuple $\M = (\F, V)$, where $\F$ is a \emph{frame} and $V: S \to 2^\Prop$ a \emph{valuation function}. Intuitively we say $p \in \Prop$ is \emph{true} at time instant $i$ iff $p \in V(i)$.
1.102 %A \emph{model} is a function $\M: \N \to 2^\Prop$ over \emph{frame} $\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 \Prop$ is \emph{true} at time instant $i$ iff $p \in \M(i)$.
1.103 \end{def:models}
1.104
1.105 \begin{def:satisfiability}
1.106 A model $\M = (\F, V)$ \emph{satisfies} a 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.107 \begin{itemize}
1.108 -\item $\M,i \models p$ for $p \in \Prop$ iff $p \in V(i)$
1.109 -\item $\M,i \models \neg \varphi$ iff not $\M,i \models \varphi$
1.110 -\item $\M,i \models \varphi \lor \psi$ iff $\M,i \models \varphi$ or $\M,i \models \psi$
1.111 -\item $\M,i \models X \varphi$ iff $\M,i+1 \models \varphi$
1.112 -\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.113 +\item $\M,i \models p$ for $p \in \Prop \iff p \in V(i)$
1.114 +\item $\M,i \models \neg \varphi \iff$ not $\M,i \models \varphi$
1.115 +\item $\M,i \models \varphi \lor \psi \iff \M,i \models \varphi$ or $\M,i \models \psi$
1.116 +\item $\M,i \models X \varphi \iff \M,i+1 \models \varphi$
1.117 +\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.118 \end{itemize}
1.119 +
1.120 \end{def:satisfiability}
1.121
1.122 \begin{def:vocabulary}
1.123 -Let $\varphi$ be a LTL-formula over atomic propositions $\Prop$, we define the \emph{vocabulary} $Voc(\varphi)$ of $\varphi$ inductively:
1.124 +Let $\varphi$ be an LTL-formula over atomic propositions $\Prop$, we define the \emph{vocabulary} $Voc(\varphi)$ of $\varphi$ inductively:
1.125 \begin{multicols}{2}
1.126 \begin{itemize}
1.127 \item $Voc(p) = \{p\}$ for $p \in \Prop$
1.128 @@ -226,15 +234,15 @@
1.129 \end{itemize}
1.130 \end{multicols}
1.131 %
1.132 -\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.133 +\noindent Let $\M = (\F, V)$ be a model and $\varphi$ an LTL-formula, we define model $\M_{Voc(\varphi)} = (\F, V_{Voc(\varphi)})$ with:
1.134 \[\forall{i \in \N}: V_{Voc(\varphi)}(i) = V(i) \cap Voc(\varphi)\]
1.135 Henceforth, we will abbreviate $\M_{Voc(\varphi)}$ and $V_{Voc(\varphi)}$ with $\M_\varphi$ and $V_\varphi$ accordingly.
1.136 -%\noindent Let $\M$ be a model and $\varphi$ a LTL-formula, we define model $\M_{Voc(\varphi)}$:
1.137 +%\noindent Let $\M$ be a model and $\varphi$ an LTL-formula, we define model $\M_{Voc(\varphi)}$:
1.138 %\[\forall{i \in \N}: \M_{Voc(\varphi)} = \M(i) \cap Voc(\varphi)\]
1.139 \end{def:vocabulary}
1.140 %
1.141 \begin{prop:vocabulary sat}
1.142 -Let $\M$ be a model and $\varphi$ a LTL-formula, then following holds:
1.143 +Let $\M$ be a model and $\varphi$ an LTL-formula, then following holds:
1.144 \[\forall{i \in \N}: \M,i \models \varphi \iff \M_\varphi,i \models \varphi\]
1.145 \end{prop:vocabulary sat}
1.146 %
1.147 @@ -265,10 +273,59 @@
1.148 \[\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.149
1.150 \section{Automata construction}
1.151 -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.152 -\[Mod(\varphi) = \{V_\varphi^\rightarrow(\N) \mid \M_\varphi = (\F, V_\varphi) \land \M_\varphi,0 \models \varphi\}\]
1.153 +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 \emph{representation function} $rep: \M \to 2^\Prop$, which returns an infinite word representing the model $\M_\varphi = (\F, V_\varphi)$ over the ordered image $V_\varphi^\rightarrow(\N)$ of its validation function, i.e., $rep(\M_\varphi) = V_\varphi(0), V_\varphi(1), ...$.
1.154 +\[Mod(\varphi) = \{rep(\M_\varphi) \mid \M_\varphi = (\F, V_\varphi) \land \M_\varphi,0 \models \varphi\}\]
1.155 $Mod(\varphi)$ is the set of all infinite words, which represent models for $\varphi$.
1.156
1.157 +\begin{def:fs closure}
1.158 +Let $\varphi$ be an LTL-formula, then the \emph{Fischer-Ladner closure} $FL(\varphi)$ of $\varphi$ is the smallest set of formulae such that following holds:
1.159 +%\begin{multicols}{2}
1.160 +\begin{itemize}
1.161 +\item $\varphi \in FL(\varphi)$
1.162 +\item $\neg \psi \in FL(\varphi) \implies \psi \in FL(\varphi)$
1.163 +\item $\psi \in FL(\varphi) \implies \neg \psi \in FL(\varphi)$
1.164 +\item $\psi \lor \chi \in FL(\varphi) \implies \psi, \chi \in FL(\varphi)$
1.165 +\item $X \psi \in FL(\varphi) \implies \psi \in FL(\varphi)$
1.166 +\item $\psi U \chi \in FL(\varphi) \implies \psi, \chi, X(\psi U \chi) \in FL(\varphi)$
1.167 +\end{itemize}
1.168 +%\end{multicols}
1.169 +\end{def:fs closure}
1.170 +
1.171 +\noindent Let $FL(\varphi)$ be the closure of formula $\varphi$, we define a subset with the \emph{until}-formulae of the closure $\mathbb{U}_\varphi \subseteq FL(\varphi)$ where:
1.172 +\[\mathbb{U}_\varphi = \{\psi U \chi \in FL(\varphi)\} \text{ and } \mathbb{U}_{\varphi_i} \text{ denotes the $i^{th}$ element of } \mathbb{U_\varphi}\]
1.173 +
1.174 +\begin{def:atoms}
1.175 +Let $\varphi$ be a formula and $FL(\varphi)$ its closure. $\mathbb{A}_\varphi \subseteq FL(\varphi)$ is an \emph{atom} if following holds:
1.176 +\begin{itemize}
1.177 +\item $\forall{\psi \in FL(\varphi)}: \psi \in \mathbb{A}_\varphi \iff \neg \psi \notin \mathbb{A_\varphi}$
1.178 +\item $\forall{\psi \lor \chi \in FL(\varphi)}: \psi \lor \chi \in \mathbb{A}_\varphi \iff \psi \in \mathbb{A}_\varphi$ or $\chi \in \mathbb{A}_\varphi$
1.179 +\item $\forall{\psi U \chi \in FL(\varphi)}: \psi U \chi \in \mathbb{A}_\varphi \iff \chi \in \mathbb{A}_\varphi$ or $\psi, X(\psi U \chi) \in \mathbb{A_\varphi}$
1.180 +\end{itemize}
1.181 +We define the set of all atoms of formula $\varphi$ with $\mathbb{AT}_\varphi = \{\mathbb{A_\varphi} \subseteq FL({\varphi}) \mid \mathbb{A_\varphi} \text{ is an atom}\}$.
1.182 +\end{def:atoms}
1.183 +
1.184 +\noindent Now that we have the required ingredients, we begin with the construction of automaton $\A_\varphi$ for formula $\varphi$. Let $\A_\varphi = (\Sigma, S, S_0, \Delta, \{F_i\}_{i < k})$ with:
1.185 +\begin{itemize}
1.186 +\item $\Sigma = 2^{Voc(\varphi)}$
1.187 +\item $S = \mathbb{AT_\varphi}$
1.188 +\item $S_0 = \{\mathbb{A} \in \mathbb{AT_\varphi} \mid \varphi \in \mathbb{A}\}$
1.189 +%\item $(A, P, B) \in \Delta$ for $A, B \in \mathbb{AT_\varphi}$ and $P = A \cap Voc(\varphi) \iff (X \psi \in A \iff \psi \in B)$
1.190 +\item $\Delta = \{(\mathbb{A}, P, \mathbb{B}) \mid \mathbb{A}, \mathbb{B} \in \mathbb{AT_\varphi}, P = \mathbb{A} \cap Voc(\varphi), X \psi \in \mathbb{A} \iff \psi \in \mathbb{B}\}$
1.191 +\item $\forall{i \in \N, i < k = |\mathbb{U}_{FL(\varphi)}|}: F_i = \{\mathbb{A} \in \mathbb{AT}_\varphi \mid \psi U \chi \notin \mathbb{A}$ or $\chi \in \mathbb{A}\}$
1.192 +\item $F_i = \{\mathbb{A} \in \mathbb{AT}_\varphi \mid \psi U \chi = \mathbb{U}_{\varphi_i}, \psi U \chi \notin \mathbb{A}$ or $\chi \in \mathbb{A}\}$ and therefore $k = |\mathbb{U}_{\varphi}|$
1.193 +%Let $A, B \in \mathbb{AT}$ and $P \subseteq Voc(\varphi)$. Then $(A, P, B) \in \Delta$ iff the following holds:
1.194 +%$P = A \cap Voc(\varphi)$ and For all $X \psi \in CL(\varphi): X \psi \in A$ iff $\psi \in B$.
1.195 +\end{itemize}
1.196 +
1.197 +\begin{thm:model language}
1.198 +Let $\M_\varphi = (\F, V_\varphi)$ be a model and $rep(\M_\varphi)$ its infinite representation word, then following holds:
1.199 +\[\M_\varphi \in L(A_\varphi) \iff \M_\varphi,0 \models \varphi\]
1.200 +\end{thm:model language}
1.201 +\noindent
1.202 +\begin{proof}
1.203 +For the eloberate proof, consult \cite{ref:ltl&büchi}.
1.204 +\end{proof}
1.205 +
1.206
1.207 \section{Model checking}
1.208