Skip to main content
SpringerLink
Log in

On the Minimization Problem for Sequential Programs

  • Published:
Automatic Control and Computer Sciences Aims and scope Submit manuscript

Abstract

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.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. Glushkov, V.M. and Letichevsky, A.A., Theory of discrete transducers, Vopr. Algebry Logiki, 1973, pp. 5–39

    Google Scholar 

  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.

    MathSciNet  Google Scholar 

  3. Ershov, A.P., Current state of the theory of program schemes, Probl. Kibern., 1973, vol. 27, pp. 87–110.

    Google Scholar 

  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. 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. 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. Zakharov, V.A., Problemy ekvivalentnosti program: Modeli, algoritmy, slojnost (Program Equivalence Problems: Models, Algorithms, and Complexity), 2016, pp. 1–304

    Google Scholar 

  8. Itkin, V.E., Logical-thermal equivalence of programs, Kibernetika, 1972, no. 1, pp. 5–27.

    Google Scholar 

  9. Kotov, V.E. and Sabelfeld, V.K., Teoriya skhem program (Theory of Program Schemes), 1991, pp. 1–348

    Google Scholar 

  10. Krinickij, N.A., Ravnosil’nye preobrazovaniya algoritmov i programmirovanie (Equivalent Algorithm Transformations and Programming), 1970, pp. 1–210

    Google Scholar 

  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. Lyapunov, A.A., About logical schemes of programs, Probl. Kibern., 1958, vol. 1, pp. 46–74.

    Google Scholar 

  13. Podlovchenko, R.I., Models of sequential programs used to study the functional equivalence of programs, Kibernetika, 1979, no. 1, pp. 20–28.

    MathSciNet  MATH  Google Scholar 

  14. Yanov, Yu.I., On logical schemes of algorithms, Probl. Kibern., 1958, vol. 1, pp. 75–127.

    MathSciNet  MATH  Google Scholar 

  15. Eder, E., Properties of substitutions and unifications, J. Symbolic Comput., 1985, vol. 1, no. 1, pp. 31–46.

    Article  MathSciNet  MATH  Google Scholar 

  16. Ershov, A.P., Alpha—an automatic programming system of high efficiency, J. Assoc. Comput. Mach., 1966, vol. 13, no. 1, pp. 17–24.

    Article  Google Scholar 

  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.

    Article  MathSciNet  Google Scholar 

  18. Harju, T. and Karhumaki, J., The equivalence of multi-tape finite automata, Theor. Comput. Sci., 1991, vol. 78, no. 2, pp. 347–355.

    Article  MATH  Google Scholar 

  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.

    Article  MATH  Google Scholar 

  20. Mohri, M., Minimization algorithms for sequential transducers, Theor. Comput. Sci., 2000, vol. 234, pp. 177–201.

    Article  MathSciNet  MATH  Google Scholar 

  21. Muchnick, S., Advanced Compiler Design and Implementation, 1997, pp. 1–856

    Google Scholar 

  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–24

    Chapter  Google Scholar 

  23. Sabelfeld, V.K., The logic-termal equivalence is polynomial-time decidable, Inf. Process. Lett., 1980, vol. 10, no. 2, pp. 57–62.

    Article  MathSciNet  MATH  Google Scholar 

  24. Senizergues, G., The equivalence problem for deterministic pushdown automata is decidable, Lect. Notes Comput. Sci., 1997, vol. 1256, pp. 271–281.

    MathSciNet  Google Scholar 

  25. Shofrutt, C., Minimizing subsequential transducers: A survey, Theor. Comput. Sci., 2003, vol. 292, pp. 131–143.

    Article  MathSciNet  MATH  Google Scholar 

  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. Zakharov, V.A., On the decidability of the equivalence problem for orthogonal sequential programs, Grammars, 1999, vol. 2, no. 3, pp. 271–281.

    Article  MathSciNet  MATH  Google Scholar 

  28. Zakharov, V.A., Equivalence checking problem for finite state transducers over semigroups, Lect. Notes Comput. Sci., 2015, vol. 9270, pp. 208–221.

    Article  MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Faculty of Computer Science, National Research University Higher School of Economics, Moscow, 101000, Russia

    V. A. Zakharov

  2. Faculty of Computational Mathematics and Cybernetics, Lomonosov Moscow State University, Moscow, 119991, Russia

    S. R. Jaylauova

Authors
  1. V. A. Zakharov
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. S. R. Jaylauova
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to V. A. Zakharov.

Additional information

Published in Russian in Modelirovanie i Analiz Informatsionnykh Sistem, 2017, Vol. 24, No. 4, pp. 415–433.

The article was translated by the authors.

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Zakharov, V.A., Jaylauova, S.R. On the Minimization Problem for Sequential Programs. Aut. Control Comp. Sci. 51, 689–700 (2017). https://doi.org/10.3103/S0146411617070288

Download citation

  • Received:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.3103/S0146411617070288

Keywords

Search

Navigation