pith. sign in

arxiv: 2602.15739 · v3 · submitted 2026-02-17 · 💻 cs.DB

Hierarchical Decomposition of Separable Workflow-Nets

Humam Kourani , Gyunam Park , Wil M.P. van der Aalst This is my paper

Pith reviewed 2026-05-15 21:40 UTC · model grok-4.3

classification 💻 cs.DB
keywords workflow netsPOWL 2.0model transformationhierarchical decompositionseparable netschoice graphsprocess modeling
0
0 comments X

The pith

A recursive algorithm decomposes separable workflow nets into POWL 2.0 models while preserving their language.

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

The paper presents an algorithm that recursively identifies patterns in safe and sound workflow nets and converts them to POWL 2.0 using choice graphs for decisions and cycles. This establishes that the resulting POWL model has exactly the same set of possible executions as the original net. A sympathetic reader would care because it allows process models from established notations to benefit from POWL's quality guarantees and expressiveness for analysis and improvement. The algorithm unifies handling of choices and loops in one strategy, unlike previous separate detections.

Core claim

The novel algorithm recursively identifies structural patterns within the WF-net and translates them into their POWL representation using choice graphs to capture generalized decision and cyclic patterns. We formally prove that the generated POWL model preserves the language of the input WF-net and that the algorithm is complete on the class of separable WF-nets.

What carries the argument

Recursive pattern identification that maps WF-net structures to POWL operators and choice graphs for non-block decisions and cycles.

If this is right

  • The POWL model is behaviorally equivalent to the input WF-net.
  • The method is complete for all separable WF-nets constructed from state machines and marked graphs.
  • The algorithm scales well to large-scale process models.
  • It successfully transforms all 1,493 models in an industrial and synthetic benchmark.

Where Pith is reading between the lines

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

  • POWL 2.0 may be expressive enough for most real-world business processes.
  • This transformation could facilitate adoption of POWL in practical process mining and management tools.
  • Extensions might apply the decomposition to non-separable nets by relaxing the separability assumption.

Load-bearing premise

The input workflow nets are safe and sound and belong to the separable class that can be built by hierarchical nesting of state machines and marked graphs.

What would settle it

Finding a safe and sound separable WF-net for which the algorithm produces a POWL model with a different set of traces than the original net.

Figures

Figures reproduced from arXiv: 2602.15739 by Gyunam Park, Humam Kourani, Wil M.P. van der Aalst.

Figure 1
Figure 1. Figure 1: Example models for a retailer’s order fulfillment process. [PITH_FULL_IMAGE:figures/full_fig_p003_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: A free-choice WF-net that is not separable. [PITH_FULL_IMAGE:figures/full_fig_p012_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Reduction rules illustrated with examples. [PITH_FULL_IMAGE:figures/full_fig_p014_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: An example illustrating a conflict-hiding partition [PITH_FULL_IMAGE:figures/full_fig_p015_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: An example illustrating a concurrency-hiding partition and the choice graph projection of [PITH_FULL_IMAGE:figures/full_fig_p018_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: Impact of preprocessing on conversion success. [PITH_FULL_IMAGE:figures/full_fig_p024_6.png] view at source ↗
Figure 7
Figure 7. Figure 7: Examples where the decomposition attempts in Algorithm 3 fail. [PITH_FULL_IMAGE:figures/full_fig_p025_7.png] view at source ↗
Figure 8
Figure 8. Figure 8: Comparison of conversion times between Algorithm 3, our previous approach from [10], [PITH_FULL_IMAGE:figures/full_fig_p034_8.png] view at source ↗
Figure 9
Figure 9. Figure 9: An example from the SAP R/3 dataset (process id: 48 [PITH_FULL_IMAGE:figures/full_fig_p035_9.png] view at source ↗
read the original abstract

The Partially Ordered Workflow Language (POWL) has recently emerged as a process modeling notation, offering strong quality guarantees and high expressiveness. While early versions of POWL relied on strict block-structured operators for choices and loops, the language has recently evolved into POWL 2.0, introducing choice graphs to enable the modeling of non-block-structured decisions and cycles. To bridge the gap between the theoretical advantages of POWL and the practical need for compatibility with established notations, robust model transformations are required. This paper presents a novel algorithm for transforming safe and sound workflow nets (WF-nets) into equivalent POWL 2.0 models. The algorithm recursively identifies structural patterns within the WF-net and translates them into their POWL representation. Unlike the previous approach that required separate detection strategies for exclusive choices and loops, our new algorithm utilizes choice graphs to capture generalized decision and cyclic patterns. We formally prove the correctness of our approach, showing that the generated POWL model preserves the language of the input WF-net. Furthermore, we prove the completeness of our algorithm on the class of separable WF-nets, which corresponds to nets constructed via the hierarchical nesting of state machines and marked graphs. We evaluate our algorithm on large-scale process models to demonstrate its high scalability. Furthermore, to test its practical expressiveness, we applied it to a benchmark of 1,493 industrial and synthetic process models. Our algorithm successfully transformed all models in this benchmark, suggesting that POWL 2.0's expressive power is generally sufficient to capture the complex logic found in real-world business processes. This work paves the way for broader adoption of POWL in practical process analysis and improvement applications.

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.

Referee Report

2 major / 2 minor

Summary. The manuscript presents a recursive algorithm for transforming safe and sound workflow nets (WF-nets) into equivalent POWL 2.0 models. The algorithm identifies structural patterns in the input net and maps them to POWL constructs, employing choice graphs to represent non-block-structured decisions and cycles. It claims formal proofs that the output POWL model preserves the language of the input WF-net (correctness) and that the algorithm is complete for the class of separable WF-nets (those constructed by hierarchical nesting of state machines and marked graphs). The approach is evaluated by successfully transforming all 1,493 models in an industrial and synthetic benchmark.

Significance. If the inductive proofs hold, the work supplies a sound and complete bridge between classical WF-net theory and POWL 2.0, allowing practitioners to obtain models with POWL's quality guarantees from existing WF-net representations. The large-scale empirical result on 1,493 models indicates that POWL 2.0's expressiveness is sufficient for the majority of real-world processes, which is a concrete strength for adoption in process mining and analysis.

major comments (2)
  1. [§4.2] §4.2 (Proof of completeness): The inductive argument relies on every place and transition participating in exactly one identified pattern at each recursion level; an explicit statement of the pattern-partitioning invariant (and a short proof that safety/soundness guarantees it) would make the induction step fully self-contained.
  2. [§5.3] §5.3 (Benchmark evaluation): The claim that all 1,493 models were transformed successfully is reported without a breakdown by separability class or by presence of non-block choice/cycle structures; without this, it is difficult to assess how much of the success is due to the new choice-graph mechanism versus the restricted class of separable nets.
minor comments (2)
  1. [Figure 3] Figure 3 (decomposition example): the arrows between the original WF-net and the resulting POWL model are not labeled, making it hard to trace which choice-graph node corresponds to which original transition set.
  2. Notation: the paper uses both 'POWL' and 'POWL 2.0' interchangeably after the abstract; a single consistent term (or an explicit definition of the 2.0 extension) would improve readability.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the positive evaluation and the constructive suggestions that will improve the clarity of the completeness proof and the interpretation of the empirical results. We address each major comment below.

read point-by-point responses

  1. Referee: [§4.2] §4.2 (Proof of completeness): The inductive argument relies on every place and transition participating in exactly one identified pattern at each recursion level; an explicit statement of the pattern-partitioning invariant (and a short proof that safety/soundness guarantees it) would make the induction step fully self-contained.

    Authors: We agree that an explicit formulation of the pattern-partitioning invariant will make the induction more transparent. In the revised manuscript we will insert a dedicated paragraph in §4.2 that states the invariant formally and supplies a short, self-contained argument showing that it is preserved under the safety and soundness assumptions of the input WF-net. This addition does not change the substance of the proof but renders the induction step fully self-contained. revision: yes

  2. Referee: [§5.3] §5.3 (Benchmark evaluation): The claim that all 1,493 models were transformed successfully is reported without a breakdown by separability class or by presence of non-block choice/cycle structures; without this, it is difficult to assess how much of the success is due to the new choice-graph mechanism versus the restricted class of separable nets.

    Authors: We acknowledge that a finer-grained breakdown would aid interpretation. The benchmark models were not pre-classified by separability, and performing such a classification for all 1,493 instances would require an independent, non-trivial analysis that lies outside the scope of the present evaluation. In the revision we will add a short discussion in §5.3 that reports the frequency of non-block-structured choice and cycle patterns observed during transformation; this will illustrate the concrete contribution of the choice-graph constructs while preserving the original claim that the algorithm succeeded on the entire set. revision: partial

Circularity Check

0 steps flagged

No significant circularity detected

full rationale

The paper establishes correctness via a formal inductive proof on decomposition depth for language preservation and completeness on separable WF-nets. Base cases for state machines and marked graphs are handled directly from net definitions, and the inductive step uses the independent structural fact that choice graphs encode all interleavings and synchronizations present in the original net. No step reduces by construction to fitted parameters, self-referential definitions, or load-bearing self-citations; the algorithm and its proofs are self-contained against the stated safety/soundness preconditions and the external semantics of WF-nets and POWL 2.0.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The central claim rests on standard assumptions from Petri net theory and process modeling; no free parameters or invented entities are introduced in the abstract.

axioms (2)
  • domain assumption Input models are safe and sound workflow nets
    Required for the transformation to preserve language and for the algorithm to apply.
  • domain assumption Separable WF-nets are exactly those constructed by hierarchical nesting of state machines and marked graphs
    Used to define the class on which completeness is proven.

pith-pipeline@v0.9.0 · 5606 in / 1290 out tokens · 26429 ms · 2026-05-15T21:40:35.474114+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

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

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

32 extracted references · 32 canonical work pages

  1. [1]

    Petri net-based modelling of workflow systems: An overview.Eur

    Salimifard K, Wright M. Petri net-based modelling of workflow systems: An overview.Eur. J. Oper. Res., 2001.134(3):664–676. doi:10.1016/S0377-2217(00)00292-7

    work page doi:10.1016/s0377-2217(00)00292-7 2001

  2. [2]

    Business Process Model and Notation - BPMN

    von Rosing M, White S, Cummins F, de Man H. Business Process Model and Notation - BPMN. In: von Rosing M, von Scheel H, Scheer A (eds.), The Complete Business Process Handbook: Body of Knowledge from Process Modeling to BPM, V olume I, pp. 429–453. Morgan Kaufmann/Elsevier, Massachusetts, USA, 2015. doi:10.1016/B978-0-12-799959-3.00021-5

    work page doi:10.1016/b978-0-12-799959-3.00021-5 2015

  3. [3]

    Robust Process Mining with Guarantees - Process Discovery, Conformance Checking and Enhancement, volume 440 ofLecture Notes in Business Information Processing

    Leemans SJJ. Robust Process Mining with Guarantees - Process Discovery, Conformance Checking and Enhancement, volume 440 ofLecture Notes in Business Information Processing. Springer, 2022. ISBN 978-3-030-96654-6. doi:10.1007/978-3-030-96655-3

    work page doi:10.1007/978-3-030-96655-3 2022

  4. [4]

    In: Internation al Conference on Business Process Management

    Kourani H, van Zelst SJ. POWL: Partially Ordered Workflow Language. In: Business Process Man- agement - 21st International Conference, BPM 2023, Utrecht, The Netherlands, September 11-15, 2023, Proceedings. 2023 pp. 92–108. doi:10.1007/978-3-031-41620-0\ 6

    work page doi:10.1007/978-3-031-41620-0 2023

  5. [5]

    Discovering partially ordered workflow models

    Kourani H, van Zelst SJ, Schuster D, van der Aalst WMP. Discovering partially ordered workflow models. Inf. Syst., 2025.128:102493. doi:10.1016/J.IS.2024.102493

    work page doi:10.1016/j.is.2024.102493 2025

  6. [6]

    Process Modeling with Large Language Models

    Kourani H, Berti A, Schuster D, van der Aalst WMP. Process Modeling with Large Language Models. In: Enterprise, Business-Process and Information Systems Modeling - 25th International Conference, BPMDS 2024, and 29th International Conference, EMMSAD 2024, Limassol, Cyprus, June 3-4, 2024, Proceedings. 2024 pp. 229–244. doi:10.1007/978-3-031-61007-3\ 18

    work page doi:10.1007/978-3-031-61007-3 2024

  7. [7]

    Unlocking Non-Block-Structured Decisions: Inductive Mining with Choice Graphs

    Kourani H, Park G, van der Aalst WMP. Unlocking Non-Block-Structured Decisions: Inductive Mining with Choice Graphs. In: Senderovich A, Cabanillas C, Vanderfeesten I, Reijers HA (eds.), Business Process Management - 23rd International Conference, BPM 2025, Seville, Spain, August 31 - September 5, 2025, Proceedings, volume 16044 ofLecture Notes in Computer...

    work page doi:10.1007/978-3-032-02867-9 2025

  8. [8]

    ProMoAI: Process Modeling with Generative AI

    Kourani H, Berti A, Schuster D, van der Aalst WMP. ProMoAI: Process Modeling with Generative AI. In: Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence, IJCAI 2024, Jeju, South Korea, August 3-9, 2024. 2024 pp. 8708–8712

    work page 2024

  9. [9]

    Polynomial-Time Conformance Checking for Process Trees

    Rocha EG, van der Aalst WMP. Polynomial-Time Conformance Checking for Process Trees. In: Francescomarino CD, Burattin A, Janiesch C, Sadiq S (eds.), Business Process Management - 21st International Conference, BPM 2023, Utrecht, The Netherlands, September 11-15, 2023, Proceed- ings, volume 14159 ofLecture Notes in Computer Science. Springer, 2023 pp. 109–...

    work page 2023

  10. [10]

    Translating Workflow Nets into the Partially Ordered Work- flow Language

    Kourani H, Park G, van der Aalst WMP. Translating Workflow Nets into the Partially Ordered Work- flow Language. In: Amparore EG, Mikulski L (eds.), Application and Theory of Petri Nets and Con- currency - 46th International Conference, PETRI NETS 2025, Paris, France, June 22-27, 2025, Pro- ceedings, volume 15714 ofLecture Notes in Computer Science. Spring...

    work page doi:10.1007/978-3-031-94634-9 2025

  11. [11]

    MCC: A Tool for Unfolding Colored Petri Nets in PNML Format

    Dal-Zilio S. MCC: A Tool for Unfolding Colored Petri Nets in PNML Format. In: Janicki R, Sidorova N, Chatain T (eds.), Application and Theory of Petri Nets and Concurrency - 41st International Conference, PETRI NETS 2020, Paris, France, June 24-25, 2020, Proceedings, volume 12152 ofLecture Notes in Computer Science. Springer, 2020 pp. 426–435. doi:10.1007...

    work page doi:10.1007/978-3-030-51831-8 2020

  12. [12]

    Reduction Using Induced Subnets to Systematically Prove Properties for Free-Choice Nets

    van der Aalst WMP. Reduction Using Induced Subnets to Systematically Prove Properties for Free-Choice Nets. In: Buchs D, Carmona J (eds.), Application and Theory of Petri Nets and Concurrency - 42nd Inter- national Conference, PETRI NETS 2021, Virtual Event, June 23-25, 2021, Proceedings, volume 12734 of Lecture Notes in Computer Science. Springer, 2021 p...

    work page doi:10.1007/978-3-030-76983-3 2021

  13. [13]

    Semantics and analysis of business process models in BPMN.Inf

    Dijkman RM, Dumas M, Ouyang C. Semantics and analysis of business process models in BPMN.Inf. Softw. Technol., 2008.50(12):1281–1294. doi:10.1016/J.INFSOF.2008.02.006

    work page doi:10.1016/j.infsof.2008.02.006 2008

  14. [14]

    UML modelling of automated business processes with a mapping to BPEL4WS.Orientation and Web Services, 2003.30

    Gardner T. UML modelling of automated business processes with a mapping to BPEL4WS.Orientation and Web Services, 2003.30

    work page 2003

  15. [15]

    Petri Net Based Certification of Event-Driven Process Chains

    Langner P, Schneider C, Wehler J. Petri Net Based Certification of Event-Driven Process Chains. In: Desel J, Su´arez MS (eds.), Application and Theory of Petri Nets 1998, 19th International Conference, ICATPN ’98, Lisbon, Portugal, June 22-26, 1998, Proceedings, volume 1420 ofLecture Notes in Computer Science. Springer, 1998 pp. 286–305. doi:10.1007/3-540...

    work page doi:10.1007/3-540-69108-1 1998

  16. [16]

    The relationship between workflow graphs and free-choice workflow nets

    Favre C, Fahland D, V ¨olzer H. The relationship between workflow graphs and free-choice workflow nets. Inf. Syst., 2015.47:197–219. doi:10.1016/J.IS.2013.12.004

    work page doi:10.1016/j.is.2013.12.004 2015

  17. [17]

    Translating unstructured workflow processes to readable BPEL: Theory and implementation.Inf

    van der Aalst WMP, Lassen KB. Translating unstructured workflow processes to readable BPEL: Theory and implementation.Inf. Softw. Technol., 2008.50(3):131–159. doi:10.1016/J.INFSOF.2006.11.004

    work page doi:10.1016/j.infsof.2006.11.004 2008

  18. [18]

    WorkflowNet2BPEL4WS: A Tool for Translating Unstructured Workflow Processes to Readable BPEL

    Lassen KB, van der Aalst WMP. WorkflowNet2BPEL4WS: A Tool for Translating Unstructured Workflow Processes to Readable BPEL. In: Meersman R, Tari Z (eds.), On the Move to Meaningful Internet Systems 2006: CoopIS, DOA, GADA, and ODBASE, OTM Confederated International Conferences, CoopIS, DOA, GADA, and ODBASE 2006, Montpellier, France, October 29 - November...

    work page 2006

  19. [19]

    Translating Workflow Nets to Process Trees: An Algorithmic Approach

    van Zelst SJ, Leemans SJJ. Translating Workflow Nets to Process Trees: An Algorithmic Approach. Algorithms, 2020.13(11):279. doi:10.3390/A13110279. 38H. Kourani et al./Hierarchical Decomposition of Separable Workflow-Nets

    work page doi:10.3390/a13110279 2020

  20. [20]

    Reisig W, Rozenberg G (eds.). Lectures on Petri Nets I: Basic Models, Advances in Petri Nets, the volumes are based on the Advanced Course on Petri Nets, held in Dagstuhl, September 1996, volume 1491 of Lecture Notes in Computer Science. Springer, 1998. ISBN 3-540-65306-6. doi:10.1007/3-540-65306-6

    work page doi:10.1007/3-540-65306-6 1996

  21. [21]

    Free choice Petri nets

    Desel J, Esparza J. Free choice Petri nets. 40. Cambridge university press, 1995

    work page 1995

  22. [22]

    Circuits, handles, bridges and nets

    Esparza J, Su ´arez MS. Circuits, handles, bridges and nets. In: Rozenberg G (ed.), Advances in Petri Nets 1990 [10th International Conference on Applications and Theory of Petri Nets, Bonn, Germany, June 1989, Proceedings], volume 483 ofLecture Notes in Computer Science. Springer, 1989 pp. 210–242. doi:10.1007/3-540-53863-1\ 27

    work page doi:10.1007/3-540-53863-1 1990

  23. [23]

    Transformations and Decompositions of Nets

    Berthelot G. Transformations and Decompositions of Nets. In: Brauer W, Reisig W, Rozenberg G (eds.), Petri Nets: Central Models and Their Properties, Advances in Petri Nets 1986, Part I, Proceedings of an Advanced Course, Bad Honnef, Germany, 8-19 September 1986, volume 254 ofLecture Notes in Computer Science. Springer, 1986 pp. 359–376. doi:10.1007/BFB0046845

    work page doi:10.1007/bfb0046845 1986

  24. [24]

    Checking properties of nets using transformations

    Berthelot G, Lri-Iie. Checking properties of nets using transformations. In: Rozenberg G (ed.), Advances in Petri Nets 1985. Springer Berlin Heidelberg, Berlin, Heidelberg. ISBN 978-3-540-39822-6, 1986 pp. 19–40

    work page 1985

  25. [25]

    Petri nets: Properties, analysis and applications.Proc

    Murata T. Petri nets: Properties, analysis and applications.Proc. IEEE, 1989.77(4):541–580. doi: 10.1109/5.24143

    work page doi:10.1109/5.24143 1989

  26. [26]

    Maximal Structuring of Acyclic Process Models

    Polyvyanyy A, Garc ´ıa-Ba˜nuelos L, Fahland D, Weske M. Maximal Structuring of Acyclic Process Models. Comput. J., 2014.57(1):12–35. doi:10.1093/COMJNL/BXS126

    work page doi:10.1093/comjnl/bxs126 2014

  27. [27]

    PTandLogGenerator: A Generator for Artificial Event Data

    Jouck T, Depaire B. PTandLogGenerator: A Generator for Artificial Event Data. In: Azevedo L, Cabanil- las C (eds.), Proceedings of the BPM Demo Track 2016 Co-located with the 14th International Conference on Business Process Management (BPM 2016), Rio de Janeiro, Brazil, September 21, 2016, volume 1789 ofCEUR Workshop Proceedings. CEUR-WS.org, 2016 pp. 23–27

    work page 2016

  28. [28]

    Generating Artificial Data for Empirical Analysis of Control-flow Discovery Al- gorithms - A Process Tree and Log Generator.Bus

    Jouck T, Depaire B. Generating Artificial Data for Empirical Analysis of Control-flow Discovery Al- gorithms - A Process Tree and Log Generator.Bus. Inf. Syst. Eng., 2019.61(6):695–712. doi: 10.1007/S12599-018-0541-5

    work page doi:10.1007/s12599-018-0541-5 2019

  29. [29]

    PM4Py: A process mining library for Python.Softw

    Berti A, van Zelst SJ, Schuster D. PM4Py: A process mining library for Python.Softw. Impacts, 2023. 17:100556. doi:10.1016/J.SIMPA.2023.100556

    work page doi:10.1016/j.simpa.2023.100556 2023

  30. [30]

    Sound Workflow Systems Used in PQL Evaluations

    Polyvyanyy A. Sound Workflow Systems Used in PQL Evaluations. 2023. doi:10.26188/21937259.v1

    work page doi:10.26188/21937259.v1 2023

  31. [31]

    SAP R/3 business blueprint: understanding the business process reference model

    Curran T, Keller G, Ladd A. SAP R/3 business blueprint: understanding the business process reference model. Prentice-Hall, Inc., USA, 1997. ISBN 0135211476

    work page 1997

  32. [32]

    Process Query Language: Design, Implementation, and Evaluation.Inf

    Polyvyanyy A, ter Hofstede AHM, Rosa ML, Ouyang C, Pika A. Process Query Language: Design, Implementation, and Evaluation.Inf. Syst., 2024.122:102337. doi:10.1016/J.IS.2023.102337

    work page doi:10.1016/j.is.2023.102337 2024