On the use of Automata-based Techniques in Symbolic Model Checking
------------------------------------------------------------------

Checking infinite-state systems is frequently done by encoding
infinite sets of states as regular languages. Computing such a regular
representation of, say, the reachable set of states of a system
requires acceleration techniques that can finitely compute the effect
of an unbounded number of transitions. Among the acceleration
techniques that have been proposed, one finds both specific and
generic techniques. Specific techniques exploit the particular type of
system being analyzed, e.g. a system manipulating queues or integers,
whereas generic techniques only assume that the transition relation is
represented by a finite-state transducer, which has to be iterated.
In this paper, we survey two generic techniques that have been
presented in \cite{BLW03} and \cite{BLW04a}. Those techniques build on
earlier work, but exploits a number of new conceptual and algorithmic
ideas, often induced with the help of experiments, that give it a
broad scope, as well as good performance.