Laura Bocchi ; Ivan Lanese ; Claudio Antares Mezzina ; Shoji Yuen - revTPL: The Reversible Temporal Process Language

lmcs:10440 - Logical Methods in Computer Science, January 31, 2024, Volume 20, Issue 1 - https://doi.org/10.46298/lmcs-20(1:11)2024
revTPL: The Reversible Temporal Process LanguageArticle

Authors: Laura Bocchi ; Ivan Lanese ; Claudio Antares Mezzina ; Shoji Yuen

    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.


    Volume: Volume 20, Issue 1
    Published on: January 31, 2024
    Accepted on: December 26, 2023
    Submitted on: December 8, 2022
    Keywords: Computer Science - Programming Languages,Computer Science - Logic in Computer Science
    Funding:
      Source : OpenAIRE Graph
    • Session Types for Reliable Distributed Systems (STARDUST); Funder: UK Research and Innovation; Code: EP/T014512/1
    • Behavioural Application Program Interfaces; Funder: European Commission; Code: 778233
    • Causal debugging for concurrent systems; Funder: French National Research Agency (ANR); Code: ANR-18-CE25-0007

    Consultation statistics

    This page has been seen 888 times.
    This article's PDF has been downloaded 464 times.