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 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 finitestate 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 <ω , using a novel behavioural equivalence that is based past and future bisimulations computed on finite approximations of T <ω . The extrapolation to ...

• Type: Conference
• Year: 2001
• Where: CAV
• Authors: Dennis Dams, Yassine Lakhnech, Martin Steffen
• Keywords: CAV 2001, Hardware, Infinite State Systems, Symbolic State Exploration, finite-state Transducer