Iterating transducers

Dennis Dams, Yassine Lakhnech and Martin Steffen

To appear at 13th Conference on Computer-Aided Verification (CAV01), Paris, France, 18-22 July 2001


Regular languages have proved useful for the symbolic state exploration of infinite state systems. They can be used to represent infinite sets of system configurations; the transitional semantics of the system consequently can be modeled by finite-state transducers. A standard problem encountered when doing symbolic state exploration for infinite state systems is how to explore all states in a finite amount of time. When representing the one-step transition relation of a system by a finite-state transducer $\T$, this problem boils down to finding an appropriate finite-state representation $\Tmany$ for its transitive closure. In this paper we give a partial algorithm to compute a finite-state transducer $\Tmany$ for a general class of transducers, including transducers that are not length-preserving. The construction builds a quotient of an underlying infinite-state transducer $\Tmanyinfinite$, using a novel behavioural equivalence that is based \emph{past} and \emph{future} bisimulations computed on finite approximations of $\Tmanyinfinite$. The extrapolation to $\Tmanyinfinite$ of these finite bisimulations capitalizes on the structure of the states of $\Tmanyinfinite$, which are strings of states of $\T$. We show how this extrapolation may be rephrased as a problem of detecting \emph{confluence} properties of rewrite systems that represent the bisimulations. Thus, we can draw upon techniques that have been developed in the area of rewriting. As in general, $\Tmanyinfinite$ is not representable by a finite-state transducer, the construction may not terminate. Nevertheless our implementation is able to calculate the transitive closure on examples investigated by related symbolic techniques in the literature.

Server START Conference Manager
Update Time 28 Mar 2001 at 08:36:01
Start Conference Manager
Conference Systems