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.

翻译：可逆调试器通过从观察到异常行为的位置向后执行程序，并查找导致该行为的错误，从而帮助程序员更快地发现并发程序中的异常原因。可逆调试器可以建立在经过充分研究的因果一致性可逆理论之上，该理论仅允许撤销一个动作，前提是该动作的后果（如果有的话）已事先撤销。因果一致性可逆通过减少向后查找时需要探索的状态数量，实现了更高效的调试。迄今为止，因果一致性可逆从未考虑过时间这一现实应用中的关键因素。本文通过进程代数研究并发系统中可逆性（reversibility）与时间之间的相互作用。Hennessy和Regan提出的时间进程语言（TPL）是CCS的扩展，包含离散时间和超时操作符，其理论基础已十分完善。我们定义了TPL的可逆扩展——revTPL，并证明了它满足因果一致性可逆演算所期望的性质。此外，我们还展示了revTPL可以等价地解释为带时间的可逆CCS的扩展。