Reversible Computation in Truly Concurrent Models of Distributed Systems (ciclo LiMoSP)

Reversible computation is an unconventional form of computing that extends the standard forward-only mode of computation with the ability to execute a sequence of operations in reverse at any point during computation. It has recently been attracting increasing attention in various research communities, as it promises low-power computation and is inherent or relevant in a variety of applications, from biochemical reactions to fault-tolerant distributed processes. This talk presents Reversing Petri Nets (RPNs), a formal framework for modelling and reasoning about reversible behavior in distributed systems. RPNs extend classical Petri nets with persistent tokens, which can either be distinguished individually or treated collectively, allowing flexible representation of multiple entities or resources. The framework captures different types of reversibility, including backtracking, causal reversing, and out-of-causal-order reversing, and also supports controlled reversibility, where the system can dynamically decide whether transitions proceed forward or backward based on specified conditions. The talk will consider the expressiveness relation between the various models and explain how these concepts can be applied to model the behavior of practical applications, such as biochemical pathways and distributed algorithms, in a structured, visual, and intuitive way.