A complete axiomatisation of reversible Kleene lattices

Partially Observable Concurrent Kleene Algebra

We introduce partially observable concurrent Kleene algebra (POCKA), an algebraic framework to reason about concurrent programs with control structures, such as conditionals and loops. POCKA enables reasoning about programs that can access variables and values, which we illustrate through concrete examples. We prove that POCKA is a sound and complete axiomatisation of a model of partial observations, and show the semantics passes an important check for sequential consistency.

Concurrent Dynamic Algebra

We reconstruct Peleg's concurrent dynamic logic in the context of modal Kleene algebras. We explore the algebraic structure of its multirelational semantics and develop an abstract axiomatisation of concurrent dynamic algebras from that basis. In this axiomatisation, sequential composition is not associative. It interacts with concurrent composition through a weak distributivity law. The modal operators of concurrent dynamic algebra are obtained from abstract axioms for domain and antidomain operators; the Kleene star is modelled as a least fixpoint. Algebraic variants of Peleg's axioms are sh…

Completeness and Incompleteness of Synchronous Kleene Algebra

Synchronous Kleene algebra (SKA), an extension of Kleene algebra (KA), was proposed by Prisacariu as a tool for reasoning about programs that may execute synchronously, i.e., in lock-step. We provide a countermodel witnessing that the axioms of SKA are incomplete w.r.t. its language semantics, by exploiting a lack of interaction between the synchronous product operator and the Kleene star. We then propose an alternative set of axioms for SKA, based on Salomaa's axiomatisation of regular languages, and show that these provide a sound and complete characterisation w.r.t. the original language se…

Free Kleene algebras with domain

First we identify the free algebras of the class of algebras of binary relations equipped with the composition and domain operations. Elements of the free algebras are pointed labelled finite rooted trees. Then we extend to the analogous case when the signature includes all the Kleene algebra with domain operations; that is, we add union and reflexive transitive closure to the signature. In this second case, elements of the free algebras are 'regular' sets of the trees of the first case. As a corollary, the axioms of domain semirings provide a finite quasiequational axiomatisation of the equat…

带有假设的连续代数

Continuous Algebras with Hypotheses

本文提出一个统一的框架，涵盖Kleene代数的各种变体以及正则树语言，通过考虑由完全格有序的代数，其中可以计算最小固定点，并提供一个由封闭语言组成的标准模型，证明其在所有连续模型上都是正确且完整的。此外，本文研究了准等式公理化，并展示了如何通过模块化的方式获得完整公理化，从而在每个情况下证明了交换Kleene代数、bi-KA和正则树语言在不同假设下的完备性。

带有Hoare假设的守卫Kleene代数与测试

GKAT with Hoare Hypotheses

提出在GKAT中引入Hoare假设以建模基本程序的前后条件，证明公理化系统的完备性，并扩展为单词假设，基于自动机理论证明等价性判定效率与普通GKAT相同。