Static versus dynamic reversibility in CCS
Static versus dynamic reversibility in CCS
复制标题
DOI：
10.1007/s00236-019-00346-6
复制
发表时间：
2019-11-07
期刊：
影响因子：
0.6
通讯作者：
Mezzina, Claudio Antares
中科院分区：
文献类型：
--
作者：
Lanese, Ivan;MediC, Doriana;Mezzina, Claudio Antares
可逆计算的概念正吸引着人们的兴趣，因为它在不同领域的应用，特别是容错系统的编程抽象的研究。大多数计算模型不是自然可逆的，因为计算会导致信息丢失，并且必须存储历史信息才能实现可逆性。在文献中，存在两种逆转CCS过程演算的方法，它们在如何保存历史信息上存在差异。由Danos和Krivine提出的可逆CCS（RCCS）利用连接到每个线程的专用内存堆栈。由菲利普斯和Ulidowski提出的带密钥的CCS（CCSK）使CCS算子是静态的，从而计算不会导致信息丢失。本文证明了RCCS和CCSK在LTS同构方面是等价的。
The notion of reversible computing is attracting interest because of its applications in diverse fields, in particular the study of programming abstractions for fault tolerant systems. Most computational models are not naturally reversible since computation causes loss of information, and history information must be stored to enable reversibility. In the literature, two approaches to reverse the CCS process calculus exist, differing on how history information is kept. Reversible CCS (RCCS), proposed by Danos and Krivine, exploits dedicated stacks of memories attached to each thread. CCS with Keys (CCSK), proposed by Phillips and Ulidowski, makes CCS operators static so that computation does not cause information loss. In this paper we show that RCCS and CCSK are equivalent in terms of LTS isomorphism.