可逆演算中基于独立性的并发、因果与冲突
Concurrency, Causality and Conflict via Independence in Reversible Calculi
浏览论文内容
中文总结 AI 辅助
本文在可逆演算中引入独立性概念，证明预可逆系统具有唯一独立性及真并发关系，给出因果与冲突的独立性刻画，并通过Beluga验证两个演算中独立性与依赖性的性质，最后探讨其扩展应用。
中文摘要 AI 辅助
在探讨进程演算语义的不同方法中，真并发模型因其能够揭示事件之间微妙的相互作用而脱颖而出。其核心在于三个关键关系：并发、因果与冲突。本文表明，可逆性在赋予独立性概念后，为研究和刻画这些真并发关系提供了丰富的工具。首先，我们证明，允许预可逆性（即可以通过满足一些基本公理的独立性关系进行扩展）的系统具有唯一的独立性、事件、并发、因果与冲突概念。接着，我们分析独立性与真并发关系之间的联系，建立了基于独立性的因果与冲突的新刻画。我们的第二系列贡献围绕两个具体的进程演算以及在其转移标签上定义的两种句法概念，即独立性与依赖性；我们证明它们划分了连接的转移，并优雅地刻画了相邻转移上的并发性。这部分开发工作使用了证明助手Beluga进行了机器验证。最后，我们研究可逆进程代数中常用的关键机制如何作为代理来检索过去事件上的因果与核心独立性。我们通过讨论我们的结果如何扩展到可逆系统之外来结束本文。
英文摘要
Among the different ways of approaching the semantics of process calculi, true-concurrency models stand out for their ability to highlight subtle interplays between events. At their heart lie three crucial relations: concurrency, causality and conflict. This paper shows that reversibility, when endowed with a notion of independence, provides a rich tooling to study and characterise these true-concurrency relations. First, we prove that systems admitting pre-reversibility (i.e., that can be extended with an independence relation satisfying some basic axioms) have a unique notion of independence, events, concurrency, causality and conflict. We then analyse the relationship between independence and the true-concurrency relations, establishing novel independence-based characterisations of causality and conflict. Our second series of contributions revolves around two concrete process calculi and two syntactic notions defined on their transition labels, namely independence and dependence; we prove that they partition connected transitions and characterise elegantly concurrency on adjacent transitions. This part of our development was machine-checked using the proof assistant Beluga. Last, we study how the key mechanism commonly used in reversible process algebra can be used as a proxy to retrieve causality and core independence on past events. We conclude by discussing how our results extend beyond reversible systems.
发表机构
- Augusta University（奥古斯塔大学）
- Imperial College London（伦敦帝国学院）
- IAR Nagoya University（名古屋大学国际学术研究院）
- AGH University of Kraków（克拉科夫AGH科技大学）
- University of Leicester（莱斯特大学）
机构由 AI 辅助整理，请以论文原文为准。
