О задаче минимизации последовательных программ

Моделирование и анализ информационных систем. 2017. Т. 24. № 4. С. 415–433.

Zakharov V., Жайлауова Ш. Р.

rst-order program schemata is one of the simplest models of sequential imperative
programs intended for solving verication and optimization problems. We consider the decidable rela-
tion 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 rst-order program schemata supplied with logical-thermal equivalence and nite state determinis-
tic 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 rst-
order program schemata such that their minimization can be performed in polynomial time by means
of known techniques for minimization of nite state transducers operating over semigroups. Finally, we
demonstrate that in general case the minimization problem for nite state transducers over semigroups
may have several non-isomorphic solutions.

Keywords: эквивалентность, полугруппа, компьютерная программа, минимизация, equivalence, semigroup, автомат, minimization problem, program, finite automaton

Publication based on the results of: Synthesis and analysis of process models (2017)