论文标题
部分可观察的并发kleene代数
Partially Observable Concurrent Kleene Algebra
论文作者
论文摘要
我们引入了部分可观察到的并发Kleene代数（POCKA），这是一个代数框架，以推理与控制结构（例如条件和循环）的并发程序。 Pocka实现了可以访问变量和值的程序的推理，我们通过具体示例说明了这些程序。我们证明，POCKA是部分观测模型的声音和完整的公理化，并显示语义通过对顺序一致性的重要检查。
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.
