On the Minimization of Finite State Trans- ducers over Semigroups - V. A. Zakharov; G. G. Temerbekova (Моделирование и анализ информационных систем)
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 veriﬁcation of such programs can be reduced to minimization and equivalence checking problems for ﬁnite state transducers. Minimization of a transducer over a semigroup is performed in three stages. At ﬁrst 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 ﬁnally a minimization algorithm for ﬁnite state automata is applied to the reduced transducer.