revTPL: The Reversible Temporal Process Language

TL;DR

This paper addresses the challenge of integrating time with causal-consistent reversibility in concurrent systems by introducing revTPL, a reversible extension of the Temporal Process Language ($\mathrm{TPL}$). It develops a static, key-based reversible semantics with forward and backward LTSs, along with histories and time-passage tracking using $\sigma_{\bot}$ prefixes, and proves that revTPL satisfies causal-consistency via SP, BTI, and WF, including a Parabolic Lemma. The authors establish precise embeddings to $\mathrm{TPL}$ and to CCSK, via history- and time-forgetting maps, and show that revTPL can be viewed as an extension of reversible CCS with time. They discuss the implications for real-time debugging and future work, such as rollback constructs and asynchronous communications, highlighting potential applications to timed Erlang debugging and real-time system analysis. Overall, revTPL provides a rigorous foundation for reversible timed concurrency and opens avenues for practical timed reversible debugging and analysis.

Abstract

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.

Figures (12)

• Figure 1: Syntax of $\mathtt{revTPL}$
• Figure 2: $\mathtt{revTPL}$ forward LTS
• Figure 3: $\mathtt{revTPL}$ backward LTS
• Figure 4: Forgetting maps.
• Figure 5: Syntax of CCS

Theorems & Definitions (47)

• Example 1: Motivating example
• Definition 2.1: Standard configuration
• Definition 2.2: Not-acted configuration
• Definition 2.3: Semantics
• Example 2.4
• Definition 2.5: Reachable configurations
• Definition 3.1: History forgetting map
• Proposition 3.2: Embedding of TPL
• proof
• Definition 3.3: Timed bisimulation