This paper introduces Concurrent Valuation Algebras (CVAs), extending ordered valuation algebras (OVAs) by incorporating two combine operators representing parallel and sequential products that adhere to a weak exchange law. CVAs present significant theoretical and practical advantages for specifying and modelling concurrent and distributed systems. As a presheaf on a space of domains, a CVA facilitates localised specifications, promoting modularity, compositionality, and the capability to represent large and complex systems. Moreover, CVAs facilitate lattice-based refinement reasoning, and are compatible with standard methodologies such as Hoare and Rely-Guarantee logics. We demonstrate the flexibility of CVAs through three trace models that represent distinct paradigms of concurrent/distributed computing, and interrelate them via morphisms. We also discuss the potential for importing a powerful local computation framework from valuation algebras for the model checking of concurrent and distributed systems.

翻译：本文提出并发估价代数（Concurrent Valuation Algebras, CVAs），通过引入分别表示并行和顺序乘积且服从弱交换律的两个组合算子，对有序估价代数（Ordered Valuation Algebras, OVAs）进行了扩展。CVA为规范与建模并发及分布式系统提供了重要的理论与实践优势。作为域空间上的预层，CVA支持局部化规范，从而促进模块化、组合性，并具备表示大型复杂系统的能力。此外，CVA有助于基于格精化推理，且与霍尔逻辑、依赖保证逻辑等标准方法兼容。本文通过三个表示并发/分布式计算不同范式的迹模型展示了CVA的灵活性，并通过态射建立它们之间的关联。我们还探讨了将估价代数中的强大局部计算框架引入并发及分布式系统模型检测的潜在可能性。