并发估值代数的追踪模型
摘要：并发估值代数（CVAs）是有序估值代数（OVAs）的一种新的扩展，包含表示并行和顺序运算的两个组合操作符，并遵循弱交换法则。该发展在并发和分布式系统的规范和建模方面具有理论和实际的好处。作为定义在域空间上的前函子，CVAs能够进行局部化规范，支持模块化、组合性和表示大型复杂系统的能力。此外，CVAs与基于格的细化推理相一致，并与Hoare和Rely-Guarantee逻辑等已有方法论兼容。CVAs的灵活性通过三个跟踪模型来探索，这些模型展示了并发/分布式计算的不同范式，并通过态射相互关联。该论文还突出了在并发和分布式系统的模型检验中，结合估值代数的强大本地计算框架的潜力。所提出的基础结果已经通过证明助手Isabelle/HOL进行验证。
作者：Naso Evangelou-Oost, Larissa Meinicke, Callum Bannister, Ian J. Hayes
论文ID：2305.18017
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-08-22