论文标题
并发的Kleene代数与观察：从假设到完整性
Concurrent Kleene Algebra with Observations: from Hypotheses to Completeness
论文作者
论文摘要
并发Kleene代数（CKA）使用平行的组成运算符扩展了基本的Kleene代数，这使得有关并发程序的推理。但是，CKA从根本上错过了测试，这是为标准编程结构（例如条件和$ \ Mathsf {while} $ - loops建模所需的测试。事实证明，由于它们与并行性的相互作用，在CKA中集成测试是微妙的。在本文中，我们提供了一种与观测值（CKAO）并发的Kleene代数形式的解决方案。我们的主要贡献是CKAO的完整定理。我们的结果对CKA的“假设”进行了更一般的研究，其中CKAO被证明是一个例子：这种分析具有独立的兴趣，因为它可以应用于CKA的扩展。
Concurrent Kleene Algebra (CKA) extends basic Kleene algebra with a parallel composition operator, which enables reasoning about concurrent programs. However, CKA fundamentally misses tests, which are needed to model standard programming constructs such as conditionals and $\mathsf{while}$-loops. It turns out that integrating tests in CKA is subtle, due to their interaction with parallelism. In this paper we provide a solution in the form of Concurrent Kleene Algebra with Observations (CKAO). Our main contribution is a completeness theorem for CKAO. Our result resorts on a more general study of CKA "with hypotheses", of which CKAO turns out to be an instance: this analysis is of independent interest, as it can be applied to extensions of CKA other than CKAO.
