Symbolic Methods for Exploring Infinite State Spaces

In this thesis, we introduce a general method for computing the
set of reachable states of an infinite-state system. The basic
idea, inspired by well-known state-space exploration methods for
finite-state systems, is to propagate reachability from the
initial state of the system in order to determine exactly which
are the reachable states. Of course, the problem being in
general undecidable, our goal is not to obtain an algorithm which
is guaranteed to produce results, but one that often produces
results on practically relevant cases.

Our approach is based on the concept of meta-transition, which is
a mathematical object that can be associated to the model, and
whose purpose is to make it possible to compute in a finite
amount of time an infinite set of reachable states. Different
methods for creating meta-transitions are studied. We also study
the properties that can be verified by state-space exploration,
in particular linear-time temporal properties.

The state-space exploration technique that we introduce relies on
a symbolic representation system for the sets of data values
manipulated during exploration. This representation system has
to satisfy a number of conditions. We give a generic way of
obtaining a suitable representation system, which consists of
encoding each data value as a string of symbols over some finite
alphabet, and to represent a set of values by a finite-state
automaton accepting the language of the encodings of the values
in the set. Finally, we particularize the general representation
technique to two important domains: unbounded FIFO buffers, and
unbounded integer variables. For each of those domains, we give
detailed algorithms for performing the required operations on
represented sets of values.