Words-to-Letters Valuations for Language Kleene Algebras with Variable Complements

TL;DR

This paper studies the equational theory of Kleene algebra with variable complements, introducing words-to-letters valuations to analyze decidability and showing the theory's relation to word equivalence.

Contribution

It introduces words-to-letters valuations for Kleene algebra with variable complements and proves decidability results for certain fragments of the theory.

Findings

Universality problem is coNP-complete.

Inequational theory t <= s is coNP-complete when t lacks Kleene-star.

Equational theory coincides with word equivalence for words with variable complements.

Abstract

We investigate the equational theory of Kleene algebra terms with variable complements -- (language) complement where it applies only to variables -- w.r.t. languages. While the equational theory w.r.t. languages coincides with the language equivalence (under the standard language valuation) for Kleene algebra terms, this coincidence is broken if we extend the terms with complements. In this paper, we prove the decidability of some fragments of the equational theory: the universality problem is coNP-complete, and the inequational theory t <= s is coNP-complete when t does not contain Kleene-star. To this end, we introduce words-to-letters valuations; they are sufficient valuations for the equational theory and ease us in investigating the equational theory w.r.t. languages. Additionally, we prove that for words with variable complements, the equational theory coincides with the word equivalence.