Abstract
We introduce a natural topology on Kripke models of propositional dynamic logic (PDL) and exhibit a useful duality between certain topological Kripke models and separable dynamic algebras analogous to the duality between Boolean algebras and their Stone spaces. We prove several results which clarify the role of the * operator of PDL and characterize the discrepancy between the standard and nonstandard models in terms of well-understood topological concepts.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Aho A.V., J.E. Hopcroft, and J.D. Ullman, The Design and Analysis of Computer Algorithms. Addison-Wesley, Reading, Mass., 1974.
Bell, J.S. and A.B. Slomson, Models and Ultraproducts. North Holland, Amsterdam, 1971.
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.
Berman, F., "A completeness technique for D-axiomatizable semantics," Proc. 11th ACM Symp. on Theory of Comp. (May 1979), 160–166.
Conway, J.H. Regular Algebra and Finite Machines. Chapman-Hall, London, 1971.
Everett, C.J. and S. Ulam, "Projective algebra I," Amer. J. Math. 68:1 (1946), 77–88.
Fischer, M.J. and R.E.Ladner, "Propositional modal logic of programs," Proc. 9th ACM Symp. on Theory of Comp. (May 1977), 286–294.
Gabbay, D., "Axiomatizations of logics of programs," manuscript, Nov. 1977.
Harel, D. First-Order Dynamic Logic. Lecture Notes in Computer Science 68, ed. Goos and Hartmanis, Springer-Verlag, Berlin, 1979.
Jonsson, B. and A. Tarski, "Representation problems for relation algebras," abstract 89t, Bull. Amer. Math. Soc. 54 (1948), 80.
Kozen, D., "A representation theorem for models of *-free PDL," Report RC7864, IBM Research, Yorktown Heights, New York, Sept. 1979.
Lyndon, R.C., "The representation of relation algebras," Ann. Math. 51:3 (1950), 707–729.
McKinsey, J.C.C., "Postulates for the calculus of binary relations," J. Symb. Logic 5:3 (1940), 85–97.
— "On the representation of projective algebras," Amer. J. Math. 70 (1948), 375–384.
Parikh, R., "A completeness result for PDL," Symp. on Math. Found. of Comp. Sci., Zakopane, Warsaw, Springer-Verlag, May 1978.
Pratt, V.R., "Semantical considerations on Floyd-Hoare logic," Proc. 17th IEEE Symp. on Foundations of Comp. Sci. (Oct. 1976), 109–121.
— "A practical decision method for Propositional Dynamic Logic," Proc. 10th ACM Symp. on Theory of Computing (May 1978), 326–337.
—, "Models of program logics," Proc. 20th IEEE Symp. on Foundations of Comp. Sci. (Oct. 1979), to appear.
—, "Dynamic algebras: examples, constructions, applications," manuscript, July 1979.
Segerberg, K., "A completeness theorem in the modal logic of programs," Not. AMS 24:6 (1977), A-552.
Salomaa, A. and M. Soittala. Automata Theoretic Aspects of Formal Power Series. Springer-Verlag, New York, 1978.
Tarski, A., "On the calculus of relations," J. Symb. Logic 6:3 (1941), 73–89.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1981 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kozen, D. (1981). On the duality of dynamic algebras and kripke models. In: Engeler, E. (eds) Logic of Programs. Logic of Programs 1979. Lecture Notes in Computer Science, vol 125. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-11160-3_1
Download citation
DOI: https://doi.org/10.1007/3-540-11160-3_1
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-11160-3
Online ISBN: 978-3-540-38631-5
eBook Packages: Springer Book Archive