This paper introduces Concurrent Valuation Algebras (CVAs), a novel extension of ordered valuation algebras (OVAs). CVAs include two combine operators representing parallel and sequential products, adhering to a weak exchange law. This development offers theoretical and practical benefits for the specification and modelling of concurrent and distributed systems. As a presheaf on a space of domains, CVAs enable localised specifications, supporting modularity, compositionality, and the ability to represent large and complex systems. Furthermore, CVAs align with lattice-based refinement reasoning and are compatible with established methodologies such as Hoare and Rely-Guarantee logics. The flexibility of CVAs is explored through three trace models, illustrating distinct paradigms of concurrent/distributed computing, interrelated by morphisms. The paper also highlights the potential to incorporate a powerful local computation framework from valuation algebras for model checking in concurrent and distributed systems. The foundational results presented have been verified with the proof assistant Isabelle/HOL.

翻译：本文提出了并发估值代数（Concurrent Valuation Algebras，CVA），这是有序估值代数（Ordered Valuation Algebras，OVA）的一种新颖扩展。CVA包含两个组合算子，分别表示并行和顺序乘积，并遵循弱交换律。这一发展在理论及实践上为并发与分布式系统的规范与建模提供了优势。作为域空间上的预层，CVA支持局部化规范，促进了模块化、组合性，并能够表示大型复杂系统。此外，CVA与基于格精化的推理方法一致，且兼容已有的方法论，如霍尔逻辑（Hoare logic）和保证-依赖逻辑（Rely-Guarantee logics）。本文通过三个迹模型探索了CVA的灵活性，展示了并发/分布式计算的不同范式，并通过态射相互关联。论文还强调了将估值代数中强大的局部计算框架应用于并发与分布式系统模型检查的潜力。文中所呈现的基础性结果已通过证明助手Isabelle/HOL验证。