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.
Model Checking Reversible Systems: Forwardly
Dal Pio Luogo F.
Membro del Collaboration Group
;Pinna G. M.
Membro del 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.
File in questo prodotto:
Non ci sono file associati a questo prodotto.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
