Goal-Driven Unfolding of Petri Nets

TL;DR

This paper introduces a goal-driven unfolding algorithm for 1-safe Petri nets that efficiently computes minimal configurations reaching a specific target marking by combining unfolding techniques with static analysis for model reduction.

Contribution

It presents a novel algorithm that integrates unfolding with on-the-fly static analysis to focus on goal reachability in Petri nets, reducing unnecessary exploration.

Findings

Algorithm effectively computes minimal configurations for goal reachability.

Combines unfolding with static analysis for efficient state-space exploration.

Experimental results demonstrate improved performance in reachability analysis.

Abstract

Unfoldings provide an efficient way to avoid the state-space explosion due to interleavings of concurrent transitions when exploring the runs of a Petri net. The theory of adequate orders allows one to define finite prefixes of unfoldings which contain all the reachable markings. In this paper we are interested in reachability of a single given marking, called the goal. We propose an algorithm for computing a finite prefix of the unfolding of a 1-safe Petri net that preserves all minimal configurations reaching this goal. Our algorithm combines the unfolding technique with on-the-fly model reduction by static analysis aiming at avoiding the exploration of branches which are not needed for reaching the goal. We present some experimental results.