Damien Pous ; Jana Wagemaker - Completeness Theorems for Kleene algebra with tests and top

lmcs:11198 - Logical Methods in Computer Science, September 30, 2024, Volume 20, Issue 3 - https://doi.org/10.46298/lmcs-20(3:27)2024
Completeness Theorems for Kleene algebra with tests and topArticle

Authors: Damien Pous ; Jana Wagemaker

    We prove two completeness results for Kleene algebra with tests and a top element, with respect to guarded string 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. For one of our constructions, we extend the concept of finite monoid recognisability to guarded-string languages; this device makes it possible to obtain a PSpace algorithm for the equational theory of binary relations.


    Volume: Volume 20, Issue 3
    Published on: September 30, 2024
    Accepted on: July 22, 2024
    Submitted on: April 17, 2023
    Keywords: Computer Science - Formal Languages and Automata Theory

    Consultation statistics

    This page has been seen 267 times.
    This article's PDF has been downloaded 73 times.