On the Minimization Problem for Sequential Programs

Abstract

First-order program schemata represent one of the most simple models of sequential imperative programs intended for solving verification and optimization problems. We consider the decidable relation of logical-thermal equivalence on these schemata and the problem of their size minimization while preserving logical-thermal equivalence. We prove that this problem is decidable. Further we show that the first-order program schemata supplied with logical-thermal equivalence and finite-state deterministic transducers operating over substitutions are mutually translated into each other. This relationship makes it possible to adapt equivalence checking and minimization algorithms developed in one of these models of computation to the solution of the same problems for the other model of computation. In addition, on the basis of the discovered relationship, we describe a subclass of first-order program schemata such that minimization of the program schemata from this class can be performed in polynomial time by means of known techniques for minimization of finite-state transducers operating over semigroups. Finally, we demonstrate that in the general case the minimization problem for finite state transducers over semigroups may have several non-isomorphic solutions.