Reversibility-Aware Step Graphs for State Space Reduction and Reversibility Checking in Concurrent Systems

Reversibility is a critical property of concurrent systems, reflecting their ability to return to the initial state without external intervention. Petri nets (PN) are widely used to model such systems, as they effectively capture complex interleavings and asynchronous behaviors. Traditional approaches to reversibility checking typically rely on constructing the reachability graph (RG) of a PN, which often encounters state-space explosion. Although partial order methods have been proposed to mitigate this issue by eliminating redundant interleavings, few are tailored to reversibility analysis. In this work, we propose a novel approach based on the notion of sound steps and introduce a definition called reversibility-aware score. Each transition is annotated with a reversibility-aware score indicating the likelihood of returning to the initial marking after its firing. At a given marking, transitions with the highest scores in a maximal sound step are grouped and fired simultaneously, resulting in a new marking. This procedure is conducted iteratively until no new markings are generated, producing a reversibility-aware step graph (RASG). We formally prove that RASG preserves the presence of deadlocks and enables efficient reversibility checking.