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

TL;DR

This paper explores the decidability and completeness of the equational theory for Kleene algebra with variable and constant complements, introducing words-to-letters valuations to analyze language equivalences.

Contribution

It introduces words-to-letters valuations and proves decidability results for fragments of the theory involving language complements in Kleene algebra.

Findings

Universality problem is coNP-complete.

Inequational theory $t \\le s$ is coNP-complete when $t$ lacks Kleene-star.

Completeness theorem established for words with variable complements and non-empty constant.

Abstract

We investigate the equational theory for Kleene algebra terms with variable complements and constant complements -- (language) complement where it applies only to variables or constants -- 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 \le 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 show a completeness theorem of the equational theory for words with variable complements and the non-empty constant.