Loading
December 2003
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.
Available as Postscript (856 kB), PDF (391 kB), and compressed Postscript (292 kB)
Download BibTeX entry.