On the minimization and equivalence checking of sequential reactive systems

Finite state transducers over semigroups can be regarded as a formal model of sequential reactive programs. In some cases verification of such programs can be reduced to minimization and equivalence checking problems for this model of computation. To solve efficiently these problems certain requirements are imposed on a semigroup these transducers operate on. 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 a transducer, next a 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. As a byproduct of this minimization technique we obtain an equivalence checking procedure for transducers operating on certain classes of semigroups.