{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T21:16:25Z","timestamp":1779138985951,"version":"3.51.4"},"reference-count":0,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>In the literature on Kleene algebra, a number of variants have been proposed\nwhich impose additional structure specified by a theory, such as Kleene algebra\nwith tests (KAT) and the recent Kleene algebra with observations (KAO), or make\nspecific assumptions about certain constants, as for instance in NetKAT. Many\nof these variants fit within the unifying perspective offered by Kleene algebra\nwith hypotheses, which comes with a canonical language model constructed from a\ngiven set of hypotheses. For the case of KAT, this model corresponds to the\nfamiliar interpretation of expressions as languages of guarded strings. A\nrelevant question therefore is whether Kleene algebra together with a given set\nof hypotheses is complete with respect to its canonical language model. In this\npaper, we revisit, combine and extend existing results on this question to\nobtain tools for proving completeness in a modular way. We showcase these tools\nby giving new and modular proofs of completeness for KAT, KAO and NetKAT, and\nwe prove completeness for new variants of KAT: KAT extended with a constant for\nthe full relation, KAT extended with a converse operation, and a version of KAT\nwhere the collection of tests only forms a distributive lattice.<\/jats:p>","DOI":"10.46298\/lmcs-20(2:8)2024","type":"journal-article","created":{"date-parts":[[2024,5,16]],"date-time":"2024-05-16T10:10:08Z","timestamp":1715854208000},"source":"Crossref","is-referenced-by-count":5,"title":["On Tools for Completeness of Kleene Algebra with Hypotheses"],"prefix":"10.46298","volume":"Volume 20, Issue 2","author":[{"given":"Damien","family":"Pous","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jurriaan","family":"Rot","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jana","family":"Wagemaker","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"25203","published-online":{"date-parts":[[2024,5,16]]},"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/13603\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/13603\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,5,16]],"date-time":"2024-05-16T10:10:09Z","timestamp":1715854209000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/10197"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,5,16]]},"references-count":0,"URL":"https:\/\/doi.org\/10.46298\/lmcs-20(2:8)2024","relation":{"has-preprint":[{"id-type":"arxiv","id":"2210.13020v3","asserted-by":"subject"},{"id-type":"arxiv","id":"2210.13020v2","asserted-by":"subject"},{"id-type":"arxiv","id":"2210.13020v1","asserted-by":"subject"}],"is-same-as":[{"id-type":"arxiv","id":"2210.13020","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.2210.13020","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"value":"1860-5974","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,5,16]]},"article-number":"10197"}}