Partial Projection of Sets Represented by Finite Automata, with Application to State-Space Visualization?

Abstract. This work studies automata-based symbolic data structures for representing infinite sets. Such structures are used in particular by verification tools in order to represent the sets of configurations han-dled during symbolic exploration of infinite state spaces. Our goal is to develop an efficient projection operator for these representations. There are several needs for such an operator during state-space exploration; we focus here on projecting the set of reachable configurations obtained at the end of exploration. An interesting application is the state-space visu-alization problem, which consists in providing the user with a graphical picture of a relevant fragment of the reachable state space. For theoretical reasons, the projection of automata-represented sets is inherently costly. The contribution of this paper is to introduce an im-proved automata-based data structure that makes it possible to reduce in several cases the effective cost of projection. The idea is twofold. First, our structure allows to apply projection to only a part of an automaton, in cases where a full computation is not necessary. Second, the structure is able to store the results of past projection operations, and to reuse them in order to speed up subsequent computations. We show how our structure can be applied to the state-space visualization problem, and discuss some experimental results.