Modal Semirings Revisited

  • Jules Desharnais
  • Georg Struth
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5133)


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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
  2. 2.
  3. 3.
  4. 4.
    Birkhoff, G.: Lattice Theory. Colloquium Publications, vol. 25. American Mathematical Society (reprint, 1984)Google Scholar
  5. 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)CrossRefGoogle Scholar
  6. 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. 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. 8.
    Desharnais, J., Möller, B., Struth, G.: Kleene algebra with domain. ACM Trans. Computational Logic 7(4), 798–833 (2006)Google Scholar
  9. 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. 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. 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)CrossRefGoogle Scholar
  12. 12.
    Höfner, P., Struth, G.: Can refinement be automated? ENTCS 201, 197–222 (2008)Google Scholar
  13. 13.
    Johnstone, P.J.: Stone Spaces. Cambridge University Press, Cambridge (1982)zbMATHGoogle Scholar
  14. 14.
    Jónsson, B., Tarski, A.: Boolean algebras with operators, Part I. American Journal of Mathematics 73, 891–939 (1951)CrossRefMathSciNetzbMATHGoogle Scholar
  15. 15.
    Kozen, D.: A completeness theorem for Kleene algebras and the algebra of regular events. Information and Computation 110(2), 366–390 (1994)CrossRefMathSciNetzbMATHGoogle Scholar
  16. 16.
    Kozen, D.: Kleene algebra with tests. ACM Trans. Program. Lang. Syst. 19(3), 427–443 (1997)CrossRefGoogle Scholar
  17. 17.
    Leiß, H.: Kleene modules and linear languages. Journal of Logic and Algebraic Programming 66(2), 185–194 (2006)CrossRefMathSciNetzbMATHGoogle Scholar
  18. 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. 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)CrossRefGoogle Scholar
  20. 20.
    Möller, B., Struth, G.: Algebras of modal operators and partial correctness. Theoretical Computer Science 351(2), 221–239 (2006)CrossRefMathSciNetzbMATHGoogle Scholar
  21. 21.
    Sofronie-Stokkermans, V.: Automated theorem proving by resolution in non-classical logics. Annals of Mathematics and Artificial Intelligence 49, 221–252 (2007)CrossRefMathSciNetzbMATHGoogle Scholar
  22. 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)CrossRefGoogle Scholar
  23. 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. 24.
    von Wright, J.: Towards a refinement algebra. Science of Computer Programming 51(1-2), 23–45 (2004)CrossRefMathSciNetzbMATHGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2008

Authors and Affiliations

  • Jules Desharnais
    • 1
  • Georg Struth
    • 2
  1. 1.Département d’informatique et de génie logicielPavillon Adrien-PouliotQuébecCanada
  2. 2.Department of Computer ScienceUniversity of SheffieldUnited Kingdom

Personalised recommendations