Skip to main content
SpringerLink
Log in
Book cover

International Colloquium on Automata, Languages, and Programming

ICALP 1982: Automata, Languages and Programming pp 348–359Cite as

Results on the propositional μ-calculus

  • Conference paper
  • First Online:

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

Abstract

We define a propositional version of the Μ-calculus, and give an exponential-time decision procedure, small model property, and complete deductive system. We also show that it is strictly more expressive than PDL. Finally, we give an algebraic semantics and prove a representation theorem.

On leave from IBM Thomas J. Watson Research Center, Yorktown Heights, New York 10598, USA.

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

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. P. Hitchcock and D.M.R. Park, Induction Rules and Termination Proofs, Proc. 1st ICALP, 1973, 225–251.

    Google Scholar 

  2. D. Kozen and R. Parikh, An Elementary Proof of the Completeness of PDL, TCS 14 (1981), 113–118.

    Article  MathSciNet  Google Scholar 

  3. D. Kozen, A Representation Theorem for Models of *-free PDL, Proc. 7th ICALP, Springer LNCS 85 (1980), 352–362.

    Google Scholar 

  4. D. Kozen, On the Duality of Dynamic Algebras and Kripke Models, Proc. Workshop on Logic of, Programs, Springer LNCS 125, 1–11.

    Google Scholar 

  5. D. Kozen, On Induction vs. *-continuity, Proc. Workshop on Logics of Programs, Springer LNCS 131 (1982), 167–176.

    Google Scholar 

  6. D.M.R. Park, Fixpoint Induction and proof of program semantics, Mach. Int. 5, ed. Meltzer and Michie, Edinburgh Univ. Press, 1970, 59–78.

    Google Scholar 

  7. V.R. Pratt, A Decidable Μ-calculus (Preliminary Report), Proc. 22nd FOCS, Oct. 1981, 421–427.

    Google Scholar 

  8. V.R. Pratt, A near optimal method for reasoning about action, JCSS 20 (1980), 231–254.

    MathSciNet  MATH  Google Scholar 

  9. D. Scott and J. deBakker, A Theory of Programs, unpublished, IBM, Vienna, 1969.

    Google Scholar 

  10. R. Streett, Propositional Dynamic Logic of Looping and Converse, Proc. 13th STOC, May 1981, 375–383.

    Google Scholar 

  11. A. Chandra, D. Kozen, L. Stockmeyer, Alternation, JACM, Jan. 1981.

    Article  MathSciNet  Google Scholar 

  12. J. deBakker, Mathematical Theory of Program Correctness, Prentice-Hall, 1980.

    Google Scholar 

  13. J. deBakker and W. deRoever, A Calculus for Recursive Program Schemes, Proc. 1st ICALP, 1973, 167–196.

    Google Scholar 

  14. W.P. deRoever, Recursive. Program Schemes: Semantics and Proof Theory, Ph.D. Thesis, Free University, Amsterdam, 1974.

    Google Scholar 

  15. E.A. Emerson and E.M. Clarke, Design and Synthesis of Synchronization Skeletons using Branching-Time Temporal Logic, Proc. Workshop on Logics of Programs, Springer LNCS 131 (1982), 52–71.

    Google Scholar 

  16. M. Fischer and R. Ladner, Propositional Dynamic Logic of Regular Programs, JCSS 18:2 (79).

    Article  MathSciNet  Google Scholar 

  17. J. Halpern and J. Reif, The Propositional Dynamic Logic of Deterministic, Well-Structured Programs, (extended abstract), Proc. 22nd FOCS, Oct. 1981, 322–334.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Aarhus University, Aarhus, Denmark

    Dexter Kozen

Authors
  1. Dexter Kozen
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Mogens Nielsen Erik Meineche Schmidt

Rights and permissions

Reprints and permissions

Copyright information

© 1982 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Kozen, D. (1982). Results on the propositional μ-calculus. In: Nielsen, M., Schmidt, E.M. (eds) Automata, Languages and Programming. ICALP 1982. Lecture Notes in Computer Science, vol 140. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0012782

Download citation

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

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

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

  • Online ISBN: 978-3-540-39308-5

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation