Dynamic algebras: Examples, constructions, applications | Studia Logica Skip to main content
Springer Nature Link
Log in

Dynamic algebras: Examples, constructions, applications

  • Published:
Studia Logica Aims and scope Submit manuscript

Abstract

Dynamic algebras combine the classes of Boolean (B ∨ ′ 0) and regular (R ∪; *) algebras into a single finitely axiomatized variety (B R ◊) resembling an R-module with “scalar” multiplication ◊. The basic result is that * is reflexive transitive closure, contrary to the intuition that this concept should require quantifiers for its definition. Using this result we give several examples of dynamic algebras arising naturally in connection with additive functions, binary relations, state trajectories, languages, and flowcharts. The main result is that free dynamic algebras are residually finite (i.e. factor as a subdirect product of finite dynamic algebras), important because finite separable dynamic algebras are isomorphic to Kripke structures. Applications include a new completeness proof for the Segerberg axiomatization of prepositional dynamic logic, and yet another notion of regular algebra.

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

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
¥17,985 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price includes VAT (Japan)

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. G. Birkhoff. On the structure of abstract algebras. Proc. Cambridge Phil. Soc, 31, 1935.

  2. G. Birkhoff. Lattice Theory. Volume 25, A.M.S. Colloq. Publications, 1967.

  3. G. Birkhoff and J.D. Lipson. Heterogeneous algebras. J. of Combinatorial Theory, 8:115–133, 1970.

    Google Scholar 

  4. C. Brink. Boolean modules. Journal of Algebra, 71:291–313, 1981.

    Google Scholar 

  5. R.T Casley, R.F. Crew, J. Meseguer, and V.R. Pratt. Temporal structures. In Proc. Conf. on Category Theory and Computer Science, LNCS, Springer-Verlag, Manchester, September 1989.

    Google Scholar 

  6. P.M. Cohn. Universal Algebra. Harper and Row, New York, 1965.

    Google Scholar 

  7. J.H. Conway. Regular Algebra and Finite Machines. Chapman and Hall, London, 1971.

    Google Scholar 

  8. J.H. Conway. Regular Algebra and Finite Machines. Chapman and Hall, London, 1971.

    Google Scholar 

  9. R.L. Constable. On the theory of programming logics. In Proc. 9th Annual ACM Symp. on Theory of Computing, pages 269–285, Boulder, Col., May 1977.

  10. J.W. de Bakker and W.P. de Roever. A calculus for recursive program schemes. In M. Nivat, editor, Automata, Languages and Programming, pages 167–196, North Holland, 1972.

  11. E.W. Dijkstra. A Discipline of Programming. Prentice-Hall, Englewood Cliffs, N.J., 1976.

    Google Scholar 

  12. M.J Fischer and R.E. Ladner. Propositional dynamic logic of regular programs. JCSS, 18(2), 1979.

  13. R.W. Floyd. Assigning meanings to programs. In J.T Schwartz, editor, Mathematical Aspects of Computer Science, pages 19–32, 1967.

  14. G. Graetzer. Universal Algebra. Van Nostrand, Princeton, NJ, 1968.

    Google Scholar 

  15. P.R. Halmos. Algebraic Logic. Chelsea, New York, 1962.

    Google Scholar 

  16. D. Harel. Dynamic logic. In Handbook of Philosophical Logic. II: Extensions of Classical Logic, pages 497–604, D. Reidel, Boston, 1984.

    Google Scholar 

  17. L. Henkin. The logic of equality. Amer. Math. Monthly, 84(8):597–612, October 1977.

    Google Scholar 

  18. C.A.R. Hoare. An axiomatic basis for computer programming. Communications of the ACM, 12:576–580, 1969.

    Google Scholar 

  19. A. Horn. On sentences which are true of direct unions of algebras. J. Symbolic Logic, 16:14–21, 1951.

    Google Scholar 

  20. S.C. Kleene. Representation of events in nerve nets and finite automata. In Automata Studies, pages 3–42, Princeton University Press, Princeton, NJ, 1956.

    Google Scholar 

  21. D. Kozen. On the duality of dynamic algebras and Kripke models. In E. Engeler, editor, Proc. Workshop on Logic of Programs 1979, LNCS 125, pages 1–11, Springer-Verlag, 1979.

  22. D. Kozen. On the representation of dynamic algebras. Technical Report RC7898, IBM, October 1979.

  23. D. Kozen. A representation theorem for models of *-free PDL. May 1979. Manuscript.

  24. D. Kozen. A representation theorem for models of *-free PDL. Technical Report RC7864, IBM, September 1979.

  25. D. Kozen. On the representation of dynamic algebras II. Technical Report RC8290, IBM, May 1980.

  26. D. Kozen. A representation theorem for models of *-free PDL. In Proc. 7th Colloq. on Automata, Languages, and Programming, pages 351–362, July 1980.

  27. D. Kozen. Dynamic algebra: Section in: Propositional dynamic logics of programs: a survey, by R. Parikh. In E. Engeler, editor, Proc. Workshop on Logic of Programs 1979, LNCS 125, pages 102–144, Springer, 1981.

  28. D. Kozen. On induction vs. *-continuity. In D. Kozen, editor, Proc. Workshop on Logics of Programs 1981, LNCS 131, pages 167–176, Spring-Verlag, 1981.

  29. D. Kozen. A Completeness Theorem for Kleene Algebras and the Algebra of Regular Events. Technical Report 90–1123, Cornell U., May 1990.

  30. D. Kozen and R. Parikh. A decision procedure for the propositional μ-calculus. In E. Clarke and Kozen D., editors, Proc. Workshop on Logics of Programs 1983, LNCS 164, pages 313–325, Springer-Verlag, 1983.

  31. R, Milner. Calculus of Communicating Behavior, LNCS 92. Springer-Verlag, 1980.

  32. J.D. Monk. On representable relation algebras. Michigan Math. J., 11:207–210, 1964.

    Google Scholar 

  33. I. Németi. Dynamic algebras of programs. In Proc. Fundamentals of Computation Theory, LNCS 117, pages 281–290, Springer-Verlag, 1981.

  34. I. Németi. Every free algebra in the variety generated by the representable dynamic algebras is separable and representable. Theoretical Computer Science, 17:343–347, 1982.

    Google Scholar 

  35. K.C. Ng. Relation Algebras with Transitive Closure. PhD thesis, University of California, Berkeley, 1984. 157+iv pp.

    Google Scholar 

  36. K.C. Ng and A. Tarski. Relation algebras with transitive closure, Abstract 742-02-09. Notices Amer. Math. Soc., 24:A29-A30, 1977.

    Google Scholar 

  37. R. Parikh. A completeness result for a prepositional dynamic logic. In LNCS 64, pages 403–415, Springer-Verlag, 1978.

  38. A. Pnueli. The temporal logic of programs. In 18th IEEE Symposium on Foundations of Computer Science, pages 46–57, October 1977.

  39. V.R. Pratt. Semantical considerations on Floyd-Hoare logic. In Proc. 17th Ann. IEEE Symp. on Foundations of Comp. Sci., pages 109–121, October 1976.

  40. V.R. Pratt. Models of program logics. In 20th Symposium on foundations of Computer Science, San Juan, October 1979.

  41. V.R. Pratt. Process logic. In Proc. 6th Ann. ACM Symposium on Principles of Programming Languages, pages 93–100, San Antonio, January 1979.

  42. V.R. Pratt. Application of modal logic to programming. Studia Logica, 34(2/3):257–274, 1980.

    Google Scholar 

  43. V.R. Pratt. Dynamic algebras and the nature of induction. In 12th ACM Symposium on Theory of Computation, Los Angeles, April 1980.

  44. V.R. Pratt. A near optimal method for reasoning about action. Journal of Computer and System Sciences, 2:231–254, April 1980. Also MIT/LCS/TM-113, M.I.T., Sept. 1978.

    Google Scholar 

  45. V.R. Pratt. A decidable mu-calculus. In Proc. 22nd IEEE Conference on Foundations of Computer Science, pages 421–427, October 1981.

  46. V.R. Pratt. Using graphs to understand PDL. In D. Kozen, editor, Proc. Workshop on Logics of Programs 1981, LNCS 131, pages 387–396, Spring-Verlag, 1981.

  47. V.R. Pratt. Action logic and pure induction. In Logics in AI, LNCS 478, pages 97–120, Springer-Verlag, Amsterdam, September 1990.

    Google Scholar 

  48. V.R. Pratt. Dynamic algebras as a well-behaved fragment of relation algebras. In Algebraic Logic and Universal Algebra in Computer Science, LNCS 425, Springer-Verlag, Ames, Iowa, June 1988, 1990.

    Google Scholar 

  49. V.N. Redko. On defining relations for the algebra of regular events (Russian). Ukrain. Mat. Z., 16:120–126, 1964.

    Google Scholar 

  50. A. Salomaa. Two complete axiom systems for the algebra of regular events. Journal of the ACM, 13:158–169, 1966.

    Google Scholar 

  51. A. Salwicki. Formalized algorithmic languages. Bull. Acad. Pol. Sci., Ser. Sci. Math. Astr. Phys., 18(5), 1970.

  52. K. Segerberg. A completeness theorem in the modal logic of programs. Notices of the AMS, 24(6):A-552, October 1977.

    Google Scholar 

  53. A. Salomaa and M. Soittola. Automata-Theoretic Aspects of Formal Power Series. Springer-Verlag, New York, 1978.

    Google Scholar 

  54. M. Stone. The theory of representations for Boolean algebras. Trans. Amer. Math. Soc., 40:37–111, 1936.

    Google Scholar 

  55. A. Tarski. On the calculus of relations. J. Symbolic Logic, 6:73–89, 1941.

    Google Scholar 

  56. V. Trnkova and J. Reiterman. Dynamic algebras with tests. Journal of Computer and System Sciences, 35:229–242, 1987.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, Stanford University, 94305, Stanford, CA, USA

    Vaughan Pratt

Authors
  1. Vaughan Pratt
    View author publications

    You can also search for this author in PubMed Google Scholar

Additional information

Dept. of Computer Science, Stanford, CA 94305 This research was supported by the National Science Foundation under NSF grant no. MCS78-04338. Preparation of the present version was supported by the National Science Foundation under NSF grant number CCR-8814921.

This paper originally appeared as Technical Memo #138, Laboratory for Computer Science, MIT, July 1979, and was subsequently revised, shortened, retitled, and published as [Pra80b]. After more than a decade of armtwisting I. Németi and H. Andréka finally persuaded the author to publish TM#138 itself on the ground that it contained a substantial body of interesting material that for the sake of brevity had been deleted from the STOC-80 version. The principal changes here to TM#138 are the addition of footnotes and the sections at the end on retrospective citations and reflections.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Pratt, V. Dynamic algebras: Examples, constructions, applications. Stud Logica 50, 571–605 (1991). https://doi.org/10.1007/BF00370685

Download citation

  • Received:

  • Issue Date:

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

Keywords

Search

Navigation