摘要
The algebraic specification and representation of networks of agents have been greatly impacted by the study of reversible phenomena: reversible declensions of the calculus of communicating systems (CCSK and RCCS) offer new semantic models, finer congruence relations, original properties, and revisits existing theories and results in a finer light. But much remains to be done: concurrency, a central notion in establishing causal consistency–a crucial property for reversible systems–, was never given a syntactical definition in CCSK. We remedy this gap by leveraging a definition of concurrency developed for forward-only calculi using proved transition systems, and prove that CCSK still enjoys causal consistency for this elegant and syntactical notion of reversible concurrency. We also compare it to a definition of concurrency inspired by reversible \(\pi \)-calculus, discuss its relation with structural congruence, and prove that it can be adapted to any CCS-inspired reversible system and is equivalent—or refines—existing definitions of concurrency for those systems.
摘要译文
可逆现象的研究极大地影响了代理网络的代数规范和表示：通信系统计算（CCSK和RCCS）的可逆下降（CCSK和RCCS）提供了新的语义模型，更充分的一致性关系，原始属性，原始属性，以及Revisories现有理论和现有理论和现有理论和现有理论和现有理论和属性产生更好的光。但是还有很多事情要做：并发是建立因果一致性的中心概念，这是可逆系统的关键特性，从未在CCSK中给出句法定义。我们通过利用证明的过渡系统为远期的微积分开发的并发定义来纠正这一差距，并证明CCSK仍然对这种优雅而句法的可逆并发性概念享有因果关系。我们还将其与受可逆\（\ pi \）的启发的并发定义进行了比较 - 计算，讨论其与结构一致性的关系，并证明它可以适应任何CCS启发的可逆系统，并且是等效的（或完善）这些系统并发的定义。
Clément Aubert[1];Claudio Antares Mezzina[2];Dr. Krzysztof Podlaski[3]. Concurrencies in Reversible Concurrent Calculi. Reversible Computation[M].DE: Springer;LNCS, 2022