Skip to main content

An efficient and unified approach to the decidability of equivalence of propositional programs

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1443))

Abstract

The aim of this paper is to present a unified and easy-to-use technique for deciding the equivalence problem for propositional deterministic programs. The key idea is to reduce this problem to the well-known group-theoretic problems by revealing an algebraic nature of program computations. By applying the main theorems of this paper to some traditional computational models we demonstrate that the equivalence problem for these models is decidable by the simple algorithms in polynomial time.

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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. K.Apt, From Logic Programming to Prolog, Prentice Hall, 1997.

    Google Scholar 

  2. E.Ashcroft, Z.Manna, A.Pnueli, A decidable properties of monadic functional schemes, Journal of the ACM, vol 20 (1973), N 3, p.489–499.

    Article  MATH  MathSciNet  Google Scholar 

  3. V.M.Glushkov, A.A.Letichevskii, Theory of algorithms and discrete processors, Advances in Information System Science, vol 1 (1969), N 1.

    Google Scholar 

  4. E.M.Gurari, O.H.Ibarra, The complexity of equivalence problem for simple programs, Journal of the ACM, vol 28 (1981), N 3, p.535–560.

    Article  MATH  MathSciNet  Google Scholar 

  5. E.M.Gurari, Decidable problems for the reinforced programs, Journal of the ACM, vol 32 (1985), N 2, p.466–483.

    Article  MATH  MathSciNet  Google Scholar 

  6. D.Harel, R.Sherman, Propositional dynamic logic of flowcharts, Lecture Notes in Computer Science, vol 158 (1982), p.195–206.

    MathSciNet  Google Scholar 

  7. D.Harel, Dynamic logics, in Handbook of Philosophical Logics, D.Gabbay and F.Guenthner (eds.), (1984), p.497–604.

    Google Scholar 

  8. T.Harju, J.Karhumaki, The equivalence of multi-tape finite automata, Theoretical Computer Science, vol 78 (1991), p.347–355.

    Article  MATH  MathSciNet  Google Scholar 

  9. O.H.Ibarra, Reversal-bounded multicounter machines and their decision problems, Journal of the ACM, vol 25 (1978), N 1, p.116–133.

    Article  MATH  MathSciNet  Google Scholar 

  10. A.A. Letichevskii, On the equivalence of automata over semigroup, Theoretic Cybernetics, vol 6 (1970), p.3–71 (in Russian)

    Google Scholar 

  11. A.A. Letichevskii, To the practical methods for recognizing the equivalence of finite transducers and program schemata, Kibernetika, (1973), N 4, p.15–26 (in Russian).

    Google Scholar 

  12. A.A.Letichevskii, L.B.Smikun, On a class of groups with solvable problem of automata equivalence, Sov. Math. Dokl., vol 17 (1976), N 2, p.341–344.

    MATH  Google Scholar 

  13. D.C.Luckham, D.M.Park, M.S.Paterson, On formalized computer programs, J. Computer and System Sci., vol 4 (1970), N 3, p.220–249.

    MATH  MathSciNet  Google Scholar 

  14. M.S.Paterson, Programs schemata, Machine Intelligence, Edinburgh: Univ. Press, vol 3 (1968), p.19–31.

    Google Scholar 

  15. M.S.Paterson, Decision problems in computational models, SIGPLAN Notices, vol 7 (1972), p.74–82.

    Article  Google Scholar 

  16. R.I.Podlovchenko, V.A.Zakharov, On the polynomial-time algorithm deciding the commutative equivalence of program schemata, to be published in Reports of the Soviet Academy of Science, (1998).

    Google Scholar 

  17. M.O.Rabin, D.Scott, Finite automata and their decision problems, IBM Journal of Research and Development, vol 3 (1959), N 2, p.114–125.

    Article  MathSciNet  Google Scholar 

  18. J.D.Rutledge, On Ianov's program schemata, J. ACM, vol 11 (1964), N 1, p.1–9.

    Article  MATH  MathSciNet  Google Scholar 

  19. V.K.Sabelfeld, An algorithm deciding functional equivalence in a new class of program schemata, Theoretical Computer Science, vol 71 (1990), p.265–279.

    Article  MATH  MathSciNet  Google Scholar 

  20. G.Senizergues, The equivalence problem for deterministic pushdown automata is decidable, Lecture Notes in Computer Science, v.1256(1997), p.671–681.

    MathSciNet  Google Scholar 

  21. M.A. Taiclin, The equivalence of automata w.r.t. commutative semigroups, Algebra and Logic, vol 8 (1969), N 5, p.553–600 (in Russian).

    MathSciNet  Google Scholar 

  22. L.G.Valiant, Decision procedures for families of deterministic pushdown automata, Report N 7, Univ. of Warwick Computer Center, (1973)

    Google Scholar 

  23. L.G.Valiant, The equivalence problem for deterministic finite-turn pushdown automata, Information and Control, vol25 (1974), N 2, p.123–133.

    Article  MATH  MathSciNet  Google Scholar 

  24. L.G.Valiant, M.S.Paterson, Deterministic one-counter automata, Journal of Computer and System Sci., vol 10 (1975), p.340–350.

    MATH  MathSciNet  Google Scholar 

  25. Y.Yanov, To the equivalence and transformations of program schemata, Reports of the Soviet Academy of Science, vol 113 (1957), N 1, p.39–42 (in Russian).

    MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Editor information

Kim G. Larsen Sven Skyum Glynn Winskel

Rights and permissions

Reprints and permissions

Copyright information

© 1998 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Zakharov, V.A. (1998). An efficient and unified approach to the decidability of equivalence of propositional programs. In: Larsen, K.G., Skyum, S., Winskel, G. (eds) Automata, Languages and Programming. ICALP 1998. Lecture Notes in Computer Science, vol 1443. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0055058

Download citation

  • DOI: https://doi.org/10.1007/BFb0055058

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-64781-2

  • Online ISBN: 978-3-540-68681-1

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics