@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.}
}