部分弦的并发Kleene代数
Concurrent Kleene Algebra of Partial Strings
摘要：
并发Kleene代数（CKA）是Hoare等人最近提出的一种代数结构，它统一了并发编程的规律。CKA的统一力量主要依赖于所谓的交换定律，该定律描述了并发和顺序组合操作符如何互换。本文在前人对真并发性理论研究的基础上，利用最小不动点算子扩展了Gischer的pomset模型，并利用Ésik的单调双射态射形式化了程序精化关系，构造了CKA的偏序模型.当我们想证明和反驳带有循环的并发程序的性质时，这种模型的存在是相关的。特别是，它提供了一个基础的分析程序，同时访问放松的内存中所示的后续工作。
英文摘要：
Concurrent Kleene Algebra (CKA) is a recently proposed algebraic structure by Hoare and collaborators that unifies the laws of concurrent programming. The unifying power of CKA rests largely on the so-called exchange law that describes how concurrent and sequential composition operators can be interchanged. Based on extensive theoretical work on true concurrency in the past, this paper extends Gischer's pomset model with least fixed point operators and formalizes the program refinement relation by Ésik's monotonic bijective morphisms to construct a partial order model of CKA. The existence of such a model is relevant when we want to prove and disprove properties about concurrent programs with loops. In particular, it gives a foundation for the analysis of programs that concurrently access relaxed memory as shown in subsequent work.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
