# Completeness and Incompleteness of Synchronous Kleene Algebra

## TL;DR

This paper investigates the completeness of Synchronous Kleene algebra (SKA), identifies its limitations, and proposes an alternative axiomatization that is both sound and complete with respect to language semantics.

## Contribution

It demonstrates the incompleteness of existing SKA axioms and introduces a new set of axioms based on Salomaa's regular language axiomatization.

## Key findings

- Identified a counterexample showing SKA axioms are incomplete.
- Proposed an alternative axiomatization for SKA.
- Proved the new axioms are sound and complete.

## Abstract

Synchronous Kleene algebra (SKA), an extension of Kleene algebra (KA), was proposed by Prisacariu as a tool for reasoning about programs that may execute synchronously, i.e., in lock-step. We provide a countermodel witnessing that the axioms of SKA are incomplete w.r.t. its language semantics, by exploiting a lack of interaction between the synchronous product operator and the Kleene star. We then propose an alternative set of axioms for SKA, based on Salomaa's axiomatisation of regular languages, and show that these provide a sound and complete characterisation w.r.t. the original language semantics.