Kleene algebra with domain

ABSTRACT

We propose Kleene algebra with domain (KAD), an extension of Kleene algebra by simple equational axioms for a domain and a codomain operation. KAD considerably augments the expressiveness of Kleene algebra, in particular for the specification and analysis of programs and state transition systems. We develop the basic calculus, present the most interesting models and discuss some related theories. We demonstrate applicability by two examples: algebraic reconstructions of Noethericity and propositional Hoare logic based on equational reasoning.

REFERENCES

• 1: Aarts, C. J. 1992. Galois connections presented calculationally. M.S. thesis, Department of Mathematics and Computing Science, Eindhoven University of Technology.
• 2: Abrial, J.-R. 1996. The B-Book. Cambridge University Press, Cambridge, UK.
• 3: Krzysztof R. Apt , Ernst-Rüdiger Olderog, Verification of sequential and concurrent programs (2nd ed.), Springer-Verlag New York, Inc., Secaucus, NJ, 1997
• 4: Birkhoff, G. 1984. Lattice Theory. Colloquium Publications, vol. 25. American Mathematical Society. (Reprint).
• 5: Bull, R. and Segerberg, K. 1984. Basic modal logic. In Handbook of Philosophical Logic, D. Gabbay and F. Guenthner, Eds. vol. II. D. Reidel, Chapter II.1, 1--88.
• 6: Chellas, B. F. 1980. Modal Logic: An Introduction. Cambridge University Press, Cambridge, UK.
• 7: Cohen, E. 1993. Hypotheses in Kleene algebra. Tech. rep. TM-ARH-023814. Bellcore.
• 8: Ernie Cohen, Separation and Reduction, Proceedings of the 5th International Conference on Mathematics of Program Construction, p.45-59, July 03-05, 2000
• 9: Conway, J. H. 1971. Regular Algebra and Finite State Machines. Chapman and Hall.
• 10: S. Crvenković , I. Dolinka , Z. Ésik, The variety of Kleene algebras with conversion is not finitely based, Theoretical Computer Science, v.230 n.1-2, p.235-245, Jan. 2000 [doi>10.1016/S0304-3975(99)00079-1 ]
• 11: Desharnais, J. and Möller, B. 2001. Characterizing determinacy in Kleene algebras. Inf. Sci. 139, 3--4, 253--273.
• 12: Desharnais, J., Möller, B., and Struth, G. 2004a. Applications of modal Kleene algebra---a survey. JoRMiCS---Journal on Relational Methods in Computer Science 1, 93--131. http://www.cosc.brocku.ca/Faculty/Winter/JoRMiCS.
• 13: Desharnais, J., Möller, B., and Struth, G. 2004b. Termination in modal Kleene algebra. In Exploring New Frontiers of Theoretical Informatics, J.-J. Lévy, E. Mayr, and J. Mitchell, Eds. IFIP International Federation for Information Processing Series, vol. 155. Kluwer, 647--660.
• 14: Jules Desharnais , Bernhard Möller , Fairouz Tchier, Kleene under a Demonic Star, Proceedings of the 8th International Conference on Algebraic Methodology and Software Technology, p.355-370, May 20-27, 2000
• 15: Samuel Eilenberg, Automata, Languages, and Machines, Academic Press, Inc., Orlando, FL, 1974
• 16: Fischer, J. M. and Ladner, R. F. 1979. Propositional dynamic logic of regular programs. J. Comput. System Sci. 18, 2, 194--211.
• 17: Gaubert, S. and Plus, M. 1997. Methods and applications of (max,+) linear algebra. Tech. Rep. RR-3088, INRIA- Rocquencourt.
• 18: Goldblatt, R. 1985. An algebraic study of well-foundedness. Studia Logica 44, 4, 422--437.
• 19: David Harel , Jerzy Tiuryn , Dexter Kozen, Dynamic Logic, MIT Press, Cambridge, MA, 2000
• 20: Burghard von Karger , C. A. R. Hoare, Sequential calculus, Information Processing Letters, v.53 n.3, p.123-130, Feb. 10, 1995 [doi>10.1016/0020-0190(94)00205-D ]
• 21: Marco Hollenberg, Equational Axioms of Test Algebra, Selected Papers from the11th International Workshop on Computer Science Logic, p.295-310, August 23-29, 1997
• 22: Kozen, D. 1979. A representation theorem for *-free PDL. Tech. Rep. RC7864, IBM.
• 23: Dexter Kozen, A completeness theorem for Kleene algebras and the algebra of regular events, Information and Computation, v.110 n.2, p.366-390, May 1, 1994
• 24: Dexter Kozen, On action algebras, Logic and information flow, MIT Press, Cambridge, MA, 1994
• 25: Dexter Kozen, Kleene algebra with tests, ACM Transactions on Programming Languages and Systems (TOPLAS), v.19 n.3, p.427-443, May 1997 [doi>10.1145/256167.256195]
• 26: Dexter Kozen, On Hoare logic and Kleene algebra with tests, ACM Transactions on Computational Logic (TOCL), v.1 n.1, p.60-76, July 2000 [doi>10.1145/343369.343378]
• 27: Dexter Kozen , Frederick Smith, Kleene Algebra with Tests: Completeness and Decidability, Selected Papers from the10th International Workshop on Computer Science Logic, p.244-259, September 21-27, 1996
• 28: Werner Kuich, Semirings and formal power series: their relevance to formal languages and automata, Handbook of formal languages, vol. 1: word, language, grammar, Springer-Verlag New York, Inc., New York, NY, 1997
• 29: Jacques Loeckx , Kurt Sieber, The foundations of program verification (2nd ed.), John Wiley & Sons, Inc., New York, NY, 1987
• 30: Möller, B. 2005. Complete tests do not gurantee domain. Tech. Rep. 2005-6, Universität Augsburg, Institut für Informatik. http://www.informatik.uni-augsburg.de/forschung/techBerichte/reports/2005-6.pdf.
• 31: Bernhard Möller , Georg Struth, Algebras of modal operators and partial correctness, Theoretical Computer Science, v.351 n.2, p.221-239, 21 February 2006 [doi>10.1016/j.tcs.2005.09.069]
• 32: Mulvey, C. 1986. &. Rend. Circ. Math. Palermo 2, 12, 99--104.
• 33: István Németi, Dynamic Algebras of Programs, Proceedings of the 1981 International FCT-Conference on Fundamentals of Computation Theory, p.281-290, August 24-28, 1981
• 34: Vaughan R. Pratt, Dynamic algebras as a well-behaved fragment of relation algebras, Proceedings of the Conference on Algebraic Logic and Universal Algebra in Computer Science, p.77-110, June 01-04, 1988
• 35: Vaughan R. Pratt, Action Logic and Pure Induction, Proceedings of the European Workshop on Logics in AI, p.97-120, September 11-14, 1990
• 36: Pratt, V. 1991. Dynamic algebras: Examples, constructions, applications. Studia Logica 50, 571--605.
• 37: Gunther Schmidt , Thomas Ströhlein, Relations and graphs: discrete mathematics for computer scientists, Springer-Verlag, London, 1993
• 38: Spivey, J. M. 1988. Understanding Z. Cambridge University Press, Cambridge, UK.
• 39: Vera Trnková , Jan Reiterman, Dynamic algebras with test, Journal of Computer and System Sciences, v.35 n.2, p.229-242, Oct. 1987 [doi>10.1016/0022-0000(87)90014-6]

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Correctness proofs

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Mechanical verification; Specification techniques; Assertions; Logics of programs; Invariants; Pre- and post-conditions
      F.3.2 Semantics of Programming Languages
          Subjects: Algebraic approaches to semantics

  I. Computing Methodologies
  I.1 SYMBOLIC AND ALGEBRAIC MANIPULATION
      I.1.3 Languages and Systems
          Subjects: Special-purpose algebraic systems

General Terms:
Theory, Verification

Keywords:
Idempotent semiring, Kleene algebra, codomain, domain, equational reasoning, image and preimage operation, program development and analysis, state transition systems