{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T05:26:34Z","timestamp":1742966794350,"version":"3.40.3"},"publisher-location":"Cham","reference-count":39,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783031280825"},{"type":"electronic","value":"9783031280832"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,3,8]],"date-time":"2023-03-08T00:00:00Z","timestamp":1678233600000},"content-version":"vor","delay-in-days":66,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Kleene Algebra (KA) is the algebra of regular expressions. Central to the study of KA is Kozen\u2019s (1994) <jats:italic>completeness<\/jats:italic> result, which says that any equivalence valid in the language model of KA follows from the axioms of KA. Also of interest is the <jats:italic>finite model property<\/jats:italic> (FMP), which says that false equivalences always have a finite counterexample. Palka (2005) showed that, for KA, the FMP is equivalent to completeness.<\/jats:p><jats:p>We provide a unified and elementary proof of both properties. In contrast with earlier completeness proofs, this proof does not rely on minimality or bisimilarity techniques for deterministic automata. Instead, our approach avoids deterministic automata altogether, and uses Antimirov\u2019s derivatives and the well-known transition monoid construction.<\/jats:p><jats:p>Our results are fully verified in the Coq proof assistant.<\/jats:p>","DOI":"10.1007\/978-3-031-28083-2_10","type":"book-chapter","created":{"date-parts":[[2023,3,7]],"date-time":"2023-03-07T09:03:07Z","timestamp":1678179787000},"page":"158-175","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Completeness and\u00a0the\u00a0Finite Model Property for\u00a0Kleene Algebra, Reconsidered"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6068-880X","authenticated-orcid":false,"given":"Tobias","family":"Kapp\u00e9","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2023,3,8]]},"reference":[{"key":"10_CR1","doi-asserted-by":"publisher","unstructured":"Anderson, C.J., et al.: NetKAT: semantic foundations for networks. In: POPL, pp. 113\u2013126 (2014). https:\/\/doi.org\/10.1145\/2535838.2535862","DOI":"10.1145\/2535838.2535862"},{"issue":"2","key":"10_CR2","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1016\/0304-3975(95)00182-4","volume":"155","author":"VM Antimirov","year":"1996","unstructured":"Antimirov, V.M.: Partial derivatives of regular expressions and finite automaton constructions. Theor. Comput. Sci. 155(2), 291\u2013319 (1996). https:\/\/doi.org\/10.1016\/0304-3975(95)00182-4","journal-title":"Theor. Comput. Sci."},{"key":"10_CR3","unstructured":"Backhouse, R.: Closure algorithms and the star-height problem of regular languages. Ph.D. thesis, University of London (1975). https:\/\/hdl.handle.net\/10044\/1\/22243"},{"key":"10_CR4","doi-asserted-by":"publisher","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development - Coq\u2019Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. An EATCS Series (2004). https:\/\/doi.org\/10.1007\/978-3-662-07964-5","DOI":"10.1007\/978-3-662-07964-5"},{"key":"10_CR5","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781107050884","volume-title":"Modal Logic, Cambridge Tracts in Theoretical Computer Science","author":"P Blackburn","year":"2001","unstructured":"Blackburn, P., de Rijke, M., Venema, Y.: Modal Logic, Cambridge Tracts in Theoretical Computer Science, vol. 53. Cambridge University Press, Cambridge (2001). https:\/\/doi.org\/10.1017\/CBO9781107050884"},{"key":"10_CR6","doi-asserted-by":"publisher","first-page":"419","DOI":"10.1051\/ita\/1990240404191","volume":"24","author":"M Boffa","year":"1990","unstructured":"Boffa, M.: Une remarque sur les syst\u00e8mes complets d\u2019identit\u00e9s rationnelles. RAIRO Theor. Informatics Appl. 24, 419\u2013423 (1990). https:\/\/doi.org\/10.1051\/ita\/1990240404191","journal-title":"RAIRO Theor. Informatics Appl."},{"issue":"4","key":"10_CR7","doi-asserted-by":"publisher","first-page":"481","DOI":"10.1145\/321239.321249","volume":"11","author":"JA Brzozowski","year":"1964","unstructured":"Brzozowski, J.A.: Derivatives of regular expressions. J. ACM 11(4), 481\u2013494 (1964). https:\/\/doi.org\/10.1145\/321239.321249","journal-title":"J. ACM"},{"key":"10_CR8","series-title":"Graduate Texts in Mathematics","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4613-8130-3","volume-title":"A Course in Universal Algebra","author":"S Burris","year":"1981","unstructured":"Burris, S., Sankappanavar, H.P.: A Course in Universal Algebra. Graduate Texts in Mathematics, Springer, Heidelberg (1981)"},{"key":"10_CR9","unstructured":"Cohen, E., Kozen, D., Smith, F.: The complexity of Kleene algebra with tests. Technical report TR96-1598 (1996). https:\/\/hdl.handle.net\/1813\/7253"},{"key":"10_CR10","volume-title":"Regular Algebra and Finite Machines","author":"JH Conway","year":"1971","unstructured":"Conway, J.H.: Regular Algebra and Finite Machines. Chapman and Hall Ltd., London (1971)"},{"key":"10_CR11","unstructured":"Coq Development Team: The Coq Reference Manual, version 8.15 (2022). https:\/\/coq.inria.fr\/doc"},{"key":"10_CR12","doi-asserted-by":"publisher","unstructured":"Das, A., Doumane, A., Pous, D.: Left-handed completeness for Kleene algebra, via cyclic proofs. In: LPAR, pp. 271\u2013289 (2018). https:\/\/doi.org\/10.29007\/hzq3","DOI":"10.29007\/hzq3"},{"issue":"2","key":"10_CR13","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1007\/s10817-014-9318-9","volume":"54","author":"S Foster","year":"2014","unstructured":"Foster, S., Struth, G.: On the fine-structure of regular Algebra. J. Autom. Reason. 54(2), 165\u2013197 (2014). https:\/\/doi.org\/10.1007\/s10817-014-9318-9","journal-title":"J. Autom. Reason."},{"key":"10_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"375","DOI":"10.1007\/11780274_20","volume-title":"Algebra, Meaning, and Computation","author":"B Jacobs","year":"2006","unstructured":"Jacobs, B.: A bialgebraic review of deterministic automata, regular expressions and languages. In: Futatsugi, K., Jouannaud, J.-P., Meseguer, J. (eds.) Algebra, Meaning, and Computation. LNCS, vol. 4060, pp. 375\u2013404. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11780274_20"},{"key":"10_CR15","doi-asserted-by":"publisher","unstructured":"Kapp\u00e9, T.: Completeness and the finite model property for Kleene algebra, reconsidered (2022). https:\/\/doi.org\/10.48550\/arXiv.2212.10931. (Full version)","DOI":"10.48550\/arXiv.2212.10931"},{"key":"10_CR16","doi-asserted-by":"publisher","unstructured":"Kapp\u00e9, T.: Completeness and the finite model property for Kleene algebra, reconsidered - Coq formalization (2022). https:\/\/doi.org\/10.5281\/zenodo.7467245","DOI":"10.5281\/zenodo.7467245"},{"key":"10_CR17","first-page":"3","volume":"34","author":"SC Kleene","year":"1956","unstructured":"Kleene, S.C.: Representation of events in nerve nets and finite automata. Automata Stud. 34, 3\u201341 (1956)","journal-title":"Automata Stud."},{"issue":"2","key":"10_CR18","doi-asserted-by":"publisher","first-page":"366","DOI":"10.1006\/inco.1994.1037","volume":"110","author":"D Kozen","year":"1994","unstructured":"Kozen, D.: A completeness theorem for Kleene algebras and the algebra of regular events. Inf. Comput. 110(2), 366\u2013390 (1994). https:\/\/doi.org\/10.1006\/inco.1994.1037","journal-title":"Inf. Comput."},{"key":"10_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1007\/3-540-61042-1_35","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Kozen","year":"1996","unstructured":"Kozen, D.: Kleene algebra with tests and commutativity conditions. In: Margaria, T., Steffen, B. (eds.) TACAS 1996. LNCS, vol. 1055, pp. 14\u201333. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/3-540-61042-1_35"},{"issue":"3","key":"10_CR20","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1145\/256167.256195","volume":"19","author":"D Kozen","year":"1997","unstructured":"Kozen, D.: Kleene algebra with tests. ACM Trans. Program. Lang. Syst. 19(3), 427\u2013443 (1997). https:\/\/doi.org\/10.1145\/256167.256195","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"10_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1007\/3-540-44693-1_3","volume-title":"STACS 2001","author":"D Kozen","year":"2001","unstructured":"Kozen, D.: Myhill-Nerode relations on automatic systems and the completeness of Kleene algebra. In: Ferreira, A., Reichel, H. (eds.) STACS 2001. LNCS, vol. 2010, pp. 27\u201338. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-44693-1_3"},{"key":"10_CR22","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"568","DOI":"10.1007\/3-540-44957-4_38","volume-title":"Computational Logic \u2014 CL 2000","author":"D Kozen","year":"2000","unstructured":"Kozen, D., Patron, M.-C.: Certification of compiler optimizations using Kleene algebra with tests. In: Lloyd, J., et al. (eds.) CL 2000. LNCS (LNAI), vol. 1861, pp. 568\u2013582. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/3-540-44957-4_38"},{"key":"10_CR23","doi-asserted-by":"publisher","first-page":"220","DOI":"10.1016\/j.tcs.2019.10.040","volume":"807","author":"D Kozen","year":"2020","unstructured":"Kozen, D., Silva, A.: Left-handed completeness. Theor. Comput. Sci. 807, 220\u2013233 (2020). https:\/\/doi.org\/10.1016\/j.tcs.2019.10.040","journal-title":"Theor. Comput. Sci."},{"key":"10_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1007\/3-540-63172-0_43","volume-title":"Computer Science Logic","author":"D Kozen","year":"1997","unstructured":"Kozen, D., Smith, F.: Kleene algebra with tests: completeness and decidability. In: van Dalen, D., Bezem, M. (eds.) CSL 1996. LNCS, vol. 1258, pp. 244\u2013259. Springer, Heidelberg (1997). https:\/\/doi.org\/10.1007\/3-540-63172-0_43"},{"key":"10_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1007\/978-3-540-70594-9_11","volume-title":"Mathematics of Program Construction","author":"D Kozen","year":"2008","unstructured":"Kozen, D., Tseng, W.-L.D.: The B\u00f6hm\u2013Jacopini theorem is false, propositionally. In: Audebaud, P., Paulin-Mohring, C. (eds.) MPC 2008. LNCS, vol. 5133, pp. 177\u2013192. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-70594-9_11"},{"key":"10_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1007\/BFb0032022","volume-title":"Automata, Languages and Programming","author":"D Krob","year":"1990","unstructured":"Krob, D.: A complete system of B-rational identities. In: Paterson, M.S. (ed.) ICALP 1990. LNCS, vol. 443, pp. 60\u201373. Springer, Heidelberg (1990). https:\/\/doi.org\/10.1007\/BFb0032022"},{"key":"10_CR27","unstructured":"McNaughton, R., Papert, S.: The syntactic monoid of a regular event. Algebraic Theory of Machines, Languages, and Semigroups, pp. 297\u2013312 (1968)"},{"issue":"1","key":"10_CR28","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1109\/TEC.1960.5221603","volume":"9","author":"R McNaughton","year":"1960","unstructured":"McNaughton, R., Yamada, H.: Regular expressions and state graphs for automata. IRE Trans. Electron. Comput. 9(1), 39\u201347 (1960). https:\/\/doi.org\/10.1109\/TEC.1960.5221603","journal-title":"IRE Trans. Electron. Comput."},{"key":"10_CR29","unstructured":"Palka, E.: On finite model property of the equational theory of Kleene algebras. Fundam. Inform. 68(3), 221\u2013230 (2005). https:\/\/content.iospress.com\/articles\/fundamenta-informaticae\/fi68-3-02"},{"key":"10_CR30","doi-asserted-by":"publisher","unstructured":"Pratt, V.R.: Dynamic algebras and the nature of induction. In: STOC, pp. 22\u201328 (1980). https:\/\/doi.org\/10.1145\/800141.804649","DOI":"10.1145\/800141.804649"},{"issue":"1","key":"10_CR31","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/S0304-3975(00)00056-6","volume":"249","author":"JJMM Rutten","year":"2000","unstructured":"Rutten, J.J.M.M.: Universal coalgebra: a theory of systems. Theor. Comput. Sci. 249(1), 3\u201380 (2000). https:\/\/doi.org\/10.1016\/S0304-3975(00)00056-6","journal-title":"Theor. Comput. Sci."},{"issue":"1","key":"10_CR32","doi-asserted-by":"publisher","first-page":"158","DOI":"10.1145\/321312.321326","volume":"13","author":"A Salomaa","year":"1966","unstructured":"Salomaa, A.: Two complete axiom systems for the algebra of regular events. J. ACM 13(1), 158\u2013169 (1966). https:\/\/doi.org\/10.1145\/321312.321326","journal-title":"J. ACM"},{"key":"10_CR33","doi-asserted-by":"publisher","unstructured":"Schmid, T., Kapp\u00e9, T., Kozen, D., Silva, A.: Guarded Kleene algebra with tests: coequations, coinduction, and completeness. In: ICALP, pp. 142:1\u2013142:14 (2021). https:\/\/doi.org\/10.4230\/LIPIcs.ICALP.2021.142","DOI":"10.4230\/LIPIcs.ICALP.2021.142"},{"key":"10_CR34","doi-asserted-by":"publisher","unstructured":"Smolka, S., Eliopoulos, S.A., Foster, N., Guha, A.: A fast compiler for NetKAT. In: ICFP, pp. 328\u2013341 (2015). https:\/\/doi.org\/10.1145\/2784731.2784761","DOI":"10.1145\/2784731.2784761"},{"key":"10_CR35","doi-asserted-by":"publisher","unstructured":"Smolka, S., Foster, N., Hsu, J., Kapp\u00e9, T., Kozen, D., Silva, A.: Guarded Kleene algebra with tests: verification of uninterpreted programs in nearly linear time. In: POPL (2020). https:\/\/doi.org\/10.1145\/3371129","DOI":"10.1145\/3371129"},{"key":"10_CR36","doi-asserted-by":"publisher","unstructured":"Stockmeyer, L.J., Meyer, A.R.: Word problems requiring exponential time: Preliminary report. In: STOC, pp. 1\u20139 (1973). https:\/\/doi.org\/10.1145\/800125.804029","DOI":"10.1145\/800125.804029"},{"key":"10_CR37","unstructured":"Streicher, T.: Investigations into intensional type theory. Habilitiation thesis, Ludwig Maximilian Universit\u00e4t (1993). https:\/\/www2.mathematik.tu-darmstadt.de\/ streicher\/HabilStreicher.pdf"},{"issue":"6","key":"10_CR38","doi-asserted-by":"publisher","first-page":"419","DOI":"10.1145\/363347.363387","volume":"11","author":"K Thompson","year":"1968","unstructured":"Thompson, K.: Regular expression search algorithm. Commun. ACM 11(6), 419\u2013422 (1968). https:\/\/doi.org\/10.1145\/363347.363387","journal-title":"Commun. ACM"},{"key":"10_CR39","unstructured":"Watson, B.W.: A taxonomy of finite automata construction algorithms. Technical report, Technische Universiteit Eindhoven (1993). https:\/\/research.tue.nl\/files\/2482472\/9313452"}],"container-title":["Lecture Notes in Computer Science","Relational and Algebraic Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-28083-2_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,3,12]],"date-time":"2024-03-12T18:40:25Z","timestamp":1710268825000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-28083-2_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031280825","9783031280832"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-28083-2_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"8 March 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"RAMiCS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Relational and Algebraic Methods in Computer Science","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Augsburg","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Germany","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 April 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 April 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ramics2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/ramics20.lis-lab.fr\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Easychair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"26","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"17","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"65% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"17","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}