Verifying Systems with Infinite but Regular State Spaces

Thanks to the development of a number of efficiency enhancing
techniques, state-space exploration based verification, and in
particular model checking, has been quite successful for finite-state
systems. This has prompted efforts to apply a similar approach to
systems with infinite state spaces. Doing so amounts to developing
algorithms for computing a symbolic representation of the infinite
state space, as opposed to requiring the user to characterize the
state space by assertions. Of course, in most cases, this can only be
done at the cost of forgoing any general guarantee of success. The
goal of this paper is to survey a number of results in this area and
to show that a surprisingly common characteristic of the systems that
can be analyzed with this approach is that their state space
can be represented as a regular language.