Completeness Theorems for Kleene Algebra with Top

Autor:	Pous, Damien, Wagemaker, Jana
Přispěvatelé:	Preuves et Langages (PLUME), Laboratoire de l'Informatique du Parallélisme (LIP), Centre National de la Recherche Scientifique (CNRS)-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-École normale supérieure - Lyon (ENS Lyon)-Centre National de la Recherche Scientifique (CNRS)-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-École normale supérieure - Lyon (ENS Lyon), Radboud university [Nijmegen], Plume, ANR-10-LABX-0070,MILYON,Community of mathematics and fundamental computer science in Lyon(2010), European Project: 678157,H2020,ERC-2015-STG,CoVeCe(2016), École normale supérieure de Lyon (ENS de Lyon)-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure de Lyon (ENS de Lyon)-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS), Radboud University [Nijmegen]
Jazyk:	angličtina
Rok vydání:	2022
Předmět:	Completeness Kleene algebra Closed languages Hypotheses Theory of computation → Equational logic and rewriting [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] Theory of computation → Regular languages Theory of computation → Logic and verification
Zdroj:	CONCUR CONCUR, Sep 2022, Varsovie, Poland. ⟨10.4230/LIPIcs.CONCUR.2022.26⟩
DOI:	10.4230/LIPIcs.CONCUR.2022.26⟩
Popis:	We prove two completeness results for Kleene algebra with a top element, with respect to languages and binary relations. While the equational theories of those two classes of models coincide over the signature of Kleene algebra, this is no longer the case when we consider an additional constant "top" for the full element. Indeed, the full relation satisfies more laws than the full language, and we show that those additional laws can all be derived from a single additional axiom. We recover that the two equational theories coincide if we slightly generalise the notion of relational model, allowing sub-algebras of relations where top is a greatest element but not necessarily the full relation. We use models of closed languages and reductions in order to prove our completeness results, which are relative to any axiomatisation of the algebra of regular events. LIPIcs, Vol. 243, 33rd International Conference on Concurrency Theory (CONCUR 2022), pages 26:1-26:18
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=doi_dedup___::04631926ed9d6abb7765e6cd9fb936c5 https://hal.archives-ouvertes.fr/hal-03644317/document Zobrazit plný text záznamu