{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T06:56:33Z","timestamp":1770274593945,"version":"3.49.0"},"reference-count":36,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2006,10,1]],"date-time":"2006-10-01T00:00:00Z","timestamp":1159660800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2006,10]]},"abstract":"<jats:p>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.<\/jats:p>","DOI":"10.1145\/1183278.1183285","type":"journal-article","created":{"date-parts":[[2007,1,16]],"date-time":"2007-01-16T19:38:29Z","timestamp":1168976309000},"page":"798-833","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":121,"title":["Kleene algebra with domain"],"prefix":"10.1145","volume":"7","author":[{"given":"Jules","family":"Desharnais","sequence":"first","affiliation":[{"name":"Universit\u00e9 Laval, Qu\u00e9bec QC, Canada"}]},{"given":"Bernhard","family":"M\u00f6ller","sequence":"additional","affiliation":[{"name":"Universit\u00e4t Augsburg, Augsburg, Germany"}]},{"given":"Georg","family":"Struth","sequence":"additional","affiliation":[{"name":"Universit\u00e4t der Bundeswehr M\u00fcnchen"}]}],"member":"320","published-online":{"date-parts":[[2006,10]]},"reference":[{"key":"e_1_2_1_2_1","volume-title":"The B-Book","author":"Abrial J.-R.","unstructured":"Abrial , J.-R. 1996. The B-Book . Cambridge University Press , Cambridge, UK .]] Abrial, J.-R. 1996. The B-Book. Cambridge University Press, Cambridge, UK.]]"},{"key":"e_1_2_1_3_1","volume-title":"-R","author":"Apt K.-R.","year":"1997","unstructured":"Apt , K.-R. and Olderog , E . -R . 1997 . Verification of Sequential and Concurrent Programs, 2 nd ed. Springer , Berlin.]] Apt, K.-R. and Olderog, E.-R. 1997. Verification of Sequential and Concurrent Programs, 2nd ed. Springer, Berlin.]]","edition":"2"},{"key":"e_1_2_1_4_1","volume-title":"Colloquium Publications","volume":"25","author":"Birkhoff G.","year":"1984","unstructured":"Birkhoff , G. 1984 . Lattice Theory . Colloquium Publications , vol. 25 . American Mathematical Society. (Reprint).]] Birkhoff, G. 1984. Lattice Theory. Colloquium Publications, vol. 25. American Mathematical Society. (Reprint).]]"},{"key":"e_1_2_1_5_1","first-page":"1","article-title":"Basic modal logic. In Handbook of Philosophical Logic, D. Gabbay and F. Guenthner, Eds. vol. II. D. Reidel","author":"Bull R.","year":"1984","unstructured":"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 .]] 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.]]","journal-title":"Chapter"},{"key":"e_1_2_1_6_1","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511621192","volume-title":"Modal Logic: An Introduction","author":"Chellas B. F.","year":"1980","unstructured":"Chellas , B. F. 1980 . Modal Logic: An Introduction . Cambridge University Press , Cambridge, UK .]] Chellas, B. F. 1980. Modal Logic: An Introduction. Cambridge University Press, Cambridge, UK.]]"},{"key":"e_1_2_1_7_1","unstructured":"Cohen E. 1993. Hypotheses in Kleene algebra. Tech. rep. TM-ARH-023814. Bellcore.]]  Cohen E. 1993. Hypotheses in Kleene algebra. Tech. rep. TM-ARH-023814. Bellcore.]]"},{"key":"e_1_2_1_8_1","volume-title":"Proceedings of Mathematics of Program Construction, 5th International Conference, MPC","volume":"1837","author":"Cohen E.","year":"2000","unstructured":"Cohen , E. 2000 . Separation and reduction . In Proceedings of Mathematics of Program Construction, 5th International Conference, MPC 2000, R. Backhouse and J. N. Oliveira, Eds. Lecture Notes in Computer Science , vol. 1837 . Springer, Berlin, 45--59.]] Cohen, E. 2000. Separation and reduction. In Proceedings of Mathematics of Program Construction, 5th International Conference, MPC 2000, R. Backhouse and J. N. Oliveira, Eds. Lecture Notes in Computer Science, vol. 1837. Springer, Berlin, 45--59.]]"},{"key":"e_1_2_1_9_1","volume-title":"Regular Algebra and Finite State Machines","author":"Conway J. H.","unstructured":"Conway , J. H. 1971. Regular Algebra and Finite State Machines . Chapman and Hall .]] Conway, J. H. 1971. Regular Algebra and Finite State Machines. Chapman and Hall.]]"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(99)00079-1"},{"key":"e_1_2_1_11_1","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/S0020-0255(01)00168-2","article-title":"Characterizing determinacy in Kleene algebras","volume":"139","author":"Desharnais J.","year":"2001","unstructured":"Desharnais , J. and M\u00f6ller , B. 2001 . Characterizing determinacy in Kleene algebras . Inf. Sci. 139 , 3 -- 4 , 253--273.]] Desharnais, J. and M\u00f6ller, B. 2001. Characterizing determinacy in Kleene algebras. Inf. Sci. 139, 3--4, 253--273.]]","journal-title":"Inf. Sci."},{"key":"e_1_2_1_12_1","first-page":"93","article-title":"Applications of modal Kleene algebra---a survey","volume":"1","author":"Desharnais J.","year":"2004","unstructured":"Desharnais , J. , M\u00f6ller , B. , and Struth , G. 2004 a. 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.]] Desharnais, J., M\u00f6ller, 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.]]","journal-title":"JoRMiCS---Journal on Relational Methods in Computer Science"},{"key":"e_1_2_1_13_1","volume-title":"Eds. IFIP International Federation for Information Processing Series","volume":"155","author":"Desharnais J.","unstructured":"Desharnais , J. , M\u00f6ller , B. , and Struth , G . 2004b. Termination in modal Kleene algebra. In Exploring New Frontiers of Theoretical Informatics, J.-J. L\u00e9vy, E. Mayr, and J. Mitchell , Eds. IFIP International Federation for Information Processing Series , vol. 155 . Kluwer, 647--660.]] Desharnais, J., M\u00f6ller, B., and Struth, G. 2004b. Termination in modal Kleene algebra. In Exploring New Frontiers of Theoretical Informatics, J.-J. L\u00e9vy, E. Mayr, and J. Mitchell, Eds. IFIP International Federation for Information Processing Series, vol. 155. Kluwer, 647--660.]]"},{"key":"e_1_2_1_14_1","volume-title":"Ed. Lecture Notes in Computer Science","volume":"1816","author":"Desharnais J.","unstructured":"Desharnais , J. , M\u00f6ller , B. , and Tchier , F . 2000. Kleene under a demonic star. In Algebraic Methodology and Software Technology, T. Rus , Ed. Lecture Notes in Computer Science , vol. 1816 . Springer, Berlin, 355--370.]] Desharnais, J., M\u00f6ller, B., and Tchier, F. 2000. Kleene under a demonic star. In Algebraic Methodology and Software Technology, T. Rus, Ed. Lecture Notes in Computer Science, vol. 1816. Springer, Berlin, 355--370.]]"},{"key":"e_1_2_1_15_1","unstructured":"Eilenberg S. 1974. Automata Languages and Machines. vol. A. Academic Press Orlando FL.]]   Eilenberg S. 1974. Automata Languages and Machines. vol. A. Academic Press Orlando FL.]]"},{"key":"e_1_2_1_16_1","doi-asserted-by":"crossref","first-page":"194","DOI":"10.1016\/0022-0000(79)90046-1","article-title":"Propositional dynamic logic of regular programs","volume":"18","author":"Fischer J. M.","year":"1979","unstructured":"Fischer , J. M. and Ladner , R. F. 1979 . Propositional dynamic logic of regular programs . J. Comput. System Sci. 18 , 2, 194 -- 211 .]] Fischer, J. M. and Ladner, R. F. 1979. Propositional dynamic logic of regular programs. J. Comput. System Sci. 18, 2, 194--211.]]","journal-title":"J. Comput. System Sci."},{"key":"e_1_2_1_17_1","volume-title":"Tech. Rep. RR-3088, INRIA- Rocquencourt.]]","author":"Gaubert S.","year":"1997","unstructured":"Gaubert , S. and Plus , M . 1997 . Methods and applications of (max,&plus;) linear algebra. Tech. Rep. RR-3088, INRIA- Rocquencourt.]] Gaubert, S. and Plus, M. 1997. Methods and applications of (max,&plus;) linear algebra. Tech. Rep. RR-3088, INRIA- Rocquencourt.]]"},{"key":"e_1_2_1_18_1","doi-asserted-by":"crossref","first-page":"422","DOI":"10.1007\/BF00370431","article-title":"An algebraic study of well-foundedness","volume":"44","author":"Goldblatt R.","year":"1985","unstructured":"Goldblatt , R. 1985 . An algebraic study of well-foundedness . Studia Logica 44 , 4, 422 -- 437 .]] Goldblatt, R. 1985. An algebraic study of well-foundedness. Studia Logica 44, 4, 422--437.]]","journal-title":"Studia Logica"},{"key":"e_1_2_1_19_1","doi-asserted-by":"crossref","unstructured":"Harel D. Kozen D. and Tiuryn J. 2000. Dynamic Logic. MIT Press Cambridge MA.]]   Harel D. Kozen D. and Tiuryn J. 2000. Dynamic Logic. MIT Press Cambridge MA.]]","DOI":"10.7551\/mitpress\/2516.001.0001"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(94)00205-D"},{"key":"e_1_2_1_21_1","volume-title":"11th International Workshop, CSL'97, M. Nielsen and W. Thomas, Eds. Lecture Notes in Computer Science","volume":"1414","author":"Hollenberg M.","year":"1997","unstructured":"Hollenberg , M. 1997 . Equational axioms of test algebra. In Computer Science Logic , 11th International Workshop, CSL'97, M. Nielsen and W. Thomas, Eds. Lecture Notes in Computer Science , vol. 1414 . Springer, Berlin, 295--310.]] Hollenberg, M. 1997. Equational axioms of test algebra. In Computer Science Logic, 11th International Workshop, CSL'97, M. Nielsen and W. Thomas, Eds. Lecture Notes in Computer Science, vol. 1414. Springer, Berlin, 295--310.]]"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1037"},{"key":"e_1_2_1_24_1","volume-title":"On action algebras","author":"Kozen D.","unstructured":"Kozen , D. 1994b. On action algebras . In Logic and Information Flow, J. van Eijck and A. Visser, Eds. MIT Press, Cambridge , MA , 78--88.]] Kozen, D. 1994b. On action algebras. In Logic and Information Flow, J. van Eijck and A. Visser, Eds. MIT Press, Cambridge, MA, 78--88.]]"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/256167.256195"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/343369.343378"},{"key":"e_1_2_1_27_1","volume-title":"Proceedings of the 10th International Workshop on Computer Science Logic (CSL'96)","volume":"1258","author":"Kozen D.","unstructured":"Kozen , D. and Smith , F . 1996. Kleene algebra with tests: Completeness and decidability . In Proceedings of the 10th International Workshop on Computer Science Logic (CSL'96) , D. van Dalen and M. Bezem, Eds. Lecture Notes in Computer Science , vol. 1258 . Springer, Berlin, 244--259.]] Kozen, D. and Smith, F. 1996. Kleene algebra with tests: Completeness and decidability. In Proceedings of the 10th International Workshop on Computer Science Logic (CSL'96), D. van Dalen and M. Bezem, Eds. Lecture Notes in Computer Science, vol. 1258. Springer, Berlin, 244--259.]]"},{"key":"e_1_2_1_28_1","volume-title":"Handbook of Formal Language Theory","author":"Kuich W.","unstructured":"Kuich , W. 1997. Semirings and formal power series: Their relevance to formal languages and automata . In Handbook of Formal Language Theory , G. Rozenberg and A. Salomaa, Eds. vol. I. Springer , Berlin , 609--677.]] Kuich, W. 1997. Semirings and formal power series: Their relevance to formal languages and automata. In Handbook of Formal Language Theory, G. Rozenberg and A. Salomaa, Eds. vol. I. Springer, Berlin, 609--677.]]"},{"key":"e_1_2_1_29_1","doi-asserted-by":"crossref","unstructured":"Loeckx J. and Sieber K. 1987. The Foundations of Program Verification 2nd ed. Wiley Teubner New York.]]   Loeckx J. and Sieber K. 1987. The Foundations of Program Verification 2nd ed. Wiley Teubner New York.]]","DOI":"10.1007\/978-3-322-96753-4"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.09.069"},{"key":"e_1_2_1_32_1","first-page":"99","article-title":"&","volume":"2","author":"Mulvey C.","year":"1986","unstructured":"Mulvey , C. 1986 . & . Rend. Circ. Math. Palermo 2 , 12, 99 -- 104 .]] Mulvey, C. 1986. &. Rend. Circ. Math. Palermo 2, 12, 99--104.]]","journal-title":"Rend. Circ. Math. Palermo"},{"key":"e_1_2_1_33_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of FCT'81---Fundamentals of Computation Theory","author":"N\u00e9meti I.","unstructured":"N\u00e9meti , I. 1981. Dynamic algebras of programs . In Proceedings of FCT'81---Fundamentals of Computation Theory . Lecture Notes in Computer Science , vol. 117 . Springer , Berlin , 281--291.]] N\u00e9meti, I. 1981. Dynamic algebras of programs. In Proceedings of FCT'81---Fundamentals of Computation Theory. Lecture Notes in Computer Science, vol. 117. Springer, Berlin, 281--291.]]"},{"key":"e_1_2_1_34_1","volume-title":"Proceegings of the Conference on Algebra and Computer Science, D. Pigozzi, Ed. Lecture Notes in Computer Science","volume":"425","author":"Pratt V.","year":"1988","unstructured":"Pratt , V. 1988 . Dynamic logic as a well-behaved fragment of relation algebras . In Proceegings of the Conference on Algebra and Computer Science, D. Pigozzi, Ed. Lecture Notes in Computer Science , vol. 425 . Springer, Berlin, 77--110.]] Pratt, V. 1988. Dynamic logic as a well-behaved fragment of relation algebras. In Proceegings of the Conference on Algebra and Computer Science, D. Pigozzi, Ed. Lecture Notes in Computer Science, vol. 425. Springer, Berlin, 77--110.]]"},{"key":"e_1_2_1_35_1","volume-title":"European Workshop, JELIA'90","volume":"478","author":"Pratt V.","year":"1990","unstructured":"Pratt , V. 1990 . Action logic and pure induction. In Logics in AI , European Workshop, JELIA'90 , J. van Eijck, Ed. Lecture Notes in Computer Science , vol. 478 . Springer, Berlin, 97--110.]] Pratt, V. 1990. Action logic and pure induction. In Logics in AI, European Workshop, JELIA'90, J. van Eijck, Ed. Lecture Notes in Computer Science, vol. 478. Springer, Berlin, 97--110.]]"},{"key":"e_1_2_1_36_1","doi-asserted-by":"crossref","first-page":"571","DOI":"10.1007\/BF00370685","article-title":"Dynamic algebras: Examples, constructions, applications","volume":"50","author":"Pratt V.","year":"1991","unstructured":"Pratt , V. 1991 . Dynamic algebras: Examples, constructions, applications . Studia Logica 50 , 571 -- 605 .]] Pratt, V. 1991. Dynamic algebras: Examples, constructions, applications. Studia Logica 50, 571--605.]]","journal-title":"Studia Logica"},{"key":"e_1_2_1_37_1","unstructured":"Schmidt G. W. and Str\u00f6hlein T. 1993. Relations and Graphs: Discrete Mathematics for Computer Scientists. EATCS Monographs on Theoretical Computer Science. Springer Berlin.]]   Schmidt G. W. and Str\u00f6hlein T. 1993. Relations and Graphs: Discrete Mathematics for Computer Scientists. EATCS Monographs on Theoretical Computer Science. Springer Berlin.]]"},{"key":"e_1_2_1_38_1","volume-title":"Cambridge University Press","author":"Spivey J. M.","unstructured":"Spivey , J. M. 1988. Understanding Z. Cambridge University Press , Cambridge, UK .]] Spivey, J. M. 1988. Understanding Z. Cambridge University Press, Cambridge, UK.]]"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(87)90014-6"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1183278.1183285","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1183278.1183285","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T15:06:37Z","timestamp":1750259197000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1183278.1183285"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,10]]},"references-count":36,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2006,10]]}},"alternative-id":["10.1145\/1183278.1183285"],"URL":"https:\/\/doi.org\/10.1145\/1183278.1183285","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"value":"1529-3785","type":"print"},{"value":"1557-945X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006,10]]},"assertion":[{"value":"2006-10-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}