On the Minimization Problem for Sequential Programsстатья
Информация о цитировании статьи получена из
Web of Science,
Scopus
Статья опубликована в журнале из списка Web of Science и/или Scopus
Дата последнего поиска статьи во внешних источниках: 20 марта 2018 г.
Аннотация: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.