Skip to main content
SpringerLink
Log in

Modal Semirings Revisited

  • Conference paper
Mathematics of Program Construction (MPC 2008)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 5133))

Included in the following conference series:

Abstract

A new axiomatisation for domain and codomain on semirings and Kleene algebras is proposed. It is simpler, more general and more flexible than a predecessor, and it is particularly suitable for program analysis and construction via automated deduction. Different algebras of domain elements for distributive lattices, (co-)Heyting algebras and Boolean algebras arise by adapting this axiomatisation. Modal operators over all these domain algebras can then easily be defined. The calculus of the previous axiomatisation arises as a special case. An application in terms of a fully automated proof of a modal correspondence result for Löb’s formula is also presented.

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

Access this chapter

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

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. http://www.dcs.shef.ac.uk/~georg/ka

  2. Prover9 and Mace4, http://www.cs.unm.edu/~mccune/prover9

  3. Waldmeister, http://www.waldmeister.org

  4. Birkhoff, G.: Lattice Theory. Colloquium Publications, vol. 25. American Mathematical Society (reprint, 1984)

    Google Scholar 

  5. De Carufel, J.-L., Desharnais, J.: Demonic Algebra with Domain. In: Schmidt, R.A. (ed.) RelMiCS/AKA 2006. LNCS, vol. 4136, pp. 120–134. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  6. Degen, W., Werner, J.M.: Towards intuitionistic dynamic logic. In: Proceedings of Studia Logica 2006. Logic and Logical Philosophy, vol. 15, pp. 305–324. Nicolaus Copernicus University Press (2007)

    Google Scholar 

  7. Desharnais, J., Möller, B., Struth, G.: Termination in modal Kleene algebra. In: Lévy, J.-J., Mayr, E.W., Mitchell, J.C. (eds.) IFIP TCS 2004, pp. 647–660. Kluwer, Dordrecht (2004); Revised version: Algebraic Notions of Termination. Technical Report 2006-23, Institut für Informatik, Universität Augsburg (2006)

    Google Scholar 

  8. Desharnais, J., Möller, B., Struth, G.: Kleene algebra with domain. ACM Trans. Computational Logic 7(4), 798–833 (2006)

    Google Scholar 

  9. Desharnais, J., Struth, G.: Enabledness conditions for action systems, probabilistic systems, and processes. Technical Report CS-06-08, Department of Computer Science, University of Sheffield (2008)

    Google Scholar 

  10. Ésik, Z., Kuich, W.: A Semiring-Semimodule Generalization of ω-Context-Free Languages. In: Karhumäki, J., Maurer, H., Păun, G., Rozenberg, G. (eds.) Theory is Forever. LNCS, vol. 3113, pp. 68–80. Springer, Heidelberg (2004)

    Google Scholar 

  11. Höfner, P., Struth, G.: Automated Reasoning in Kleene Algebra. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 279–294. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  12. Höfner, P., Struth, G.: Can refinement be automated? ENTCS 201, 197–222 (2008)

    Google Scholar 

  13. Johnstone, P.J.: Stone Spaces. Cambridge University Press, Cambridge (1982)

    MATH  Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

  16. Kozen, D.: Kleene algebra with tests. ACM Trans. Program. Lang. Syst. 19(3), 427–443 (1997)

    Article  Google Scholar 

  17. Leiß, H.: Kleene modules and linear languages. Journal of Logic and Algebraic Programming 66(2), 185–194 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  18. Maier, P.: Intuitionistic LTL and a New Characterization of Safety and Liveness. In: Marcinkowski, J., Tarlecki, A. (eds.) CSL 2004. LNCS, vol. 3210, pp. 295–309. Springer, Heidelberg (2004)

    Google Scholar 

  19. McIver, A.K., Cohen, E., Morgan, C.C.: Using Probabilistic Kleene Algebra for Protocol Verification. In: Schmidt, R.A. (ed.) RelMiCS/AKA 2006. LNCS, vol. 4136, pp. 296–310. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  20. Möller, B., Struth, G.: Algebras of modal operators and partial correctness. Theoretical Computer Science 351(2), 221–239 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  21. Sofronie-Stokkermans, V.: Automated theorem proving by resolution in non-classical logics. Annals of Mathematics and Artificial Intelligence 49, 221–252 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  22. Solin, K., von Wright, J.: Refinement Algebra with Operators for Enabledness and Termination. In: Uustalu, T. (ed.) MPC 2006. LNCS, vol. 4014, pp. 397–415. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  23. Struth, G.: Reasoning automatically about termination and refinement. In: S. Ranise, editor, 6th International Workshop on First-Order Theorem Proving, Technical Report ULCS-07-018, Department of Computer Science, pp. 36–51. University of Liverpool (2007)

    Google Scholar 

  24. von Wright, J.: Towards a refinement algebra. Science of Computer Programming 51(1-2), 23–45 (2004)

    Article  MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Département d’informatique et de génie logiciel, Pavillon Adrien-Pouliot, 1065, avenue de la Médecine, Université Laval, Québec, QC, Canada, G1V 0A6

    Jules Desharnais

  2. Department of Computer Science, University of Sheffield, S1 4DP, United Kingdom

    Georg Struth

Authors
  1. Jules Desharnais
    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

Philippe Audebaud Christine Paulin-Mohring

Rights and permissions

Reprints and permissions

Copyright information

© 2008 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Desharnais, J., Struth, G. (2008). Modal Semirings Revisited. In: Audebaud, P., Paulin-Mohring, C. (eds) Mathematics of Program Construction. MPC 2008. Lecture Notes in Computer Science, vol 5133. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-70594-9_19

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-70594-9_19

  • Publisher Name: Springer, Berlin, Heidelberg

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

  • Online ISBN: 978-3-540-70594-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation