可逆计算的公理化理论
摘要：并发系统的计算撤销在许多情况下是有益的，例如在多线程程序的可逆调试和由并行离散事件仿真中的乐观执行错误恢复中。已经提出了许多方法来逆转并发计算的形式模型，包括诸如CCS这样的进程演算、像Erlang这样的语言、以及主要事件结构和发生网络。然而，仍未解决可逆系统应该具有什么属性，以及已经提出的各种属性（如抛物线引理和因果一致性属性）之间的关系。通过使用具有捕获转换是否独立关系的泛型带标记的转换系统，我们为这些问题提供了一个解决方案，以探索这些属性之间的含义。特别地，我们展示了它们如何从一组公理中推导出来。我们的意图是在建立某种形式模型的属性时，验证公理比直接证明抛物线引理等属性更容易。我们还引入了与因果一致的可逆性相关的两个新概念，即因果活性和因果安全性，分别说明了只有当一个动作与其后续的所有动作都是独立的时才能撤销。我们证明了因果活性和因果安全性都可以从我们的公理中推导出来。
作者：Ivan Lanese (Focus Team, University of Bologna/INRIA, Italy), Iain Phillips (Imperial College London, England) and Irek Ulidowski (University of Leicester, England and AGH University of Science and Technology, Krakow, Poland)
论文ID：2307.13360
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-07-26