Efficient Construction of Reachability Graphs for Petri Net Product Lines

TL;DR

This paper introduces algorithms for efficiently constructing reachability graphs for Petri Net Product Lines, combining symbolic encoding, feature constraints, and reduction techniques to handle concurrency and variability.

Contribution

It presents a novel symbolic, family-preserving approach with reduction techniques that improve scalability for reachability analysis in Petri Net Product Lines.

Findings

Significant memory and time savings over naive methods.

The approach is sound and complete for standard semantics.

Enables practical analysis of large product-line models.

Abstract

This paper presents a set of algorithms for computing the reachability graph of Petri Net Product Lines (PNPLs). These algorithms address the combined challenges of concurrency and variability that arise from product-line configurations. The proposed approach integrates symbolic state representations with family-based variability handling to generate a compact, parameterised reachability graph that captures behaviour across all products without exhaustive product enumeration. The main contributions are threefold. First, we introduce a symbolic state encoding adapted to PNPL semantics. Second, we define a family-preserving successor generation procedure that applies feature constraints during exploration. Third, we propose reduction techniques to mitigate state-space explosion, including on-the-fly merging of equivalent symbolic states and selective abstraction of irrelevant state details. We prove soundness and completeness of the construction with respect to standard per-product semantics and analyse computational complexity. An implementation integrated into our modelling tool demonstrates substantial savings in memory and time compared with naive product-based exploration, while preserving diagnostic and verification capabilities. The results indicate that the method enables practical reachability analysis for realistically sized product-line models, thereby facilitating verification and design-space exploration in configurable concurrent systems.