Kleene Algebra with Dynamic Tests: Completeness and Complexity

TL;DR

This paper explores extensions of Kleene algebra with dynamic tests, establishing completeness for relational and guarded-language models, and analyzing the complexity of their equational theories, which are EXPTIME-complete.

Contribution

It introduces a dynamic test framework for Kleene algebra, linking it to propositional dynamic logic and providing completeness and complexity results.

Findings

Completeness results for relational and guarded-language models.

Equational theories are EXPTIME-complete.

Connections between Kleene algebra with tests and propositional dynamic logic.

Abstract

We study versions of Kleene algebra with dynamic tests, that is, extensions of Kleene algebra with domain and antidomain operators. We show that Kleene algebras with tests and Propositional dynamic logic correspond to special cases of the dynamic test framework. In particular, we establish completeness results with respect to relational models and guarded-language models, and we show that two prominent classes of Kleene algebras with dynamic tests have an EXPTIME-complete equational theory.