1.1 --- a/paper/src/paper.tex Sat Jul 09 21:14:09 2011 +0200
1.2 +++ b/paper/src/paper.tex Sun Jul 10 00:02:03 2011 +0200
1.3 @@ -20,6 +20,10 @@
1.4 \newcommand{\F}{\mathcal{F}}
1.5 \newcommand{\Prop}{\mathcal{P}}
1.6 \newcommand{\A}{\mathcal{A}}
1.7 +\newcommand{\X}{\mathcal{X}}
1.8 +\newcommand{\U}{\mathcal{U}}
1.9 +\newcommand{\V}{\mathcal{V}}
1.10 +\newcommand{\dnf}{\mathsf{dnf}}
1.11
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 @@ -52,6 +56,9 @@
1.15 \newtheorem*{def:fs closure}{Closure}
1.16 \newtheorem*{def:atoms}{Atoms}
1.17 \newtheorem*{def:rep function}{Representation function}
1.18 +\newtheorem*{def:next}{Next function}
1.19 +\newtheorem*{def:dnf}{Dijunctive normal form}
1.20 +\newtheorem*{def:positive formulae}{Positive formulae}
1.21
1.22 \theoremstyle{plain}
1.23 \newtheorem{prop:vocabulary sat}{Proposition}[section]
1.24 @@ -63,6 +70,7 @@
1.25 \newtheorem{cor:mod=model language}{Corollary}[thm:model language]
1.26 \newtheorem{cor:mod=program language}[cor:mod=model language]{Corollary}
1.27 \newtheorem{thm:model checking}{Theorem}[section]
1.28 +\newtheorem{lem:dnf}{Lemma}[section]
1.29
1.30 \begin{document}
1.31 \maketitle
1.32 @@ -160,11 +168,11 @@
1.33
1.34 \section{Linear temporal logic}
1.35 \subsection{Syntax}
1.36 -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.37 -\[\varphi ::= p \in \Prop \,|\, \neg \varphi \,|\, \varphi \lor \varphi \,|\, X \varphi \,|\, \varphi U \varphi\]
1.38 +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.39 +\[\varphi ::= p \in \Prop \,|\, \neg \varphi \,|\, \varphi \lor \varphi \,|\, \X \varphi \,|\, \varphi \U \varphi\]
1.40
1.41 \subsection{Interpretation}
1.42 -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.43 +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.44
1.45 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.46
1.47 @@ -184,8 +192,8 @@
1.48 \item $\M,i \models p$ for $p \in \Prop \iff p \in V(i)$
1.49 \item $\M,i \models \neg \varphi \iff$ not $\M,i \models \varphi$
1.50 \item $\M,i \models \varphi \lor \psi \iff \M,i \models \varphi$ or $\M,i \models \psi$
1.51 -\item $\M,i \models X \varphi \iff \M,i+1 \models \varphi$
1.52 -\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.53 +\item $\M,i \models \X \varphi \iff \M,i+1 \models \varphi$
1.54 +\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.55 \end{itemize}
1.56
1.57 \end{def:satisfiability}
1.58 @@ -197,8 +205,8 @@
1.59 \item $Voc(p) = \{p\}$ for $p \in \Prop$
1.60 \item $Voc(\neg \varphi) = Voc(\varphi)$
1.61 \item $Voc(\varphi \lor \psi) = Voc(\varphi) \cup Voc(\psi)$
1.62 -\item $Voc(X \varphi) = Voc(\varphi)$
1.63 -\item $Voc(\varphi U \psi) = Voc(\varphi) \cup Voc(\psi)$
1.64 +\item $Voc(\X \varphi) = Voc(\varphi)$
1.65 +\item $Voc(\varphi \U \psi) = Voc(\varphi) \cup Voc(\psi)$
1.66 \end{itemize}
1.67 \end{multicols}
1.68 %
1.69 @@ -215,7 +223,7 @@
1.70 \end{prop:vocabulary sat}
1.71 %
1.72 \subsection{Derived connectives}
1.73 -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.74 +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.75
1.76 Let $\varphi$ and $\psi$ be $L_{LTL}(\Prop)$-formulae:
1.77 \begin{multicols}{2}
1.78 @@ -225,20 +233,20 @@
1.79 \item $\varphi \land \psi \equiv \neg (\neg \varphi \lor \neg \psi)$
1.80 \item $\varphi \rightarrow \psi \equiv \neg \varphi \lor \psi$
1.81 \item $\varphi \leftrightarrow \psi \equiv (\varphi \rightarrow \psi) \land (\psi \rightarrow \varphi)$
1.82 -\item $\Diamond \varphi \equiv \top U \varphi$
1.83 +\item $\Diamond \varphi \equiv \top \U \varphi$
1.84 \item $\Box \varphi \equiv \neg \Diamond \neg \varphi$
1.85 \end{itemize}
1.86 \end{multicols}
1.87 \noindent From the derivations for operators $\Diamond$, \emph{read diamond}, and $\Box$, \emph{read box}, it follows:
1.88 \begin{multicols}{2}
1.89 \begin{itemize}
1.90 -\item $\M,i \models \Diamond \varphi$ iff $\exists{k \geq i}: \M,k \models \varphi$
1.91 -\item $\M,i \models \Box \varphi$ iff $\forall{k \geq i}: \M,k \models \varphi$
1.92 +\item $\M,i \models \Diamond \varphi \iff \exists{k \geq i}: \M,k \models \varphi$
1.93 +\item $\M,i \models \Box \varphi \iff \forall{k \geq i}: \M,k \models \varphi$
1.94 \end{itemize}
1.95 \end{multicols}
1.96
1.97 \noindent With the additional derived connectives we get the following $L_{LTL}(\Prop)$-formulae productions:
1.98 -\[\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.99 +\[\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.100
1.101 \section{Automata construction}
1.102 Before applying the automata-theoretic verification methods, we need to construct the automaton for a given specification formula $\varphi$ and for the program $P$ in test.
1.103 @@ -260,21 +268,21 @@
1.104 \item $\neg \psi \in CL(\varphi) \implies \psi \in CL(\varphi)$
1.105 \item $\psi \in CL(\varphi) \implies \neg \psi \in CL(\varphi)$
1.106 \item $\psi \lor \chi \in CL(\varphi) \implies \psi, \chi \in CL(\varphi)$
1.107 -\item $X \psi \in CL(\varphi) \implies \psi \in CL(\varphi)$
1.108 -\item $\psi U \chi \in CL(\varphi) \implies \psi, \chi, X(\psi U \chi) \in CL(\varphi)$
1.109 +\item $\X \psi \in CL(\varphi) \implies \psi \in CL(\varphi)$
1.110 +\item $\psi \U \chi \in CL(\varphi) \implies \psi, \chi, \X(\psi \U \chi) \in CL(\varphi)$
1.111 \end{itemize}
1.112 %\end{multicols}
1.113 \end{def:fs closure}
1.114
1.115 \noindent Let $CL(\varphi)$ be the closure of formula $\varphi$, we define a subset with the \emph{until}-formulae of the closure $\mathbb{U}_\varphi \subseteq CL(\varphi)$ where:
1.116 -\[\mathbb{U}_\varphi = \{\psi U \chi \in CL(\varphi)\} \text{ and } \mathbb{U}_{\varphi_i} \text{ denotes the $i^{th}$ element of } \mathbb{U_\varphi}\]
1.117 +\[\mathbb{U}_\varphi = \{\psi \U \chi \in CL(\varphi)\} \text{ and } \mathbb{U}_{\varphi_i} \text{ denotes the $i^{th}$ element of } \mathbb{U_\varphi}\]
1.118
1.119 \begin{def:atoms}
1.120 Let $\varphi$ be a formula and $CL(\varphi)$ its closure. $A \subseteq CL(\varphi)$ is an \emph{atom} if following holds:
1.121 \begin{itemize}
1.122 \item $\forall{\psi \in CL(\varphi)}: \psi \in A \iff \neg \psi \notin A$
1.123 \item $\forall{\psi \lor \chi \in CL(\varphi)}: \psi \lor \chi \in A \iff \psi \in A$ or $\chi \in A$
1.124 -\item $\forall{\psi U \chi \in CL(\varphi)}: \psi U \chi \in A \iff \chi \in A$ or $\psi, X(\psi U \chi) \in A$
1.125 +\item $\forall{\psi \U \chi \in CL(\varphi)}: \psi \U \chi \in A \iff \chi \in A$ or $\psi, \X(\psi \U \chi) \in A$
1.126 \end{itemize}
1.127 We define the set of all atoms of formula $\varphi$ with $\mathbb{AT}_\varphi = \{A \subseteq CL({\varphi}) \mid A \text{ is an atom}\}$.
1.128 \end{def:atoms}
1.129 @@ -284,12 +292,12 @@
1.130 \item $\Sigma = 2^{Voc(\varphi)}$
1.131 \item $S = \mathbb{AT_\varphi}$
1.132 \item $S_0 = \{A \in \mathbb{AT_\varphi} \mid \varphi \in A\}$
1.133 -%\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.134 -\item $\Delta = \{(A, P, B) \mid A, B \in \mathbb{AT_\varphi}, P = A \cap Voc(\varphi), X \psi \in A \iff \psi \in B\}$
1.135 -%\item $\forall{i \in \N, i < k = |\mathbb{U}_{CL(\varphi)}|}: F_i = \{A \in \mathbb{AT}_\varphi \mid \psi U \chi \notin A$ or $\chi \in A\}$
1.136 -\item $F_i = \{A \in \mathbb{AT}_\varphi \mid \psi U \chi = \mathbb{U}_{\varphi_i}, \psi U \chi \notin A$ or $\chi \in A\}$ and therefore $k = |\mathbb{U}_{\varphi}|$
1.137 +%\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.138 +\item $\Delta = \{(A, P, B) \mid A, B \in \mathbb{AT_\varphi}, P = A \cap Voc(\varphi), \X \psi \in A \iff \psi \in B\}$
1.139 +%\item $\forall{i \in \N, i < k = |\mathbb{U}_{CL(\varphi)}|}: F_i = \{A \in \mathbb{AT}_\varphi \mid \psi \U \chi \notin A$ or $\chi \in A\}$
1.140 +\item $F_i = \{A \in \mathbb{AT}_\varphi \mid \psi \U \chi = \mathbb{U}_{\varphi_i}, \psi \U \chi \notin A$ or $\chi \in A\}$ and therefore $k = |\mathbb{U}_{\varphi}|$
1.141 %Let $A, B \in \mathbb{AT}$ and $P \subseteq Voc(\varphi)$. Then $(A, P, B) \in \Delta$ iff the following holds:
1.142 -%$P = A \cap Voc(\varphi)$ and For all $X \psi \in CL(\varphi): X \psi \in A$ iff $\psi \in B$.
1.143 +%$P = A \cap Voc(\varphi)$ and For all $\X \psi \in CL(\varphi): \X \psi \in A$ iff $\psi \in B$.
1.144 \end{itemize}
1.145
1.146 \begin{thm:model language}
1.147 @@ -303,7 +311,7 @@
1.148 \end{proof}
1.149 \begin{cor:mod=model language}
1.150 \label{cor:mod=model language}
1.151 -From theorem \ref{thm:model language} follows $Mod(\varphi) = L_\omega(\A_\varphi)$.
1.152 +From Theorem \ref{thm:model language} follows $Mod(\varphi) = L_\omega(\A_\varphi)$.
1.153 \end{cor:mod=model language}
1.154
1.155 \subsection{Program automata}
1.156 @@ -331,13 +339,13 @@
1.157 \[Mod(P) = \{\rho \mid \rho \text{ is a computation of } P\}\]
1.158 \begin{cor:mod=program language}
1.159 \label{cor:mod=program language}
1.160 -From theorem \ref{thm:model language} and proposition \ref{prop:computation set=language} follows $Mod(P) = L_\omega(\A_P)$.
1.161 +From Theorem \ref{thm:model language} and Proposition \ref{prop:computation set=language} follows $Mod(P) = L_\omega(\A_P)$.
1.162 \end{cor:mod=program language}
1.163
1.164 \section{Model checking}
1.165 For effective automata-theoretic verification of reactive programs, we have modelled the program as a non-deterministic B\"uchi automaton $\A_P$ and the specification formula $\varphi$ as automaton $\A_\varphi$.
1.166
1.167 -Given a program $P$ and specification $\varphi$, the verification problem is the following: \emph{does every run of P satisfy $\varphi$?} To show this we use the previously introduced automata constructions and reduce the problem to $L_\omega(\A_P) \subseteq L_\omega(\A_\varphi)$, i.e., all runs accepted by $\A_P$ are also accepted by $\A_\varphi$. By this problem definition, we clearly have to explore the whole state space of $\A_\varphi$ for each run of $\A_P$. This prevents efficient on-demand constructions. Therefore we rephrase the problem with the contrapositive definition $L_\omega(\A_P) \cap \overline{L_\omega(\A_\varphi)} = \emptyset$, where $\overline{L_\omega(\A_\varphi)} = \Sigma^\omega - L_\omega(\A_\varphi) = L_\omega(\A_{\neg \varphi})$ \cite{ref:alternating verification}.
1.168 +Given a program $P$ and specification $\varphi$, the verification problem is the following: \emph{does every run of $P$ satisfy $\varphi$?} To show this we use the previously introduced automata constructions and reduce the problem to $L_\omega(\A_P) \subseteq L_\omega(\A_\varphi)$, i.e., all runs accepted by $\A_P$ are also accepted by $\A_\varphi$. By this problem definition, we clearly have to explore the whole state space of $\A_\varphi$ for each run of $\A_P$. This prevents efficient on-demand constructions. Therefore we rephrase the problem with the contrapositive definition $L_\omega(\A_P) \cap \overline{L_\omega(\A_\varphi)} = \emptyset$, where $\overline{L_\omega(\A_\varphi)} = \Sigma^\omega - L_\omega(\A_\varphi) = L_\omega(\A_{\neg \varphi})$ \cite{ref:alternating verification}.
1.169
1.170 In conclusion, the essence of model checking lies within the test for emptyness of the intersection between the recognised language of the program automaton and the recognised language of the automaton for its negated specification:
1.171 \[L_\omega(\A_P) \cap L_\omega(\A_{\neg \varphi}) = \emptyset\]
1.172 @@ -347,15 +355,46 @@
1.173 Let $P$ be a finite-state program and $\A_P$ its automaton, let $\varphi$ be an LTL-formula and $\A_\varphi$ its automaton. P satisfies $\varphi$ iff $L_\omega(\A_P) \cap L_\omega(\A_{\neg \varphi}) = \emptyset$.
1.174 \end{thm:model checking}
1.175
1.176 -From corollary \ref{cor:mod=model language} and \ref{cor:mod=program language} follows:
1.177 +From Corollary \ref{cor:mod=model language} and \ref{cor:mod=program language} follows:
1.178 \[L_\omega(\A_P) \cap L_\omega(\A_{\neg \varphi}) = \emptyset \iff Mod(P) \cap Mod(\neg \varphi) = \emptyset\]
1.179
1.180 \subsection{Complexity}
1.181 -Let the size $|P|$ of a program $P = (S, s_0, R, V)$ be proportional to the sum of its structural components, i.e., $|P| = |S| + |R|$. The size $|\varphi|$ is the length of the formula string. The asymptotical complexity of the presented automata-theoretic verification method is in time $O(|P| \cdot 2^{O(|\varphi|)})$\cite{ref:concurrent checking}.
1.182 +Let the size $|P|$ of a program $P = (S, s_0, R, V)$ be proportional to the sum of its structural components, i.e., $|P| = |S| + |R|$. The size $|\varphi|$ is the length of the formula string. The asymptotical complexity of the presented automata-theoretic verification method is in time $O(|P| \cdot 2^{O(|\varphi|)})$ \cite{ref:concurrent checking}.
1.183
1.184 -The size of $\varphi$ is usually short \cite{ref:concurrent checking}, so the exponential growth by it is reasonable. Generally, the number of states is at least exponential in the size of its description by means of a programming language, meaning that despite that the upper bound is polynomial in the size of the program, in practice, we are facing exponential growth in complexity \cite{ref:handbook}.
1.185 +The size of $\varphi$ is usually short \cite{ref:concurrent checking}, so the exponential growth by it is reasonable. Generally, the number of states is at least exponential in the size of its description by means of a programming language. This concludes, that despite that the upper bound is polynomial in the size of the program, in practice, we are facing exponential growth in complexity \cite{ref:handbook}.
1.186
1.187 \section{On-the-fly methods}
1.188 +The automata-theoretic approach on verification in Theorem \ref{thm:model checking} requires a fully constructed automaton for the specification, when applying the graph-theoretic emptyness test.
1.189 +
1.190 +A more space-efficient strategy is the on-the-fly construction of the automaton during a depth-first search, short DFS. The DFS explores the product states of both automata incrementally, testing for cycles in each iteration. If the program does not satisfy a formula, an accepting cycle will occur and lead to termination of the search. In the case of a valid program, i.e., the program does meet the specification, no cycles will occur. In the latter case, such a strategy would inevitably explore the whole state space of the automata.
1.191 +
1.192 +\begin{def:positive formulae}
1.193 +Let $\Prop$ be a set of atomic propositions, let $\overline{\Prop} = \{\neg p \mid p \in \Prop\}$ and let us extend the LTL-syntax with the binary operator $\V$ with $\varphi \V \psi \equiv \neg(\neg \varphi \U \psi)$. We define the set of LTL-formulae in \emph{positive form}:
1.194 +\[\Phi^+ = \Prop \cup \overline{\Prop} \cup \{\top, \bot\} \cup \{\varphi \lor \psi, \varphi \land \psi, \X\varphi, \varphi \U \psi, \varphi \V \psi \mid \varphi, \psi \in \Phi^+\} \]
1.195 +\end{def:positive formulae}
1.196 +
1.197 +\begin{def:next}
1.198 +Let $\Phi$ be a set of LTL-formulae, we define:
1.199 +\[next(\Phi) = \{ \X\varphi \mid \X\varphi \in \Phi\} \text{ and } snext(\Phi) = \{ \varphi \mid \X\varphi \in \Phi\}\]
1.200 +\end{def:next}
1.201 +
1.202 +\begin{def:dnf}
1.203 +Let $\Phi^+$ be the set of LTL-formulae in positive form and let $Q = \Prop \cup \overline{\Prop} \cup next(\Phi^+)$, we define function $\dnf: \Phi^+ \to Q$ inductively:
1.204 +\begin{align*}
1.205 +&\dnf(\top) &= &\, \{\emptyset\}\\
1.206 +&\dnf(\bot) &= &\, \emptyset\\
1.207 +&\dnf(x) &= &\, \{\{x\}\}, \text{ for } x = p, \neg p, \X\varphi\\
1.208 +&\dnf(\varphi \lor \psi) &= &\, \dnf(\varphi) \cup \dnf(\psi)\\
1.209 +&\dnf(\varphi \land \psi) &= &\, \{C \cup D \mid C \in \dnf(\varphi), D \in \dnf(\psi), C \cup D \text{ is consistent}\}\\
1.210 +&\dnf(\varphi \U \psi) &= &\, \dnf(\varphi \land \X(\varphi \U \psi)) \cup \dnf(\psi)\\
1.211 +&\dnf(\varphi \V \psi) &= &\, \dnf(\varphi \land \psi) \cup \dnf(\psi \land \X(\varphi \V \psi))\\
1.212 +\end{align*}
1.213 +\end{def:dnf}
1.214 +
1.215 +\begin{lem:dnf}
1.216 +Let $\Phi^+$ be the set of formulae in positive form, following holds:
1.217 +\[\forall{\varphi \in \Phi^+}: \varphi \iff \bigvee_{D \in \dnf(\varphi)} \bigwedge D\]
1.218 +\end{lem:dnf}
1.219
1.220 \begin{thebibliography}{99}
1.221 \bibitem{ref:ltl&büchi}