arXivDaily arXiv每日学术速递 周一至周五更新
arXiv 2007.07593cs.LOcs.FLcs.PL
收藏

部分可观测的并发Kleene代数

Partially Observable Concurrent Kleene Algebra

Jana Wagemaker, Paul Brunet, Simon Docherty, Tobias Kappé, Jurriaan Rot, Alexandra Silva

摘要:

我们引入部分可观察并发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.

机构、总结、中文摘要均由AI分析而来,可能存在错误,请以论文正文为准。

↑