带盒的偏序多重集: 并发Kleene代数中的保护、分离与局部性
计算机科学中的逻辑
2020-05-07 v2
摘要
并发Kleene代数是用于关于并发程序的等式推理的优雅工具。CKA所缺失的并发程序的一个重要特征是限制合法交错的能力。为弥补这一点，我们扩展CKA的标准模型即偏序多重集（pomsets），加入一种称为盒的新特征，其可指定系统的一部分受保护以免受外部干扰。我们研究了这一新模型的代数性质。CKA的另一个缺陷是用于表达程序性质的编程语言与用于表达程序本身的编程语言相同。这在实际中往往过于受限。我们提供了一种逻辑，‘偏序多重集逻辑’（pomset logic），作为指定此类性质的断言语言，并在带盒的偏序多重集上给出解释。与其他方法相反，该逻辑不是基于状态的，而是刻画程序的运行时行为。我们发展了偏序多重集逻辑与CKA关系的基本元理论，包括支持局部推理的框架规则，并用简单示例说明了该关系。
引用
@article{arxiv.1910.14384,
title = {Pomsets with Boxes: Protection, Separation, and Locality in Concurrent Kleene Algebra},
author = {Paul Brunet and David Pym},
journal= {arXiv preprint arXiv:1910.14384},
year = {2020}
}