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.
翻译:我们研究带动态测试的Kleene代数变体,即扩展了域算子和反域算子的Kleene代数。研究表明,带测试的Kleene代数与命题动态逻辑对应动态测试框架的特殊情形。特别地,我们建立了关于关系模型和守卫语言模型的完备性结果,并证明两类重要的带动态测试的Kleene代数具有EXPTIME完全的等式理论。