Automatic Control and Computer Sciences

, Volume 51, Issue 7, pp 689–700 | Cite as

On the Minimization Problem for Sequential Programs

  • V. A. ZakharovEmail author
  • S. R. Jaylauova


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.


sequential program transducer minimization substitution semigroup equivalence 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Glushkov, V.M. and Letichevsky, A.A., Theory of discrete transducers, Vopr. Algebry Logiki, 1973, pp. 5–39Google Scholar
  2. 2.
    Ershov, A.P., Reducing the problem of saving memory when making programs to the problem of graph vertex coloring, Dokl. Akad. Nauk SSSR, 1962, vol. 142, no. 4, pp. 785–787.MathSciNetGoogle Scholar
  3. 3.
    Ershov, A.P., Current state of the theory of program schemes, Probl. Kibern., 1973, vol. 27, pp. 87–110.Google Scholar
  4. 4.
    Zakharov, V.A. and Novikiva, T.A., A time-polynomial algorithm for verifying the logical-thermal equivalence of programs, Tr. Inst. Sist. Progr., 2012, vol. 22, no. 4, pp. 435–455.Google Scholar
  5. 5.
    Zakharov, V.A. and Podymov, V.V., Application of equivalence checking algorithms for program optimization, Tr. Inst. Sist. Progr., 2015, vol. 27, no. 3, pp. 145–174.Google Scholar
  6. 6.
    Zakharov, V.A. and Temerbekova, G.G., On the minimization and equivalence checking of sequential reactive systems, Syst. Inf., 2016, vol. 7, pp. 33–44.Google Scholar
  7. 7.
    Zakharov, V.A., Problemy ekvivalentnosti program: Modeli, algoritmy, slojnost (Program Equivalence Problems: Models, Algorithms, and Complexity), 2016, pp. 1–304Google Scholar
  8. 8.
    Itkin, V.E., Logical-thermal equivalence of programs, Kibernetika, 1972, no. 1, pp. 5–27.Google Scholar
  9. 9.
    Kotov, V.E. and Sabelfeld, V.K., Teoriya skhem program (Theory of Program Schemes), 1991, pp. 1–348Google Scholar
  10. 10.
    Krinickij, N.A., Ravnosil’nye preobrazovaniya algoritmov i programmirovanie (Equivalent Algorithm Transformations and Programming), 1970, pp. 1–210Google Scholar
  11. 11.
    Lavrov, S.S., About saving memory in closed operator schemes, Zh. Vychisl. Mat. Mat. Fiz., 1961, vol. 1, no. 4, pp. 15–19.Google Scholar
  12. 12.
    Lyapunov, A.A., About logical schemes of programs, Probl. Kibern., 1958, vol. 1, pp. 46–74.Google Scholar
  13. 13.
    Podlovchenko, R.I., Models of sequential programs used to study the functional equivalence of programs, Kibernetika, 1979, no. 1, pp. 20–28.MathSciNetzbMATHGoogle Scholar
  14. 14.
    Yanov, Yu.I., On logical schemes of algorithms, Probl. Kibern., 1958, vol. 1, pp. 75–127.MathSciNetzbMATHGoogle Scholar
  15. 15.
    Eder, E., Properties of substitutions and unifications, J. Symbolic Comput., 1985, vol. 1, no. 1, pp. 31–46.MathSciNetCrossRefzbMATHGoogle Scholar
  16. 16.
    Ershov, A.P., Alpha—an automatic programming system of high efficiency, J. Assoc. Comput. Mach., 1966, vol. 13, no. 1, pp. 17–24.CrossRefGoogle Scholar
  17. 17.
    Friedman, E.P., Equivalence problems for deterministic languages and monadic recursion schemes, J. Comput. Syst. Sci., 1977, vol. 14, no. 3, pp. 362–399.MathSciNetCrossRefGoogle Scholar
  18. 18.
    Harju, T. and Karhumaki, J., The equivalence of multi-tape finite automata, Theor. Comput. Sci., 1991, vol. 78, no. 2, pp. 347–355.CrossRefzbMATHGoogle Scholar
  19. 19.
    Luckham, D.C., Park, D.M., and Paterson, M.S., On formalized computer programs, J. Comput. Syst. Sci., 1970, vol. 4, no. 3, pp. 220–249.CrossRefzbMATHGoogle Scholar
  20. 20.
    Mohri, M., Minimization algorithms for sequential transducers, Theor. Comput. Sci., 2000, vol. 234, pp. 177–201.MathSciNetCrossRefzbMATHGoogle Scholar
  21. 21.
    Muchnick, S., Advanced Compiler Design and Implementation, 1997, pp. 1–856Google Scholar
  22. 22.
    Rutledge, J.D., Program schemata as automata, Proc. of the 11-th Annual Symposium on Switching and Automata Theory (SWAT 1970), 1970, pp. 7–24CrossRefGoogle Scholar
  23. 23.
    Sabelfeld, V.K., The logic-termal equivalence is polynomial-time decidable, Inf. Process. Lett., 1980, vol. 10, no. 2, pp. 57–62.MathSciNetCrossRefzbMATHGoogle Scholar
  24. 24.
    Senizergues, G., The equivalence problem for deterministic pushdown automata is decidable, Lect. Notes Comput. Sci., 1997, vol. 1256, pp. 271–281.MathSciNetGoogle Scholar
  25. 25.
    Shofrutt, C., Minimizing subsequential transducers: A survey, Theor. Comput. Sci., 2003, vol. 292, pp. 131–143.MathSciNetCrossRefzbMATHGoogle Scholar
  26. 26.
    Watson, B.W., A taxonomy of finite automata minimization algorithm, Comput. Sci. Rep., Eindhoven Univ. Technol., 2005, vol. 93, no. 44, pp. 1–32.Google Scholar
  27. 27.
    Zakharov, V.A., On the decidability of the equivalence problem for orthogonal sequential programs, Grammars, 1999, vol. 2, no. 3, pp. 271–281.MathSciNetCrossRefzbMATHGoogle Scholar
  28. 28.
    Zakharov, V.A., Equivalence checking problem for finite state transducers over semigroups, Lect. Notes Comput. Sci., 2015, vol. 9270, pp. 208–221.MathSciNetCrossRefzbMATHGoogle Scholar

Copyright information

© Allerton Press, Inc. 2017

Authors and Affiliations

  1. 1.Faculty of Computer ScienceNational Research University Higher School of EconomicsMoscowRussia
  2. 2.Faculty of Computational Mathematics and CyberneticsLomonosov Moscow State UniversityMoscowRussia

Personalised recommendations