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.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

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

  • Hao Dou,
  • Mengchu Zhou,
  • Shouguang Wang,
  • Dan You,
  • Wenli Duo

摘要

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.