next.png up.png previous
Next: Implementation in CLP Up: An Overview of MSR(): Previous: Symbolic Representation via Constrained


A Symbolic Verification Procedure

The next step toward an effective verification procedure consists of defining a symbolic predecessor operator working on the assertional language according to the rich denotation described in the previous section. Let us first introduce the notion of unification between two multisets of atomic formulas (with distinct variables).


Firstly, given two atomic formulas $A=p(x_1,\ldots,x_k)$ and $B=q(y_1,\ldots,y_l)$, we use $A=B$ as a shorthand for the constraint $x_1=y_1\wedge\ldots\wedge x_k=y_k$, provided $p=q$ and $k=l$. Unification is defined then as follows.
\begin{definition}Let $ {\mathcal M} ={A_1\ \vert\ \ldots\ \vert\ A_n}\,:\,{\var...
...able}, $j_1,\ldots,j_n$\ being a permutation of
$1,\ldots,n$.
\end{definition}
Below, given $E$ (e.g., a rule, constraint, or constrained configuration) we call $E'$ a variant of $E$ if $E'$ is obtained applying a renaming $\iota$ to $E$, i.e. $E'=\iota(E)$ (a renaming is a mapping from variables of $E$ to fresh variables).
\begin{definition}[The ${\bf Pre}$\ Operator]
The operator ${\bf Pre}$\ is defi...
...cal A} \oplus {\mathcal N} \}.
\end{array}
\end{displaymath}
\end{definition}
Let us give an example of application.
\begin{example}
Consider the constrained configuration
\begin{displaymath}
p(...
...$\ (the empty multiset) when applying
${\bf Pre}$\ to ${\bf S}$.
\end{example}
The new operator enjoys the following property.
\begin{theorem}[\cite{Del02}]
Let $\langle { {\mathscr P} , {\mathscr C} , {\m...
...er). Then
$[\![{{\bf Pre}({\bf S})}]\!]=Pre([\![{{\bf S}}]\!])$.
\end{theorem}
In order to define a symbolic reachability algorithm, we still need a comparison operator between constrained configurations. We discuss next the general requirements it should satisfy.
\begin{definition}
Let $\langle { {\mathscr P} , {\mathscr C} , {\mathscr I} ...
...$M\sqsubseteq^mN$\ implies
$[\![{N}]\!]\subseteq[\![{M}]\!]$.
\end{definition}
Based on this definition, we can define a symbolic backward reachability procedure that we can use to check safety properties whose negation can be expressed via an upward closed set of configurations. We can rephrase the backward reachability algorithm (which is parametric on the constraint system $ {\mathscr C} $ and entailment relation $\sqsubseteq^m$) in our setting, as follows.
\begin{definition}
% latex2html id marker 1247
Given an $\mbox{MSR($\ {\math...
...he pseudo-code of the algorithm is given in Fig. \ref{SBRFig}.
\end{definition}
Figure 6: Symbolic Backward Reachability
\begin{figure}
\begin{displaymath}
\begin{array}{ll}
{\tt Procedure}~{\bf Pre...
...~~{\tt endwhile}\\
{\tt end.}
\end{array}
\end{displaymath}
\end{figure}
In general, the algorithm is not terminating, since it is possible to encode undecidable reachability problems (e.g. for two counter machines) as verification problems of generic $\mbox{MSR($\ {\mathscr C} $)}$ specifications. However, following [1,18], if we can prove that $\sqsubseteq^m$ is a well-quasi ordering, then the previous procedure turns out to be a complete algorithm to compute $Pre^*([\![{{\bf U}}]\!])$. In order to check that a safety properties holds we also need that the emptiness test for the intersection with the initial states is decidable.
next.png up.png previous
Next: Implementation in CLP Up: An Overview of MSR(): Previous: Symbolic Representation via Constrained
Giorgio Delzanno 2003-02-03