Model Checking Reversible Systems: Forwardly

Dal Pio Luogo F.

Member of the Collaboration Group

;Mezzina C. A.

Member of the Collaboration Group

;Pinna G. M.

Member of the Collaboration Group

2024-01-01

---

Abstract

Reversibility is nowadays playing a major role when dealing with systems, allowing to revert to safe states of systems evolutions. For instance reversibility can be applied to causal-consistent debugging. On the other hand, Linear Temporal Logic (LTL) has been used to formalize properties that a system may fulfil, and it may be equipped with past operators. This makes this logic appealing to express and prove properties of a reversible system. In this paper we investigate this feature, and we use the classical approaches to model check LTL formulas on unfoldings, in order to deal with reversible systems.