Skip to main content
SpringerLink
Log in
Book cover

International Colloquium on Automata, Languages, and Programming

ICALP 1980: Automata, Languages and Programming pp 351–362Cite as

A representation theorem for models of *-free PDL

  • Conference paper
  • First Online:

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

Abstract

We introduce dynamic algebras and show how they can be used to give an algebraic interpretation to propositional dynamic logic (PDL). Dynamic algebras include all Kripke models, the standard interpretation of PDL. We give a simple algebraic condition on *-free dynamic algebras that is necessary and sufficient for representation by *-free Kripke models. In the presence of*, the condition is sufficient for representation by a nonstandard Kripke model. This result leads to a duality between certain topological Kripke models and dynamic algebras analogous to the duality between Boolean algebras and their Stone spaces.

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. Aho A.V., J.E. Hopcroft, and J.D. Ullman, The Design and Analysis of Computer Algorithms. Addison-Wesley, Reading, Mass., 1974.

    Google Scholar 

  2. Banachowski, L., A. Kreczmar, G. Mirkowska, H. Rasiowa, and A. Salwicki, "An introduction to Algorithmic Logic," in: Mazurkiewicz and Pawlak, eds., Math. Found. of Comp. Sci., Banach Center Publications, Warsaw, 1977.

    Google Scholar 

  3. Berman, F., "A completeness technique for D-axiomatizable semantics," Proc. 11th ACM Symp. on Theory of Comp. (May 1979), 160–166.

    Google Scholar 

  4. Bell, J.S. and A.B. Slomson, Models and Ultraproducts. North Holland, Amsterdam, 1971.

    Google Scholar 

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

    Google Scholar 

  6. Constable, R.L. and M.J. O'Donnell. A Programming Logic. Winthrop, Cambridge, Mass., 1978.

    Google Scholar 

  7. Everett, C.J. and S. Ulam, "Projective algebra I," Amer. J. Math. 68:1 (1946), 77–88.

    Google Scholar 

  8. Fischer, M.J. and R.E. Ladner, "Propositional dynamic logic of regular programs," J. Comput. Syst. Sci. 18:2 (1979).

    Google Scholar 

  9. Gabbay, D., "Axiomatizations of logics of programs," manuscript, Nov. 1977.

    Google Scholar 

  10. Harel, D. First-Order Dynamic Logic. Lecture Notes in Computer Science 68, ed. Goos and Hartmanis, Springer-Verlag, Berlin, 1979.

    Google Scholar 

  11. Jonsson, B. and A. Tarski, "Representation problems for relation algebras," abstract 89t, Bull. Amer. Math. Soc. 54 (1948), 80.

    Google Scholar 

  12. Kozen, D., "A representation theorem for models of *-free PDL," Report RC7864, IBM Research, Yorktown Heights, New York, Sept. 1979.

    Google Scholar 

  13. Kozen, D., "On the duality of dynamic algebras and Kripke models," Report RC7893, IBM Research, Yorktown Heights, New York, Oct. 1979.

    Google Scholar 

  14. Kozen, D., "On the representation of dynamic algebras," Report RC7898, IBM Research, Yorktown Heights, New York, Oct. 1979.

    Google Scholar 

  15. Lyndon, R.C., "The representation of relation algebras," Ann. Math. 51:3 (1950), 707–729.

    Google Scholar 

  16. McKinsey, J.C.C., "Postulates for the calculus of binary relations," J. Sym. Logic 5:3 (1940), 85–97.

    Google Scholar 

  17. —, "On the representation of projective algebras," Amer. J. Math. 70 (1948), 375–384.

    Google Scholar 

  18. Nishimura, H., "Sequential Method in Propositional Dynamic Logic," Acta Informatica 12 (1979), 377–400.

    Google Scholar 

  19. Parikh, R., "A completeness result for PDL," Symp. on Math. Found. of Comp. Sci., Zakopane, Warsaw, Springer-Verlag, May 1978.

    Google Scholar 

  20. Pratt, V.R., "Semantical considerations on Floyd-Hoare logic," Proc. 17th IEEE Symp. on Foundations of Comp. Sci. (Oct. 1976), 109–121.

    Google Scholar 

  21. —, "A practical decision method for Propositional Dynamic Logic," Proc. 10th ACM Symp. on Theory of Computing (May 1978), 326–337.

    Google Scholar 

  22. —, "Models of program logics," Proc. 20th IEEE Symp. on Foundations of Comp. Sci. (Oct. 1979), to appear.

    Google Scholar 

  23. —, "Dynamic algebras: Examples, constructions, applications," manuscript, July 1979.

    Google Scholar 

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

    Google Scholar 

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

    Google Scholar 

  26. Tarski, A., "On the calculus of relations," J. Symb. Logic 6:3 (1941), 73–89.

    Google Scholar 

  27. van Emde Boas, "The connection between modal logic and algorithmic logics," report 78-02, Univ. of Amsterdam, May 1978.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. IBM Thomas J. Watson Research Center, Yorktown Heights, 10598, New York

    Dexter Kozen

Authors
  1. Dexter Kozen
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Jaco de Bakker Jan van Leeuwen

Rights and permissions

Reprints and permissions

Copyright information

© 1980 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Kozen, D. (1980). A representation theorem for models of *-free PDL. In: de Bakker, J., van Leeuwen, J. (eds) Automata, Languages and Programming. ICALP 1980. Lecture Notes in Computer Science, vol 85. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-10003-2_83

Download citation

  • DOI: https://doi.org/10.1007/3-540-10003-2_83

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-10003-4

  • Online ISBN: 978-3-540-39346-7

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation