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