一句话：提出可逆时序进程演算 revTPL，将因果一致可逆性与离散时间/超时机制结合，并证明其满足因果一致可逆性质。
可逆调试器依赖因果一致可逆性提高并发程序调试效率，但现有理论未考虑时间。本文在 Hennessy 与 Regan 的时序进程语言 TPL（CCS 的离散时间与超时扩展）基础上，定义可逆时序进程语言 revTPL，以进程代数研究可逆性与时间的交互。作者证明 revTPL 满足因果一致可逆演算的预期性质，并说明它也可视为带时间的可逆 CCS 扩展。该工作为并发系统的时间感知可逆调试与语义分析提供形式化基础。
Reversible debuggers help programmers to find the causes of misbehaviours in concurrent programs more quickly, by executing a program backwards from the point where a misbehaviour was observed, and looking for the bug(s) that caused it. Reversible debuggers can be founded on the well-studied theory of causal-consistent reversibility, which only allows one to undo an action provided that its consequences, if any, are undone beforehand. Causal-consistent reversibility yields more efficient debugging by reducing the number of states to be explored when looking backwards. Till now, causal-consistent reversibility has never considered time, which is a key aspect in real-world applications. Here, we study the interplay between reversibility and time in concurrent systems via a process algebra. The Temporal Process Language (TPL) by Hennessy and Regan is a well-understood extension of CCS with discrete-time and a timeout operator. We define revTPL, a reversible extension of TPL, and we show that it satisfies the properties expected from a causal-consistent reversible calculus. We show that, alternatively, revTPL can be interpreted as an extension of reversible CCS with time.
@article{paperbot2780,
title = {revTPL: The Reversible Temporal Process Language},
author = {Laura Bocchi and Ivan Lanese and Claudio Antares Mezzina and Shoji Yuen},
journal = {Logical Methods in Computer Science},
volume = {Volume 20, Issue 1},
year = {2024},
doi = {10.46298/lmcs-20(1:11)2024}
}