@TechReport{ it:2003-065,
author = {Michael Baldamus and Richard Mayr and Gerardo Schneider},
title = {A Backward/Forward Strategy for Verifying Safety
Properties of Infinite-State Systems},
institution = {Department of Information Technology, Uppsala University},
department = {Division of Computer Systems},
year = {2003},
number = {2003-065},
month = dec,
abstract = {This paper has two main contributions: For one, we
describe a general method for verifying safety properties
of non-well-quasi-ordered infinite-state systems for which
reachability is undecidable in general, the question being
whether a set U of configurations is reachable. In many
cases this problem can be solved as follows: First, one
constructs a well-quasi-ordered overapproximation of the
system in question. Thereby one can compute an
overapproximation of the set Pre*(U) of all predecessors of
U. Second, one performs an exact bounded forward search for
U (starting at the initial state) which always stays inside
the already computed overapproximation of Pre*(U), thus
curbing the search space. This restricted forward search is
more efficient than a normal forward search, yielding
answers of the form YES, NO, or UNKNOWN, where the YES and
NO answers are always correct. As our second main
contribution herein, we apply our method to
relabelling-free CCS with finite summation, which is
already a process calculus for which reachability is
undecidable. To our knowledge, this part is actually the
first application of well-structered systems to verifying
safety properties in process calculi. The application is
done via a special Petri nets semantics for the calculus
that we consider.}
}