On the application of equivalence checking algorithms for program minimization

Equivalence checking algorithms found vast applications in system programming; they are used in software refactoring, security checking, malware detection, program integration, regression verification, compiler verification and validation. In this paper we show that equivalence checking procedures can be utilized for the development of global optimization transformation of programs. We consider minimization problem for two formal models of programs: deterministic finite state transducers over finitely generated decidable groups that are used as a model of sequential reactive programs, and deterministic program schemata that are used as a model of sequential imperative programs. Minimization problem for both models of programs can be solved following the same approach that is used for minimization of finite state automata by means of two basic optimizing transformations, namely, removing of useless states and joining equivalent states. The main results of the paper are Theorems 1 and 2.
Theorem 1. If $G$ is a finitely generated group and the word problem in $G$ is decidable in polynomial time then minimization problem for finite state deterministic transducers over $G$ is decidable in polynomial time as well.
Theorem 2. If $S$ is a decidable left-contracted ordered semigroup of basic program statements and the word problem in $S$ is decidable in polynomial time then minimization problem for program schemata operating on the interpretation over $S$ is decidable in polynomial time as well.