REVIEW 3 cited by
Kleene Algebra with Dynamic Tests: Completeness and Complexity
Not yet reviewed by Pith; the record is open.
This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.
SPECIMEN: schema-true, not a live event
T0 review · schema-true
One-sentence machine reading of the paper's core claim.
pith:XXXXXXXX · record.json · timestamp
read the original 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.
Forward citations
Cited by 3 Pith papers
-
The Equational Theory of Relational Kleene Algebra with Graph Loop is PSPACE-Complete
The equational theory of relational Kleene algebra with graph loop is PSPACE-complete, and this PSPACE bound extends to top, tests, converse, and nominals, resolving the complexity of relational KAT with domain.
-
Algebras for Deterministic Computation Are Inherently Incomplete
No finite set of regular control-flow operations generates the deterministic fragment of Kleene Algebra with Tests, so GKAT and all its finite regular extensions remain expressively incomplete.
-
On Propositional Program Equivalence (extended abstract)
The paper reviews GKAT, an algebraic framework with a nearly linear-time decision procedure for propositional program equivalence, and surveys open problems in its axiomatization and expressivity.
Discussion (0). Continue with ORCID to comment.