Unification Problem for Finite State Parameterized Transducers

The unification problem for parameterized finite state machines consists in finding for two given automata such values of their parameters that these automata will compute the same transduction relations. This paper presents a quadratic time algorithm for computing the most general unifiers of parameterized deterministic finite state machines. This algorithm is based on the Martelli–Montanari unification algorithm for terms and the equivalence checking algorithm for deterministic finite state machines.