Skip to main content
SpringerLink
Log in

Modal Kleene Algebra and Partial Correctness

  • Conference paper
Algebraic Methodology and Software Technology (AMAST 2004)

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

Abstract

Modal Kleene algebra is Kleene algebra enriched by forward and backward box and diamond operators. We formalize the symmetries of these operators as Galois connections and dualities. We study their properties in the associated semirings of operators. Modal Kleene algebra provides a unifying semantics for various program calculi and enhances efficient cross-theory reasoning in this class, often in a very concise state-free style. This claim is supported by novel algebraic soundness and completeness proofs for Hoare logic.

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

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

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

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. Apt, K.-R., Olderog, E.-R.: Verification of Sequential and Concurrent Programs, 2nd edn. Springer, Heidelberg (1997)

    MATH  Google Scholar 

  2. Clenaghan, K.: Calculational graph algorithmics: Reconciling two approaches with dynamic algebra. Technical Report CS-R9518, CWI, Amsterdam (1994)

    Google Scholar 

  3. Cohen, E.: Separation and reduction. In: Backhouse, R., Oliveira, J.N. (eds.) MPC 2000. LNCS, vol. 1837, pp. 45–59. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  4. Desharnais, J., Möller, B., Struth, G.: Kleene algebra with domain. Technical Report 2003-07, Universität Augsburg, Institut für Informatik (2003)

    Google Scholar 

  5. Desharnais, J., Möller, B., Struth, G.: Applications of modal Kleene algebra – a survey. Technical Report DIUL-RR-0401, D´epartement d’informatique et de g´enie logiciel, Universit´e Laval, Qu´ebec (2004)

    Google Scholar 

  6. Desharnais, J., Möller, B., Struth, G.: Termination in modal Kleene algebra. Technical Report 2004-04, Universität Augsburg, Institut für Informatik (2004)

    Google Scholar 

  7. Ehm, T., Möller, B., Struth, G.: Kleene modules. In: Berghammer, R., Möller, B., Struth, G. (eds.) RelMiCS 2003. LNCS, vol. 3051, Springer, Heidelberg (2004)

    Google Scholar 

  8. Fischer, J.M., Ladner, R.F.: Propositional dynamic logic of regular programs. J. Comput. System Sci. 18(2), 194–211 (1979)

    Article  MATH  MathSciNet  Google Scholar 

  9. Hardin, C., Kozen, D.: On the elimination of hypotheses in Kleene algebra with tests. Technical Report 2002-1879, Computer Science Department, Cornell University (October 2002)

    Google Scholar 

  10. J´onsson, B., Tarski, A.: Boolean algebras with operators, Part I. American Journal of Mathematics 73, 891–939 (1951)

    Article  MathSciNet  Google Scholar 

  11. Kozen, D.: A completeness theorem for Kleene algebras and the algebra of regular events. Information and Computation 110(2), 366–390 (1994)

    Article  MATH  MathSciNet  Google Scholar 

  12. Kozen, D.: Kleene algebra with tests. Trans. Programming Languages and Systems 19(3), 427–443 (1997)

    Article  Google Scholar 

  13. Kozen, D.: On Hoare logic and Kleene algebra with tests. Trans. Computational Logic 1(1), 60–76 (2001)

    Article  MathSciNet  Google Scholar 

  14. Kozen, D., Patron, M.-C.: Certification of compiler optimizations using Kleene algebra with tests. In: Palamidessi, C., Moniz Pereira, L., Lloyd, J.W., Dahl, V., Furbach, U., Kerber, M., Lau, K.-K., Sagiv, Y., Stuckey, P.J. (eds.) CL 2000. LNCS (LNAI), vol. 1861, pp. 568–582. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  15. Loeckx, J., Sieber, K.: The Foundations of Program Verification, 2nd edn. Wiley Teubner, Chichester (1987)

    MATH  Google Scholar 

  16. Möller, B.: Lazy Kleene algebra. In: Kozen, D. (ed.) MPC 2004. LNCS, vol. 3125, pp. 252–273. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  17. Möller, B., Struth, G.: Modal Kleene algebra and partial correctness. Technical Report 2003-08, Universität Augsburg, Institut für Informatik (2003)

    Google Scholar 

  18. Möller, B., Struth, G.: Greedy-like algorithms in modal Kleene algebra. In: Berghammer, R., Möller, B., Struth, G. (eds.) RelMiCS 2003. LNCS, vol. 3051, Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  19. Schmidt, G.W., Ströhlein, T.: Relations and Graphs: Discrete Mathematics for Computer Scientists. In: EATCS Monographs on Theoretical Computer Science, Springer, Heidelberg (1993)

    Google Scholar 

  20. Struth, G.: Calculating Church-Rosser proofs in Kleene algebra. In: de Swart, H. (ed.) RelMiCS 2001. LNCS, vol. 2561, pp. 276–290. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  21. von Karger, B.: Temporal algebra. Mathematical Structures in Computer Science 8(3), 277–320 (1998)

    Article  MATH  MathSciNet  Google Scholar 

  22. von Wright, J.: From Kleene algebra to refinement algebra. In: Boiten, E.A., Möller, B. (eds.) MPC 2002. LNCS, vol. 2386, pp. 233–262. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institut für Informatik, Universität Augsburg, Universitätsstr. 14, D-86135, Augsburg, Germany

    Bernhard Möller & Georg Struth

Authors
  1. Bernhard Möller
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Georg Struth
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. University of Stirling, FK9 4LA, Stirling, UK

    Charles Rattray

  2. University of Stirling, FK9 4LA, Stirling

    Savitri Maharaj

  3. Department of Computing Science and Mathematics, University of Stirling, FK9 4LA, Stirling, UK

    Carron Shankland

Rights and permissions

Reprints and permissions

Copyright information

© 2004 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Möller, B., Struth, G. (2004). Modal Kleene Algebra and Partial Correctness. In: Rattray, C., Maharaj, S., Shankland, C. (eds) Algebraic Methodology and Software Technology. AMAST 2004. Lecture Notes in Computer Science, vol 3116. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-27815-3_30

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-27815-3_30

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-22381-8

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

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation