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.

翻译：本文提出并发估值代数（CVA），通过引入遵循弱交换律的并行和顺序两种组合算子，扩展了有序估值代数（OVA）。CVA在规范与建模并发及分布式系统方面具有显著的理论与实践优势。作为域空间上的层，CVA支持局部化规范，促进模块化、组合性以及表示大规模复杂系统的能力。此外，CVA便于基于格的精化推理，并与Hoare逻辑、Rely-Guarantee逻辑等标准方法兼容。我们通过三个分别代表并发/分布式计算不同范式的迹模型展示了CVA的灵活性，并通过态射关联这些模型。同时讨论了将估值代数中强大的局部计算框架引入并发及分布式系统模型检测的潜在应用。