This article is cited in 3 papers

On the minimization problem for sequential programs

V. A. Zakharov^a, Sh. R. Zhailauova<sup>b

a</sup> National Reserach University Higher School of Economics, Faculty of Computer Science, 20 Myasnitskaya ul., Moscow 101000, Russia
^b Lomonosov Moscow State University, Faculty of Computational Mathematics and Cybernetics, Leninskiye Gory, GSP-1, 1-52, Moscow 119991, Russia

Abstract: First-order program schemata is one of the simplest models of sequential imperative programs intended for solving verification and optimization problems. We consider the decidable relation of logical-thermal equivalence of 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 implies that the equivalence checking problem and the minimization problem for these transducers are also decidable. In addition, on the basis of the discovered relationship, we have found a subclass of first-order program schemata such that their minimization 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 general case the minimization problem for finite state transducers over semigroups may have several non-isomorphic solutions.

Keywords: sequential program, transducer, minimization, substitution, semigroup, equivalence.

UDC: 517.9

Received: 17.07.2017

DOI: 10.18255/1818-1015-2017-4-415-433

Bibliographic databases:

•