Iterating transducers

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 system's transitional semantics consequently can be modeled by finite-state transducers. A standard problem for infinite state systems is how to explore all states in a finite amount of time. When the initial states of a system are represented by a finite-state automaton. A and the one-step transition relation by a finite-state transducer this problem amounts to effectively computing an appropriate finite-state representation T{*} o A for the transduction of A under T's 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-