Model Checking Reversible Systems: Forwardly

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.