On the Minimization Problem for Sequential Programs

Automatic Control and Computer Sciences. 2017. Vol. 51. No. 7. P. 689–700.

Zakharov V., Jaylauova S.

Translator: Zakharov V.

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 finitestate
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.

Keywords: semigroup, minimization problem, finite state transducer, equivalence checking, sequential program