在可逆并发演算中启用复制和上下文
Enabling Replications and Contexts in Reversible Concurrent Calculus
摘要：
现有的形式主义的代数规范和表示网络的可逆代理遭受一些缺点。尽管多次尝试，通信系统演算（CCS）的可逆变格并没有提供令人满意的适应的概念，通常在“向前”的过程代数，如复制或上下文。它们似乎也未能利用源于可逆性的可能的新功能，例如基于它们如何复制允许反向计算的内存机制来区分多个复制的能力。现有的形式主义不允许在也有过去的上下文中执行过程的“热插拔”。最后，它们假设存在“永远新鲜”的键或标识符，如果实现得不好，可能会导致不必要的瓶颈和涉及所有线程的查找。在本文中，我们开始调查这些问题，首先设计了一个进程代数赋予的机制来生成标识符，而不需要咨询其他线程。我们使用这种演算来重铸CCS中的非确定性的可能表示，并作为副产品建立一个简单而直接的并发定义。我们的可逆演算，然后证明满足预期的属性，并允许精确地布局不同的表示复制的过程与内存。我们还观察到，迄今为止定义的可逆互模拟都不是我们的“可逆”上下文概念下的同余。
英文摘要：
Existing formalisms for the algebraic specification and representation of networks of reversible agents suffer some shortcomings. Despite multiple attempts, reversible declensions of the Calculus of Communicating Systems (CCS) do not offer satisfactory adaptation of notions that are usual in ''forward-only'' process algebras, such as replication or context. They also seem to fail to leverage possible new features stemming from reversibility, such as the capacity of distinguishing between multiple replications, based on how they replicate the memory mechanism allowing to reverse the computation. Existing formalisms disallow the ''hot-plugging'' of processes during their execution in contexts that also have a past. Finally, they assume the existence of ''eternally fresh'' keys or identifiers that, if implemented poorly, could result in unnecessary bottlenecks and look-ups involving all the threads. In this paper, we begin investigating those issues, by first designing a process algebra endowed with a mechanism to generate identifiers without the need to consult with the other threads. We use this calculus to recast the possible representations of non-determinism in CCS, and as a by-product establish a simple and straightforward definition of concurrency. Our reversible calculus is then proven to satisfy expected properties, and allows to lay out precisely different representations of the replication of a process with a memory. We also observe that none of the reversible bisimulations defined thus far are congruences under our notion of ''reversible'' contexts.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
