revTPL: The Reversible Temporal Process Language - INRIA 2
Article Dans Une Revue Logical Methods in Computer Science Année : 2024

revTPL: The Reversible Temporal Process Language

Résumé

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.
Fichier principal
Vignette du fichier
2212.03687.pdf (531.45 Ko) Télécharger le fichier
Origine Fichiers éditeurs autorisés sur une archive ouverte
licence

Dates et versions

hal-04576057 , version 1 (15-05-2024)

Licence

Identifiants

Citer

Laura Bocchi, Ivan Lanese, Claudio Antares Mezzina, Shoji Yuen. revTPL: The Reversible Temporal Process Language. Logical Methods in Computer Science, 2024, Volume 20, Issue 1, ⟨10.46298/lmcs-20(1:11)2024⟩. ⟨hal-04576057⟩
28 Consultations
15 Téléchargements

Altmetric

Partager

More