arxiv: 2604.05657 · v1 · submitted 2026-04-07 · 💻 cs.FL

Recognition: 2 theorem links

· Lean Theorem

Efficient Construction of Reachability Graphs for Petri Net Product Lines

Elena G\'omez-Mart\'inez, Jos\'e Ignacio Requeno Jarabo

Authors on Pith no claims yet

Pith reviewed 2026-05-10 18:57 UTC · model grok-4.3

classification 💻 cs.FL

keywords Petri net product linesreachability graphssymbolic statesfamily-based analysisvariabilitystate space reductionconcurrent systemsverification

0 comments

The pith

Symbolic state representations with family-based rules produce a compact parameterized reachability graph for all products in a Petri net product line.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper presents algorithms that combine symbolic state encoding with variability handling to explore reachability in Petri net product lines. This creates one graph that represents the possible behaviors for every valid product configuration at once. The approach applies feature constraints when generating successors and merges equivalent states during construction to control the size of the graph. Reductions like selective abstraction further help avoid state-space explosion. The result is proven to match the reachability information obtained from analyzing each product on its own, with reported gains in efficiency for practical models.

Core claim

The core discovery is that a symbolic state encoding adapted to PNPL semantics, together with a family-preserving successor generation procedure that applies feature constraints during exploration, and reduction techniques including on-the-fly merging and selective abstraction, allow construction of a compact parameterized reachability graph. This graph captures the behavior across all products without requiring exhaustive product enumeration. The construction is shown to be sound and complete with respect to standard per-product reachability semantics.

What carries the argument

Parameterized reachability graph built from symbolic states that encode multiple product configurations and transitions constrained by feature requirements.

If this is right

The graph supports verification tasks for the entire product line in one pass.
Memory and time requirements drop substantially compared to per-product construction for models with many variants.
Diagnostic capabilities such as identifying reachable states remain available for any specific product.
The method facilitates design-space exploration in systems with both concurrency and configurability.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The same symbolic approach could be applied to other concurrent models that include feature variability beyond Petri nets.
Properties expressed over feature constraints could be checked directly on the parameterized graph without generating separate instances.
Further reductions might come from integrating more advanced abstraction techniques specific to variability.

Load-bearing premise

That the symbolic state encoding and the family-preserving successor rules preserve the exact reachability semantics for every valid product without spurious or missing states.

What would settle it

Finding a small Petri net product line where the states reachable in the parameterized graph differ from those in the individual reachability graphs of its products.

Figures

Figures reproduced from arXiv: 2604.05657 by Elena G\'omez-Mart\'inez, Jos\'e Ignacio Requeno Jarabo.

**Figure 1.** Figure 1: A PNPL representing a Simplistic Flexible Assembly Line. Structural properties — such as marked graphs, state machines, free-choice, and extended free-choice structures — are formally analysed using lifted analysis techniques [27]. These techniques translate structural properties into first-order logical propositions that can be efficiently resolved through satisfiability (SAT) solvers [13]. Furthermore, b… view at source ↗

**Figure 2.** Figure 2: Feature-annotated reachability graph for PNPL representing a Simplistic Flexible Assembly Line [PITH_FULL_IMAGE:figures/full_fig_p010_2.png] view at source ↗

**Figure 3.** Figure 3: Architecture overview of Titan. time in Coloured Petri Nets [14, 15], i.e., tokens carry discrete time annotations and time evolves according to a central clock. Titan can perform runtime analysis of individual TPNPL products and compute user-specified quality metrics (e.g., performance, safety indicators) from execution events obtained by simulation traces. It relies on the TPNPL-to-CPN Tools transforma… view at source ↗

**Figure 4.** Figure 4: PNPL modelling of [PITH_FULL_IMAGE:figures/full_fig_p012_4.png] view at source ↗

read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

This paper gives a workable symbolic algorithm for reachability graphs over Petri net product lines that keeps variability constraints during exploration instead of enumerating products.

read the letter

The main point is a compact reachability graph construction for Petri net product lines that uses symbolic states to cover all valid configurations at once. They encode states with feature constraints, generate successors while preserving the product family, and merge equivalent states on the fly along with selective abstraction to control explosion. An implementation in their tool shows clear time and memory savings over naive per-product checks, and the graph is still meant to support diagnostics and verification. They state proofs of soundness and completeness plus a complexity analysis. If those proofs hold, the core claim is fine; nothing in the stated approach looks internally inconsistent or circular. The reductions are the part that needs the most care, since merging and abstraction could in principle drop or add behaviors, but the paper treats them as semantics-preserving. This is a targeted algorithmic paper for people who verify configurable concurrent systems or extend Petri net tools to product lines. A reader already working in formal methods for software product lines would get immediate use from the successor rules and the reported performance numbers. It is not a foundational theoretical result, but the claims are concrete enough to check. I would send it to peer review. The work is focused, the evaluation is present, and the subfield can use practical methods like this.

Referee Report

0 major / 3 minor

Summary. The paper presents algorithms for computing the reachability graph of Petri Net Product Lines (PNPLs) by integrating symbolic state representations with family-based variability handling. This produces a compact, parameterized reachability graph capturing behavior across all valid products without exhaustive enumeration. The main contributions include a symbolic state encoding for PNPL semantics, a family-preserving successor generation procedure that incorporates feature constraints, reduction techniques such as on-the-fly merging of equivalent symbolic states and selective abstraction, proofs of soundness and completeness with respect to standard per-product reachability semantics, and a complexity analysis. An implementation in a modeling tool is reported to yield substantial memory and time savings compared to naive product enumeration while preserving diagnostic and verification capabilities.

Significance. If the soundness and completeness proofs hold and the reductions preserve exact semantics, the work would be significant for enabling practical verification and design-space exploration in configurable concurrent systems, where both concurrency and variability induce severe state-space explosion. Strengths include the explicit proofs, complexity analysis, and empirical demonstration via tool integration; these elements support reproducibility and practical adoption beyond theoretical claims.

minor comments (3)

Abstract: the claim of 'substantial savings' is not quantified with specific metrics, percentages, or model sizes from the experiments; adding these would strengthen the presentation of results.
The family-preserving successor rules and merging criteria should include a small illustrative example (e.g., a 2-feature PNPL) to clarify how feature constraints are applied during exploration without introducing spurious states.
Ensure that the complexity analysis explicitly bounds the size of the parameterized graph in terms of the number of features and the underlying Petri net size, rather than leaving it at a high-level statement.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive and accurate summary of the paper, for acknowledging the significance of the approach for verification of configurable concurrent systems, and for recommending minor revision. No specific major comments were raised in the report.

Circularity Check

0 steps flagged

No significant circularity

full rationale

The paper describes algorithmic constructions (symbolic state encoding, family-preserving successor generation, merging and abstraction reductions) together with claimed proofs of soundness and completeness relative to standard per-product reachability semantics. No equations, definitions, or derivations reduce the output reachability graph or its properties to fitted parameters, self-referential inputs, or load-bearing self-citations. The central claims rest on independent semantic-preservation arguments rather than circular reductions, consistent with an external algorithmic and proof-based approach.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The central claim rests on standard Petri-net semantics and the assumption that symbolic merging preserves per-product reachability; no free parameters or new entities are introduced in the abstract.

axioms (1)

standard math Standard Petri net reachability semantics hold for individual products
Invoked as the base semantics that the family-based construction must match.

pith-pipeline@v0.9.0 · 5494 in / 1118 out tokens · 32938 ms · 2026-05-10T18:57:28.011351+00:00 · methodology

discussion (0)

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

IndisputableMonolith/Foundation/AbsoluteFloorClosure.lean reality_from_one_distinction unclear
We introduce a symbolic state encoding adapted to PNPL semantics... family-preserving successor generation procedure that applies feature constraints during exploration... conflict detection filter... SAT(Φ_cand ∧ C)
IndisputableMonolith/Foundation/ArithmeticFromLogic.lean LogicNat recovery theorems unclear
We prove soundness and completeness of the construction with respect to standard per-product semantics

Reference graph

Works this paper leans on

32 extracted references · 13 canonical work pages

[1]

In: Proc

Amparore, E.G.: Reengineering the Editor of the GreatSPN Framework. In: Proc. PNSE@Petri Nets. CEUR Workshop Proceedings, vol. 1372, pp. 153–170. CEUR- WS.org (2015)

2015
[2]

Springer (2013)

Apel, S., Batory, D.S., Kästner, C., Saake, G.: Feature-Oriented Soft- ware Product Lines - Concepts and Implementation. Springer (2013). https://doi.org/10.1007/978-3-642-37521-7, https://doi.org/10.1007/978-3- 642-37521-7

work page doi:10.1007/978-3-642-37521-7 2013
[3]

In: Handbook of Constraint Programming, Foundations of Artificial Intelligence, vol

Brown, K.N., Miguel, I.: Chapter 21 - uncertainty and change. In: Handbook of Constraint Programming, Foundations of Artificial Intelligence, vol. 2, pp. 731 –
[4]

Ceresa, M., Gorostiaga, F., Sánchez, C.: Declarative stream runtime verification (hlola). In: d. S. Oliveira, B.C. (ed.) Procs of Programming Languages and Systems - 18th Asian Symposium, APLAS 2020. Lecture Notes in Computer Science, vol. 12470, pp. 25–43. Springer (2020). https://doi.org/10.1007/978-3-030-64437-6\_2

work page doi:10.1007/978-3-030-64437-6 2020
[5]

Addison-Wesley Longman Publishing Co., Inc., Boston, MA, USA (2002)

Clements, P., Northrop, L.: Software Product Lines: Practices and Patterns. Addison-Wesley Longman Publishing Co., Inc., Boston, MA, USA (2002)

2002
[6]

In: Massoni, T., Mousavi, M.R

Convent, L., Hungerecker, S., Leucker, M., Scheffel, T., Schmitz, M., Thoma, D.: TeSSLa: Temporal stream-based specification language. In: Massoni, T., Mousavi, M.R. (eds.) Formal Methods: Foundations and Applications - 21st Brazil- ian Symposium, SBMF 2018. LNCS, vol. 11254, pp. 144–162. Springer (2018). https://doi.org/10.1007/978-3-030-03044-5\_10

work page doi:10.1007/978-3-030-03044-5 2018
[7]

In: Reisig, W., Rozenberg, G

Desel, J.: Basic linear algebraic techniques for place or transition nets. In: Reisig, W., Rozenberg, G. (eds.) Lectures on Petri Nets I: Basic Models, Ad- vances in Petri Nets, the volumes are based on the Advanced Course on Petri Nets, held in Dagstuhl, September 1996. Lecture Notes in Computer Science, vol. 1491, pp. 257–308. Springer (1996). https://d...

work page doi:10.1007/3-540-65306- 1996
[8]

In: Limonad, L., Weber, B

Freytag, T., Sänger, M.: WoPeD - An Educational Tool for Workflow Nets. In: Limonad, L., Weber, B. (eds.) Procs. of the BPM Demo Sessions 2014 Co- located with the 12th International Conference on Business Process Management (BPM 2014), Eindhoven, The Netherlands, September 10, 2014. CEUR Work- shop Proceedings, vol. 1295, p. 31. CEUR-WS.org (2014), https...

2014
[9]

Springer Science & Business Media (2013)

Girault, C., Valk, R.: Petri nets for systems engineering: a guide to modeling, verification, and applications. Springer Science & Business Media (2013)

2013
[10]

In: The 34th Intl

Gómez-Martínez, E., Guerra, E., de Lara, J.: Analysing Product Lines of Con- current Systems with Coloured Petri Nets. In: The 34th Intl. Conf. on Software Engineering and Knowledge Engineering, SEKE 2022. pp. 118–123. KSI Research Inc. (2022). https://doi.org/10.18293/SEKE2022-015

work page doi:10.18293/seke2022-015 2022
[11]

Gómez-Martínez, E., Guerra, E., de Lara, J., Garmendia, A.: Lifted structural invariant analysis of Petri net product lines. J. Log. Algebraic Methods Program. 130, 100824 (2023). https://doi.org/10.1016/J.JLAMP.2022.100824 Efficient Construction of Reachability Graphs for Petri Net Product Lines 15

work page doi:10.1016/j.jlamp.2022.100824 2023
[12]

In: PNSE@Petri Nets/ACSD

Gómez-Martínez, E., de Lara, J., Guerra, E.: Towards Extensible Structural Anal- ysis of Petri Net Product Lines. In: PNSE@Petri Nets/ACSD. CEUR Workshop Proceedings, vol. 2424, pp. 37–46. CEUR-WS.org (2019)

2019
[13]

Gómez-Martínez, E., de Lara, J., Guerra, E.: Extensible Structural Analysis of Petri Net Product Lines. Trans. Petri Nets Other Model. Concurr.15, 27–49 (2021). https://doi.org/10.1007/978-3-662-63079-2\_2

work page doi:10.1007/978-3-662-63079-2 2021
[14]

In: International conference on application and theory of Petri nets

Jensen, K.: Coloured Petri nets: A high level language for system design and anal- ysis. In: International conference on application and theory of Petri nets. pp. 342–
[15]

Jensen, K., Kristensen, L.M., Wells, L.: Coloured Petri Nets and CPN Tools for Modelling and Validation of Concurrent Systems. Int. J. Softw. Tools Technol. Transf.9(3–4), 213–254 (2007), see also https://cpntools.org/

2007
[16]

In: Dang, T., Stolz, V

Kallwies, H., Leucker, M., Schmitz, M., Schulz, A., Thoma, D., Weiss, A.: TeSSLa - An Ecosystem for Runtime Verification. In: Dang, T., Stolz, V. (eds.) Run- time Verification (RV 2022). LNCS, vol. 13498, pp. 314–324. Springer (2022). https://doi.org/10.1007/978-3-031-17196-3\_20

work page doi:10.1007/978-3-031-17196-3 2022
[17]

Khomenko, V.: Model checking based on prefixes of Petri net unfoldings. Ph.D. thesis, Newcastle University (2003)

2003
[18]

In: CP Solvers: Modeling, Applications, Integration, and Standardization (2013)

Kuchcinski, K., Szymanek, R.: JaCoP - Java Constraint Programming solver. In: CP Solvers: Modeling, Applications, Integration, and Standardization (2013)

2013
[19]

Applied Sciences 9(16) (2019)

Lu, Z., Liu, J., Dong, L., Liang, X.: Maintenance process simulation based main- tainability evaluation by using stochastic colored petri net. Applied Sciences 9(16) (2019). https://doi.org/10.3390/app9163262, https://www.mdpi.com/2076- 3417/9/16/3262

work page doi:10.3390/app9163262 2019
[20]

Springer (2017)

Meinicke, J., Thüm, T., Schröter, R., Benduhn, F., Leich, T., Saake, G.: Mastering software variability with FeatureIDE. Springer (2017)

2017
[21]

Murata, T.: Petri Nets: Properties, Analysis and Applications. Proc. IEEE77(4), 541–580 (1989)

1989
[22]

In: Botterweck, G., Jarzabek, S., Kishi, T., Lee, J., Livengood, S

Muschevici, R., Clarke, D., Proença, J.: Feature petri nets. In: Botterweck, G., Jarzabek, S., Kishi, T., Lee, J., Livengood, S. (eds.) Software Product Lines - 14th International Conference, SPLC 2010, Jeju Island, South Korea, September 13-17,

2010
[23]

Workshop Proceedings (Volume 2 : Workshops, Industrial Track, Doctoral Symposium, Demonstrations and Tools). pp. 99–106. Lancaster University (2010), http://splc2010.postech.ac.kr/SPLC2010_second_volume.pdf

2010
[24]

Muschevici, R., Proença, J., Clarke, D.: Feature nets: behavioural mod- elling of software product lines. Softw. Syst. Model.15(4), 1181–1206 (2016). https://doi.org/10.1007/S10270-015-0475-Z, https://doi.org/10.1007/s10270-015- 0475-z

work page doi:10.1007/s10270-015-0475-z 2016
[25]

Petri, C.A.: Kommunikation mit Automaten. Ph.D. thesis, Universität Hamburg, Germany (1962)

1962
[26]

Foundations, Principles and Techniques

Pohl, K., Böckle, G., van der Linden, F.J.: Software Product Line Engineering. Foundations, Principles and Techniques. Springer (2005). https://doi.org/10.1007/3-540-28901-1

work page doi:10.1007/3-540-28901-1 2005
[27]

In: Köhler-Bussmeier, M., Moldt, D., Rölke, H

Requeno, J.I., Gómez-Martínez, E., Kallwies, H., Haustein, M., Leucker, M., Stolz, V., Stünkel, P.: Runtime verification of timed petri nets. In: Köhler-Bussmeier, M., Moldt, D., Rölke, H. (eds.) Procs. of the Int. Workshop on Petri Nets and Software Engineering 2024 co-located with the 45th Int. Conf. on Application and The- ory of Petri Nets and Concurr...

2024
[28]

Gousios, M

Salay, R., Famelis, M., Rubin, J., Sandro, A.D., Chechik, M.: Lifting model trans- formations to product lines. In: Jalote, P., Briand, L.C., van der Hoek, A. (eds.) 36th Int. Conf. on Software Engineering, ICSE ’14. pp. 117–128. ACM (2014). https://doi.org/10.1145/2568225.2568267

work page doi:10.1145/2568225.2568267 2014
[29]

Sirius: https://www.eclipse.org/sirius/
[30]

Addison-Wesley Professional, 2nd edn

Steinberg, D., Budinsky, F., Paternostro, M., Merks, E.: EMF: Eclipse Modeling Framework 2.0. Addison-Wesley Professional, 2nd edn. (2009) 30.Titan- Tool for PetrI net producT line ANalysis: https://doi.org/10.5281/zenodo.13993436

work page doi:10.5281/zenodo.13993436 2009
[31]

In: QEST

Zimmermann, A.: Modelling and performance evaluation with TimeNET 4.4. In: QEST. LNCS, vol. 10503, pp. 300–303. Springer (2017)

2017
[32]

IEEE Transactions on industrial electronics41(6), 567–583 (1994)

Zurawski, R., Zhou, M.: Petri nets and industrial applications: A tutorial. IEEE Transactions on industrial electronics41(6), 567–583 (1994)

1994