Iterating transducers

Abstract

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 T* for its transitive closure. In this paper we give a partial algorithm to compute a finite-state transducer T* for a general class of transducers. The construction builds a quotient of an underlying infinite-state transducer T