Predicate abstraction is a technique used for verification of
infinite-state systems. Methods for automatic construction of a
sufficiently precise abstraction are in general incomplete. Therefore, it
is worth identifying classes of systems for which iterative predicate
refinement is guaranteed to converge.
We study the class of well-structured transition systems, which is a
large class that contains many infinite-state models used in practice.
These are systems, for which a well-quasi ordering on the set of states
that is compatible with the transition relation exists. We consider two
classes: WSTS (well-structured transition systems) and WSLTS
(well-structured labeled transition systems), which differ in the notion
of compatibility, and we focus on the coverability problem - checking
reachability of an upward-closed set of error states. We present two
instantiations of the standard schema for forward abstract reachability
analysis with predicate refinement. One of them uses the classical
refinement based on computation of predecessors and we prove completeness
for WSLTS, which is a proper extension of the class of systems with finite
trace-equivalence for which this refinement is known to be complete. For
the more general class of WSTS we propose a new refinement operator and
prove completeness of the method for this class. Our main result is the
completeness of predicate abstraction refinement for these two classes.
The advantage of this approach for checking coverability for
well-structured systems is that not only the reachability analysis is
forward, but also the refinement is performed locally and takes into
account the abstract counterexample.