Damien Pous ; Jurriaan Rot ; Jana Wagemaker - On Tools for Completeness of Kleene Algebra with Hypotheses

lmcs:10197 - Logical Methods in Computer Science, May 16, 2024, Volume 20, Issue 2 - https://doi.org/10.46298/lmcs-20(2:8)2024
On Tools for Completeness of Kleene Algebra with HypothesesArticle

Authors: Damien Pous ; Jurriaan Rot ; Jana Wagemaker

    In the literature on Kleene algebra, a number of variants have been proposed which impose additional structure specified by a theory, such as Kleene algebra with tests (KAT) and the recent Kleene algebra with observations (KAO), or make specific assumptions about certain constants, as for instance in NetKAT. Many of these variants fit within the unifying perspective offered by Kleene algebra with hypotheses, which comes with a canonical language model constructed from a given set of hypotheses. For the case of KAT, this model corresponds to the familiar interpretation of expressions as languages of guarded strings. A relevant question therefore is whether Kleene algebra together with a given set of hypotheses is complete with respect to its canonical language model. In this paper, we revisit, combine and extend existing results on this question to obtain tools for proving completeness in a modular way. We showcase these tools by giving new and modular proofs of completeness for KAT, KAO and NetKAT, and we prove completeness for new variants of KAT: KAT extended with a constant for the full relation, KAT extended with a converse operation, and a version of KAT where the collection of tests only forms a distributive lattice.


    Volume: Volume 20, Issue 2
    Published on: May 16, 2024
    Accepted on: April 19, 2024
    Submitted on: October 25, 2022
    Keywords: Computer Science - Logic in Computer Science
    Funding:
      Source : OpenAIRE Graph
    • PROJET AVENIR LYON SAINT-ETIENNE; Funder: French National Research Agency (ANR); Code: ANR-11-IDEX-0007
    • Community of mathematics and fundamental computer science in Lyon; Funder: French National Research Agency (ANR); Code: ANR-10-LABX-0070
    • Coinduction for Verification and Certification; Funder: European Commission; Code: 678157

    Consultation statistics

    This page has been seen 1072 times.
    This article's PDF has been downloaded 365 times.