1.1 --- a/paper/src/paper.tex Sun Jul 10 00:42:42 2011 +0200
1.2 +++ b/paper/src/paper.tex Mon Jul 11 03:04:11 2011 +0200
1.3 @@ -24,6 +24,7 @@
1.4 \newcommand{\U}{\mathcal{U}}
1.5 \newcommand{\V}{\mathcal{V}}
1.6 \newcommand{\dnf}{\mathsf{dnf}}
1.7 +\newcommand{\consq}{\mathsf{consq}}
1.8
1.9 \title{\uppercase{\textbf{\Large{A}\large{lgorithmic} \Large{V}\large{erification of} \Large{R}\large{eactive} \Large{S}\large{ystems}}\\
1.10 \tiny{Draft}
1.11 @@ -57,8 +58,10 @@
1.12 \newtheorem*{def:atoms}{Atoms}
1.13 \newtheorem*{def:rep function}{Representation function}
1.14 \newtheorem*{def:next}{Next function}
1.15 -\newtheorem*{def:dnf}{Dijunctive normal form}
1.16 +\newtheorem*{def:dnf}{Disjunctive normal form}
1.17 \newtheorem*{def:positive formulae}{Positive formulae}
1.18 +\newtheorem*{def:consq}{Logical consequences}
1.19 +\newtheorem*{def:partial automata}{Partial automata}
1.20
1.21 \theoremstyle{plain}
1.22 \newtheorem{prop:vocabulary sat}{Proposition}[section]
1.23 @@ -71,6 +74,7 @@
1.24 \newtheorem{cor:mod=program language}[cor:mod=model language]{Corollary}
1.25 \newtheorem{thm:model checking}{Theorem}[section]
1.26 \newtheorem{lem:dnf}{Lemma}[section]
1.27 +\newtheorem{lem:consq}[lem:dnf]{Lemma}
1.28
1.29 \begin{document}
1.30 \maketitle
1.31 @@ -78,7 +82,7 @@
1.32 %\itshape
1.33 %\renewcommand\abstractname{Abstract}
1.34 \begin{abstract}
1.35 -Algorithmic verification is a successful application of automated temporal reasoning based on automata-theoretic model checking. We use the power of modal logics to specify computational properties. The verification of reactive systems provides a correctness proof for the program design with respect to such properties. The methods used are a composition of automata theory, graph theory and modal logics. This text is an introduction to such automata theoretic constructions and space-efficient on-the-fly verification methods for reactive systems.
1.36 +Algorithmic verification is a successful application of automated temporal reasoning based on automata-theoretic model checking. We use the power of modal logics to specify computational properties. System verification provides a correctness proof for the program design with respect to such properties. The methods used are a composition of automata theory, graph theory and modal logics. This text is an introduction to such automata theoretic constructions and space-efficient on-the-fly verification methods for reactive systems.
1.37 %Algorithmic verification of reactive systems is based on automata-theoretic model checking. Linear temporal logic accommodates the capability for the characterisation of program specifications. For formulae composed in linear temporal logic, it is possible to construct B\"uchi automata constituting the model space of the specification. The verification of reactive systems is composed of such constructions and intersections of the program and specification automata. This paper provides an introduction to the construction techniques of such automata and space-efficient on-the-fly verification methods for reactive systems.
1.38 \end{abstract}
1.39 %\normalfont
1.40 @@ -226,6 +230,8 @@
1.41 \subsection{Derived connectives}
1.42 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.43
1.44 +In anticipation of section \ref{sec:on-the-fly methods}, we extend our logic's syntax with the binary connective $\V$, which will become useful in the interpretation known as the \emph{two-state semantics}.
1.45 +
1.46 Let $\varphi$ and $\psi$ be $L_{LTL}(\Prop)$-formulae:
1.47 \begin{multicols}{2}
1.48 \begin{itemize}
1.49 @@ -236,6 +242,7 @@
1.50 \item $\varphi \leftrightarrow \psi \equiv (\varphi \rightarrow \psi) \land (\psi \rightarrow \varphi)$
1.51 \item $\Diamond \varphi \equiv \top \U \varphi$
1.52 \item $\Box \varphi \equiv \neg \Diamond \neg \varphi$
1.53 +\item $\varphi \V \psi \equiv \neg(\neg \varphi \U \psi)$
1.54 \end{itemize}
1.55 \end{multicols}
1.56 \noindent From the derivations for operators $\Diamond$, \emph{read diamond}, and $\Box$, \emph{read box}, it follows:
1.57 @@ -262,21 +269,26 @@
1.58 \end{def:rep function}
1.59
1.60 \begin{def:fs closure}
1.61 +\label{def:fs closure}
1.62 Let $\varphi$ be an LTL-formula, then the \emph{Fischer-Ladner closure} $CL(\varphi)$ of $\varphi$ is the smallest set of formulae such that following holds:
1.63 %\begin{multicols}{2}
1.64 \begin{itemize}
1.65 +\begin{multicols}{2}
1.66 \item $\varphi \in CL(\varphi)$
1.67 \item $\neg \psi \in CL(\varphi) \implies \psi \in CL(\varphi)$
1.68 \item $\psi \in CL(\varphi) \implies \neg \psi \in CL(\varphi)$
1.69 \item $\psi \lor \chi \in CL(\varphi) \implies \psi, \chi \in CL(\varphi)$
1.70 \item $\X \psi \in CL(\varphi) \implies \psi \in CL(\varphi)$
1.71 +\item $\psi \V \chi \in CL(\varphi) \implies \psi, \chi \in CL(\varphi)$
1.72 +\end{multicols}
1.73 +\vspace{-1.1em}
1.74 \item $\psi \U \chi \in CL(\varphi) \implies \psi, \chi, \X(\psi \U \chi) \in CL(\varphi)$
1.75 \end{itemize}
1.76 %\end{multicols}
1.77 \end{def:fs closure}
1.78
1.79 \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.80 -\[\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.81 +\[\mathbb{U}_\varphi = \{\psi \U \chi \mid \psi \U \chi \in CL(\varphi)\} \text{ and } \mathbb{U}_{\varphi_i} \text{ denotes the $i^{th}$ element of } \mathbb{U_\varphi}\]
1.82
1.83 \begin{def:atoms}
1.84 Let $\varphi$ be a formula and $CL(\varphi)$ its closure. $A \subseteq CL(\varphi)$ is an \emph{atom} if following holds:
1.85 @@ -296,7 +308,7 @@
1.86 %\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.87 \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.88 %\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.89 -\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.90 +\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 \leq |\mathbb{U}_{\varphi}|$
1.91 %Let $A, B \in \mathbb{AT}$ and $P \subseteq Voc(\varphi)$. Then $(A, P, B) \in \Delta$ iff the following holds:
1.92 %$P = A \cap Voc(\varphi)$ and For all $\X \psi \in CL(\varphi): \X \psi \in A$ iff $\psi \in B$.
1.93 \end{itemize}
1.94 @@ -326,6 +338,7 @@
1.95 \item $S_0 = \{s_0\}$
1.96 \item $F = S$
1.97 \end{multicols}
1.98 +\vspace{-1.1em}
1.99 \item $\Delta = \{(s, V(s), s') \mid \exists{a \in \Prop}: (s, a, s') \in R\}$
1.100 \end{itemize}
1.101 In practical verification of programs, the specification covers only the properties of a system, which are vital to the program's correctness, where our program description contains all details of all possible execution paths. Let $\varphi$ be the specification formula, we can reduce the state exploration to the vocabulary of $\varphi$ by the reduction of the transition relation to $\Delta = \{(s, A, s') \mid \exists{a \in \Prop}: (s, a, s') \in R \land A = V(s) \cap Voc(\varphi)\}$.
1.102 @@ -365,12 +378,13 @@
1.103 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.104
1.105 \section{On-the-fly methods}
1.106 +\label{sec:on-the-fly methods}
1.107 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.108
1.109 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.110
1.111 \begin{def:positive formulae}
1.112 -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.113 +Let $\Prop$ be a set of atomic propositions and let $\overline{\Prop} = \{\neg p \mid p \in \Prop\}$. We define the set of LTL-formulae in \emph{positive form}:
1.114 \[\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.115 \end{def:positive formulae}
1.116
1.117 @@ -380,7 +394,7 @@
1.118 \end{def:next}
1.119
1.120 \begin{def:dnf}
1.121 -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.122 +Let $\Phi^+$ be the set of LTL-formulae in positive form and let $Q = \Prop \cup \overline{\Prop} \cup next(\Phi^+)$. We define the function $\dnf: \Phi^+ \to 2^Q$ inductively:
1.123 \begin{align*}
1.124 &\dnf(\top) &= &\, \{\emptyset\}\\
1.125 &\dnf(\bot) &= &\, \emptyset\\
1.126 @@ -393,10 +407,50 @@
1.127 \end{def:dnf}
1.128
1.129 \begin{lem:dnf}
1.130 -Let $\Phi^+$ be the set of formulae in positive form, following holds:
1.131 +Let $\Phi^+$ be the set of formulae in positive form then following holds:
1.132 \[\forall{\varphi \in \Phi^+}: \varphi \iff \bigvee_{D \in \dnf(\varphi)} \bigwedge D\]
1.133 \end{lem:dnf}
1.134
1.135 +\begin{def:consq}
1.136 +Let $C \subseteq CL(\varphi)$, then $\consq(C)$ is the smallest subset of $CL(\varphi)$ such that following holds:
1.137 +\begin{itemize}
1.138 +%\begin{tabular}{ll}
1.139 +\begin{multicols}{2}
1.140 +\item $C \subseteq \consq(C)$
1.141 +\item $\top \in \consq(C)$, if $\top \in CL(\varphi)$
1.142 +\end{multicols}
1.143 +\vspace{-1.1em}
1.144 +\item $\psi \lor \chi \in \consq(C)$, if $\psi \lor \chi \in CL(\varphi)$ and $\psi \in \consq(C) \lor \chi \in \consq(C)$
1.145 +\item $\psi \land \chi \in \consq(C)$, if $\psi \land \chi \in CL(\varphi)$ and $\psi, \chi \in \consq(C)$
1.146 +\item $\psi \U \chi \in \consq(C)$, if $\psi \U \chi \in CL(\varphi)$ and $\psi, \X(\psi \U \chi) \in \consq(C) \lor \chi \in \consq(C)$
1.147 +\item $\psi \V \chi \in \consq(C)$, if $\psi \V \chi \in CL(\varphi)$ and $\psi, \X(\psi \U \chi) \in \consq(C) \lor \psi, \chi \in \consq(C)$
1.148 +%\end{tabular}
1.149 +\end{itemize}
1.150 +\end{def:consq}
1.151 +
1.152 +\begin{lem:consq}
1.153 +Let $\psi \in CL(\varphi)$, let $C, D \subseteq CL(\varphi)$ and let $\M$ be a model, then following holds:
1.154 +\begin{itemize}
1.155 +\begin{multicols}{2}
1.156 +\item $\consq(C) \subseteq \consq(D)$, if $C \subseteq D$
1.157 +\item $\psi \in \consq(C)$, if $C \in \dnf(\psi)$
1.158 +\item $\psi \in \consq(D)$, if $\psi \in C \land D \in \dnf(\bigwedge C)$
1.159 +\item $\M,0 \models \bigwedge \consq(C)$, if $\M,0 \models \bigwedge C$
1.160 +\end{multicols}
1.161 +\end{itemize}
1.162 +\end{lem:consq}
1.163 +
1.164 +\begin{def:partial automata}
1.165 +Let $\varphi$ be a formula with its disjunctive normal form $\dnf(\varphi)$ and let $Q = \Prop \cup \overline{\Prop} \cup next(CL(\varphi))$. Again we use the subset $\mathbb{U}_\varphi \subseteq CL(\varphi)$ of \emph{until}-formulae of the closure as defined in \ref{def:fs closure}. We define the \emph{partial automaton} $\A_\varphi = (\Sigma, S, S_0, \Delta, \{F_i\})$ with:
1.166 +\begin{itemize}
1.167 +\item $\Sigma = 2^{Voc(\varphi)}$
1.168 +\item $S = 2^Q$
1.169 +\item $S_0 = \dnf(\varphi)$
1.170 +\item $\Delta = \{(A, P, B) \mid \A \cap \Prop \subseteq P$ and $\{p \mid \neg p \in A\} \cap P = \emptyset$ and $B \in \dnf(\bigwedge snext(A)) \}$
1.171 +\item $F_i = \{A \in S \mid \psi \U \chi = \mathbb{U}_{\varphi_i}$ and $\psi \U \chi \notin \consq(A) \lor \chi \in \consq(A) \}$
1.172 +\end{itemize}
1.173 +\end{def:partial automata}
1.174 +
1.175 \begin{thebibliography}{99}
1.176 \bibitem{ref:ltl&büchi}
1.177 \uppercase{M{\footnotesize adhavan} M{\footnotesize ukund}.}