On Reversibility in Petri Nets
摘要
Reversible semantics for Petri nets have received increasing attention, yet a fully satisfactory account for general nets is still missing. Existing approaches apply either to restricted subclasses, such as occurrence nets, or to general nets studied via unfoldings, which often produce infinite models even for finite nets. Other approaches adopt a weaker notion of reversibility, based solely on the ability to restore an initial marking, without undoing individual computation steps. In this paper, we propose a reversible semantics for general Petri nets that supports stepwise reversal and enforces causal consistency. Our approach combines explicit identifiers to track executed transitions with an enriched token model. This combination ensures that only executed transitions can be reversed and that reversibility respects causal dependencies.