[go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

On induction vs. *-continuity

  • Conference paper
  • First Online:
Logics of Programs (Logic of Programs 1981)

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

Included in the following conference series:

  • 163 Accesses

Abstract

In this paper we study the relative expressibility of the infinitary *-continuity condition

$$< \alpha ^* > X \equiv V_n < \alpha ^n > X$$
((*-cont))

and the equational but weaker induction axiom

$$X \wedge [\alpha ^* ](X \supset [\alpha ]X) \equiv [\alpha ^* ]X$$
((ind))

in Propositional Dynamic Logic. We show: (1) under ind only, there is a first-order sentence distinguishing separable dynamic algebras from standard Kripke models; whereas (2) under the stronger axiom *-cont, the class of separable dynamic algebras and the class of standard Kripke models are indistinguishable by any sentence of infinitary first-order logic.

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

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

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

    Google Scholar 

  2. Keisler, H.J. Model Theory for Infinitary Logic. North Holland, Amsterdam, 1971.

    Google Scholar 

  3. Kozen, D., "A representation theorem for models of *-free PDL," Proc. 7th Int. Colloq. on Automata, Languages, and Programming, Lecture Notes in Computer Science 85, ed. Goos and Hartmanis, Springer-Verlag, Berlin, 1980, 351–362. Also Report RC7864, IBM Research, Yorktown Heights, New York, Sept. 1979.

    Google Scholar 

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

    Google Scholar 

  5. —, "On the representation of dynamic algebras," Report RC7898, IBM Research, Yorktown Heights, New York, Oct. 1979.

    Google Scholar 

  6. —, "On the representation of dynamic algebras II," Report RC8290, IBM Research, Yorktown Heights, New York, May 1980.

    Google Scholar 

  7. —, and R. Parikh, "An elementary proof of the completeness of PDL," TCS, to appear; also IBM Report RC8097, Jan. 1980.

    Google Scholar 

  8. Parikh, R., "A completeness result for PDL," Symp. on Math. Found. of Comp. Sci., Zakopane, Springer-Verlag, May 1978, 403–415.

    Google Scholar 

  9. Pratt, V.R., "Dynamic Algebras: Examples, Constructions, Applications," MIT/LCS Report TM-138, July 1979.

    Google Scholar 

  10. —, "Models of program logics," Proc. 20th IEEE Symp. on Foundations of Comp. Sci. (Oct. 1979), 115–122.

    Google Scholar 

  11. —, "Dynamic algebras and the nature of induction," Proc. 12th ACM Symp. on Theory of Computing (May 1980), 22–28.

    Google Scholar 

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

    Google Scholar 

  13. Reiterman, J. and V. Trnková, "Dynamic algebras which are not Kripke structures," Proc. 9th Symp. on Math. Found. of Computer Science (Aug. 1980), 528–538.

    Google Scholar 

  14. Salomaa, A., "Two complete axiom systems for the algebra of regular events," J. ACM 13:1 (1966), 158–169.

    Article  Google Scholar 

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

    Google Scholar 

Download references

Author information

Authors and Affiliations

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

    Dexter Kozen

Authors
  1. Dexter Kozen
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Dexter Kozen

Rights and permissions

Reprints and permissions

Copyright information

© 1982 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Kozen, D. (1982). On induction vs. *-continuity. In: Kozen, D. (eds) Logics of Programs. Logic of Programs 1981. Lecture Notes in Computer Science, vol 131. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0025782

Download citation

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

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-11212-9

  • Online ISBN: 978-3-540-39047-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation