On the minimization of finite state transducers over semigroups

Finite state transducers over semigroups are regarded as a formal model of sequential reactive programs that operate in the interaction with the environment. At receiving a piece of data a program performs a sequence of actions and displays the current result. Such programs usually arise at implementation of computer drivers, on-line algorithms, control procedures. In many cases verification of such programs can be reduced to minimization and equivalence checking problems for finite state transducers. Minimization of a transducer over a semigroup is performed in three stages. At first the greatest common left-divisors are computed for all states of the transducer, next the transducer is brought to a reduced form by pulling all such divisors “upstream”, and finally a minimization algorithm for finite state automata is applied to the reduced transducer.