{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T05:20:29Z","timestamp":1776316829028,"version":"3.50.1"},"publisher-location":"Cham","reference-count":29,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030452308","type":"print"},{"value":"9783030452315","type":"electronic"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Concurrent Kleene Algebra (CKA) extends basic Kleene algebra with a parallel composition operator, which enables reasoning about concurrent programs. However, CKA fundamentally misses<jats:italic>tests<\/jats:italic>, which are needed to model standard programming constructs such as conditionals and<jats:inline-formula><jats:alternatives><jats:tex-math>$$\\mathsf {while}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:mi>while<\/mml:mi><\/mml:math><\/jats:alternatives><\/jats:inline-formula>-loops. It turns out that integrating tests in CKA is subtle, due to their interaction with parallelism. In this paper we provide a solution in the form of Concurrent Kleene Algebra with Observations (CKAO). Our main contribution is a completeness theorem for CKAO. Our result resorts on a more general study of CKA \u201cwith hypotheses\u201d, of which CKAO turns out to be an instance: this analysis is of independent interest, as it can be applied to extensions of CKA other than CKAO.<\/jats:p>","DOI":"10.1007\/978-3-030-45231-5_20","type":"book-chapter","created":{"date-parts":[[2020,4,17]],"date-time":"2020-04-17T10:02:53Z","timestamp":1587117773000},"page":"381-400","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["Concurrent Kleene Algebra with Observations: From Hypotheses to Completeness"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6068-880X","authenticated-orcid":false,"given":"Tobias","family":"Kapp\u00e9","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9762-6872","authenticated-orcid":false,"given":"Paul","family":"Brunet","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5014-9784","authenticated-orcid":false,"given":"Alexandra","family":"Silva","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8616-3905","authenticated-orcid":false,"given":"Jana","family":"Wagemaker","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6457-1345","authenticated-orcid":false,"given":"Fabio","family":"Zanasi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2020,4,17]]},"reference":[{"key":"20_CR1","doi-asserted-by":"crossref","unstructured":"Anderson, C.J., Foster, N., Guha, A., Jeannin, J.B., Kozen, D., Schlesinger, C., Walker, D.: NetKAT: Semantic foundations for networks. In: POPL. pp. 113\u2013126. ACM (2014)","DOI":"10.1145\/2578855.2535862"},{"key":"20_CR2","unstructured":"Birkhoff, G., Bartee, T.C.: Modern applied algebra. McGraw-Hill (1970)"},{"key":"20_CR3","doi-asserted-by":"crossref","unstructured":"Bonchi, F., Pous, D.: Checking NFA equivalence with bisimulations up to congruence. In: POPL. pp. 457\u2013468 (2013)","DOI":"10.1145\/2480359.2429124"},{"key":"20_CR4","unstructured":"Brunet, P., Pous, D., Struth, G.: On decidability of concurrent Kleene algebra. In: CONCUR. pp. 28:1\u201328:15 (2017)"},{"key":"20_CR5","unstructured":"Cohen, E.: Hypotheses in Kleene algebra. Tech. rep., Bellcore (1994)"},{"key":"20_CR6","unstructured":"Conway, J.H.: Regular Algebra and Finite Machines. Chapman and Hall, Ltd., London (1971)"},{"key":"20_CR7","doi-asserted-by":"crossref","unstructured":"Doumane, A., Kuperberg, D., Pous, D., Pradic, P.: Kleene algebra with hypotheses. In: FOSSACS. pp. 207\u2013223 (2019)","DOI":"10.1007\/978-3-030-17127-8_12"},{"key":"20_CR8","doi-asserted-by":"crossref","unstructured":"Foster, N., Kozen, D., Milano, M., Silva, A., Thompson, L.: A coalgebraic decision procedure for NetKAT. In: POPL. pp. 343\u2013355 (2015)","DOI":"10.1145\/2775051.2677011"},{"key":"20_CR9","unstructured":"Gischer, J.L.: The equational theory of pomsets. Theor. Comput. Sci. 61, 199\u2013224 (1988)"},{"key":"20_CR10","doi-asserted-by":"crossref","unstructured":"Grabowski, J.: On partial languages. Fundam. Inform. 4(2), 427 (1981)","DOI":"10.3233\/FI-1981-4210"},{"key":"20_CR11","doi-asserted-by":"crossref","unstructured":"Hoare, T., M\u00f6ller, B., Struth, G., Wehrman, I.: Concurrent Kleene algebra. In: CONCUR. pp. 399\u2013414 (2009)","DOI":"10.1007\/978-3-642-04081-8_27"},{"key":"20_CR12","unstructured":"Jipsen, P., Moshier, M.A.: Concurrent Kleene algebra with tests and branching automata. J. Log. Algebr. Meth. Program. 85(4), 637\u2013652 (2016)"},{"key":"20_CR13","unstructured":"Kapp\u00e9, T., Brunet, P., Rot, J., Silva, A., Wagemaker, J., Zanasi, F.: Kleene algebra with observations. In: CONCUR. pp. 41:1\u201341:16 (2019)"},{"key":"20_CR14","unstructured":"Kapp\u00e9, T., Brunet, P., Silva, A., Wagemaker, J., Zanasi, F.: Concurrent Kleene algebra with observations: from hypotheses to completeness (2020), arXiv:2002.09682"},{"key":"20_CR15","doi-asserted-by":"crossref","unstructured":"Kapp\u00e9, T., Brunet, P., Silva, A., Zanasi, F.: Concurrent Kleene algebra: Free model and completeness. In: ESOP. pp. 856\u2013882 (2018)","DOI":"10.1007\/978-3-319-89884-1_30"},{"key":"20_CR16","unstructured":"Kozen, D.: A completeness theorem for Kleene algebras and the algebra of regular events. Inf. Comput. 110(2), 366\u2013390 (1994)"},{"key":"20_CR17","doi-asserted-by":"crossref","unstructured":"Kozen, D.: Kleene algebra with tests and commutativity conditions. In: TACAS. pp. 14\u201333 (1996)","DOI":"10.1007\/3-540-61042-1_35"},{"key":"20_CR18","unstructured":"Kozen, D.: On the complexity of reasoning in Kleene algebra. Inf. Comput. 179(2), 152\u2013162 (2002)"},{"key":"20_CR19","doi-asserted-by":"crossref","unstructured":"Kozen, D.: On the coalgebraic theory of Kleene algebra with tests. In: Ba\u015fkent, C., Moss, L.S., Ramanujam, R. (eds.) Rohit Parikh on Logic, Language and Society, Outstanding Contributions to Logic, vol.\u00a011, pp. 279\u2013298. Springer (2017)","DOI":"10.1007\/978-3-319-47843-2_15"},{"key":"20_CR20","doi-asserted-by":"crossref","unstructured":"Kozen, D., Mamouras, K.: Kleene algebra with equations. In: ICALP. pp. 280\u2013292 (2014)","DOI":"10.1007\/978-3-662-43951-7_24"},{"key":"20_CR21","doi-asserted-by":"crossref","unstructured":"Krob, D.: A complete system of B-rational identities. In: ICALP. pp. 60\u201373 (1990)","DOI":"10.1007\/BFb0032022"},{"key":"20_CR22","doi-asserted-by":"crossref","unstructured":"Kuratowski, C.: Sur l\u2019op\u00e9ration \u0100 de l\u2019Analysis Situs. Fundamenta Mathematicae 3(1), 182\u2013199 (1922)","DOI":"10.4064\/fm-3-1-182-199"},{"key":"20_CR23","doi-asserted-by":"crossref","unstructured":"Laurence, M.R., Struth, G.: Completeness theorems for bi-Kleene algebras and series-parallel rational pomset languages. In: RAMiCS. pp. 65\u201382 (2014)","DOI":"10.1007\/978-3-319-06251-8_5"},{"key":"20_CR24","unstructured":"Laurence, M.R., Struth, G.: Completeness theorems for pomset languages and concurrent Kleene algebras (2017), arXiv:1705.05896"},{"key":"20_CR25","doi-asserted-by":"crossref","unstructured":"Lodaya, K., Weil, P.: Series-parallel languages and the bounded-width property. Theoretical Computer Science 237(1), 347\u2013380 (2000)","DOI":"10.1016\/S0304-3975(00)00031-1"},{"key":"20_CR26","doi-asserted-by":"crossref","unstructured":"Prisacariu, C.: Synchronous Kleene algebra. The Journal of Logic and Algebraic Programming 79(7), 608 \u2013 635 (2010)","DOI":"10.1016\/j.jlap.2010.07.009"},{"key":"20_CR27","doi-asserted-by":"crossref","unstructured":"Salomaa, A.: Two complete axiom systems for the algebra of regular events. J. ACM 13(1), 158\u2013169 (1966)","DOI":"10.1145\/321312.321326"},{"key":"20_CR28","doi-asserted-by":"crossref","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. pp. 61:1\u201361:28 (2020)","DOI":"10.1145\/3371129"},{"key":"20_CR29","doi-asserted-by":"crossref","unstructured":"Wagemaker, J., Bonsangue, M., Kapp\u00e9, T., Rot, J., Silva, A.: Completeness and incompleteness of synchronous Kleene algebra. In: MPC (2019)","DOI":"10.1007\/978-3-030-33636-3_14"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-45231-5_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,10,21]],"date-time":"2022-10-21T15:48:56Z","timestamp":1666367336000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-45231-5_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030452308","9783030452315"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-45231-5_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"17 April 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FoSSaCS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Foundations of Software Science and Computation Structures","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Dublin","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Ireland","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 April 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30 April 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fossacs2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.etaps.org\/2020\/fossacs","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":"98","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":"31","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":"32% - 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":"12","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)"}},{"value":"The conference could not take place due to the COVID-19 pandemic. There was an online event on July 2, 2020.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}