Pith. sign in

REVIEW 4 major objections 4 minor 20 references

FoldA: Computing Partial-Order Alignments Using Directed Net Unfoldings

T0 review · 4 major / 4 minor · reviewed 2026-08-07 · deepseek-v4-flash

Pith's one-line read The paper introduces FoldA, an algorithm that computes optimal partial-order alignments by directed unfolding of the synchronous product of a process model and a trace, preserving concurrency without exploring the full reachability graph.

desk verdict Solid engineering contribution with a real proof gap in the adequate-order tie-break; worth refereeing after a fix. read the letter →

arxiv 2506.08627 v1 pith:T2EOYECT submitted 2025-06-10 cs.AI

classification cs.AI
keywords processminingconformancecheckingpartial-orderalignmentsPetrinetunfoldingadequateordercut-offeventsdirectedalignment
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

This paper claims that conformance checking can be made concurrency-preserving by computing partial-order alignments directly from a directed unfolding of the synchronous product of the process model and the trace, rather than searching the reachability graph. The algorithm, FoldA, expands the branching process event by event under a cost-based adequate order and stops as soon as the final marking is reached. Theorem 1 asserts that the returned partial-order alignment is valid, optimal, and found in finite time. The motivation is that sequential alignments impose an arbitrary total order on concurrent events, losing information about true dependencies; partial-order alignments retain those dependencies. If correct, this gives process mining a concurrency-preserving conformance check that competes with Astar and Dijkstra on state count, though slower in wall-clock time.

What carries the argument

The central object is the directed net unfolding: a branching process of the synchronous product built event-by-event by always adding the lowest-cost enabled event, guided by the adequate order $e \prec e'$ iff $Z([e], \zeta) \le Z([e'], \zeta)$, with ties broken by a unique identifier, and pruned by cut-off events when a marking has already been reached at no greater cost. The heuristic variant FoldAh adds a marking-equation lower bound $h(\text{Mark}([e]))$ to the cost, adopting an A* ordering while preserving the adequate order. This machinery lets the search stop as soon as the final marking is reached, avoiding construction of a complete prefix and thereby supporting unbounded easy-sound nets.

What would settle it

Run Algorithm 1 on a small synchronous product that contains two enabled events of equal $Z$-cost from the same marking, where one extension leads cheaply to the final marking and the other expensively; if FoldA returns an alignment with strictly greater cost than an alignment found by exhaustive search, then the tie-break failed to preserve the adequate order and Theorem 1's optimality claim is false.

Watch

Extended reading notes

Core claim

The central claim is that an optimal partial-order alignment is the local configuration $[e]$ of the first event $e$ in a directed net unfolding whose marking equals the final marking of the synchronous product, where the unfolding's adequate order is defined by the accumulated move cost $Z([e], \zeta)$ and events are expanded in best-first order. Because net unfoldings represent concurrency as a partial order rather than as interleavings, the returned configuration is itself a partial-order run of moves, and Theorem 1 states that it is valid (it corresponds to a firing sequence), complete (any valid alignment is contained in the unfolding), optimal (its cost is minimal among all valid alignments), and terminating. The practical claim is evaluated on 485 synthetic model-log pairs and 19 real-life and benchmark pairs, where FoldAh generally queues fewer states than Astar and Dijkstra while taking more computation time.

Load-bearing premise

The argument assumes that ordering events first by configuration cost and then by an arbitrary unique identifier (Python's id()) still satisfies the 'preserved by finite extensions' condition of an adequate order, so that no cut-off event ever discards a configuration needed for the optimal alignment.

Editorial extensions

If this is right

  • FoldA returns a partial-order alignment that preserves causal and concurrent relations between moves, so diagnoses can distinguish interleaving artifacts from real dependency deviations.
  • The directed unfolding terminates at the final marking, so it does not require a complete prefix, which is what allows handling of unbounded easy-sound nets.
  • The marking-equation heuristic is proven admissible in the unfolding setting, so FoldAh keeps optimality while reducing backtracking and queued states.
  • The algorithm opens the way to cost functions that are not additive over sequential moves, because the partial order is available during the search.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • If the adequate-order condition is violated by the identifier-based tie-break, the cut-off test could discard the configuration containing the optimal alignment; a small adversarial net with two same-cost, same-marking extensions that have different futures would settle this empirically.
  • Because the unfolding is built on the fly, the algorithm suggests a natural incremental or parallel variant where new trace events are appended and the search resumes, a direction the paper mentions but does not develop.
  • The heuristic's success hints that other admissible heuristics exploiting the partial-order structure directly, rather than the marking equation, could reduce FoldA's runtime gap relative to Astar.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

4 major / 4 minor

Summary. The paper introduces FoldA, an algorithm for computing partial-order alignments by unfolding the synchronous product of a trace net and a process model in a cost-directed manner. The unfolding is built on the fly and stops as soon as the final marking is reached; the algorithm returns the configuration reaching that marking as an allegedly optimal partial-order alignment. The paper defines a cost-based adequate order over local configurations using the cost function Z([e], ζ) with Python id() tie-breaking, and proposes a heuristic variant. It reports experiments on 485 synthetic model-log pairs and 19 real-life/benchmark pairs, comparing against PM4Py implementations of Dijkstra- and Astar-alignments.

Significance. If its correctness claims are established, FoldA would offer a concurrency-preserving alternative to sequential alignment computation and address a known limitation of methods that first compute a sequential optimal alignment and then derive a partial-order alignment from it. The empirical evaluation is a genuine strength: it is extensive (485 synthetic pairs, 13 real-life and 6 benchmark pairs), the code is publicly available, and all completed alignments matched baseline costs. However, the central optimality proof rests on an adequate-order claim that is not proven, so the theoretical contribution needs substantial repair.

major comments (4)
  1. [Section 4.1, after Algorithm 1] The order e ≺ e′ iff Z([e],ζ) ≤ Z([e′],ζ), with ties broken by Python id(), is asserted to be adequate, but Definition 12(3), preservation by finite extensions, is not verified for this tie-break. The order is only defined on events and local configurations, not on all finite configurations, so condition 3 is not even well-formed as stated. Moreover, Python id() values are memory addresses and are not invariant under the configuration isomorphism I_2^1 used in Definition 12(3); under any natural extension of the order to arbitrary configurations, equal-cost same-marking local configurations can be reversed after adding one-event extensions with different ids. Since cut-off events are pruned and the algorithm stops at the first final marking, a failure of adequacy would invalidate Theorem 1(2)-(4). A proof of adequacy for a canonically defined, isomorphism-invariant tie-break (or a different adequate order) is required.
  2. [Section 4.1, Proof of Theorem 1] The proof of claims (2) and (4) cites Theorem 4.3.4 and Lemma 4.4.1 of [3] and the ERV unfolding guarantee to conclude that the final marking is reachable in sp and therefore 'also reachable in β'. But Algorithm 1's β is an on-the-fly directed prefix with cut-offs and early stopping, not an ERV complete prefix, so the cited guarantees do not apply. The early-stopping rule in Lines 12-15 requires a separate proof that no pruned branch contains a lower-cost path to the final marking; this is exactly what the adequate-order condition would supply, and that condition is not established.
  3. [Section 4.2, Theorem 3] The proof of Theorem 3 is invalid. From the contradiction hypothesis Z([e1])+h(Mark([e1])) > Z([e2])+h(Mark([e2])), the paper obtains h(Mark([e1])) > Z(Ed)+h(Mark([e2])). Because h(Mark([e2])) is only a lower bound on the true remaining cost, this does not imply the existence of a path from Mark([e1]) to fm with cost smaller than h(Mark([e1])); the actual path through Ed has cost Z(Ed)+dist(Mark([e2]),fm), which can be larger than Z(Ed)+h(Mark([e2])). Thus the monotonicity condition C1 ⊂ C2 ⇒ C1 ≺ C2 is not proven for the heuristic order, and the heuristic variant's optimality is not established.
  4. [Appendix B and Section 2] Appendix B states that 'in the following, we assume all nets to be 1-safe nets', while Section 2 claims that the approach supports 'unbounded, easy sound nets' and Appendix A.2 provides an example. The formal definitions and proofs are carried out only for 1-safe nets; a single example does not establish correctness for unbounded nets. The paper should either restrict its scope statement or provide a separate correctness argument for the unbounded case.
minor comments (4)
  1. [Algorithm 1, Data line] The word 'reachabile' should be 'reachable'.
  2. [Definition 8] The notation C ⊕ E would be clearer if E were explicitly defined as a finite set of events in the unfolding and if the definition stated that C ⊕ E is the configuration C ∪ E.
  3. [Section 5.2, Table 2] The reported medians and means are computed only over finished traces, while FoldAh timed out on several datasets (e.g., ITL prCm6, BPIC17); the text should state this bias explicitly as a limitation of the comparison.
  4. [Section 4.2, Theorem 2] Theorem 2 is essentially tautological, and its hypothesis refers to a 'complete, finite prefix' that is never constructed by Algorithm 1; either remove it or state clearly how it applies to the directed prefix built by the algorithm.

Circularity Check

2 steps flagged · score 4.0 of 10

Correctness derivation is partially circular: Theorem 3 prices the 'contradicting path' with the heuristic's own estimate, and Theorem 1's optimality rests on the asserted adequacy of the Z-plus-Python-id order.

  1. other [Section 4.2, Theorem 3 proof (adequate-order condition 2 for FoldAh)]
    "Let Ed = [e2] \ [e1], i.e., [e1] ∪ Ed = [e2]. This implies that h(Mark ([e1])) > Z(Ed, ζ) + h(Mark ([e2]). This implies that there exists a path from Mark ([e1]) to the final marking fm via Ed and Mark ([e2]) that is cheaper than the heuristic from Mark ([e1]) alone. This contradicts the assumption that h is a lower bound."

    The claimed contradiction requires the 'path via Ed and Mark([e2])' to be a real firing sequence whose continuation from Mark([e2]) costs h(Mark([e2])). But h is the marking-equation (ILP) estimate: a minimal marking-equation solution need not be realizable as a firing sequence, and admissibility gives only h ≤ d (true optimal distance), the reverse of what is needed to price a real continuation. The proof therefore constructs the cheaper path using the heuristic's own numerical value as if it were an achievable continuation cost, which is exactly the realizability/monotonicity property that Theorem 3 (needed for condition (2) of Definition 12) is meant to establish.

  2. other [Section 4.1, after Algorithm 1 (adequate-order definition); Definition 12(3); Theorem 1 proof]
    "Thus, e ≺ e′ if and only if Z([e], ζ) ≤ Z([e′], ζ). To break any ties and maintain the adequate order ≺, each event e is assigned a unique numerical identifier using Python's built-in id () function. [...] Our algorithm explores configurations in order of increasing cost guaranteed by ≺ and selects the first reaching fm, ensuring optimality."

    Definition 12(3) requires ≺ to be preserved by finite extensions: if Mark(C1)=Mark(C2) and C1≺C2, then C1⊕E ≺ C2⊕I(E) under the configuration isomorphism I. The cost part of Z is preserved because Z(E)=Z(I(E)), but a Python id() tie-break is an object-creation memory address with no invariance under I, and the paper never defines ≺ on arbitrary finite configurations (only on local configurations/events, despite Definition 12 talking about all finite configurations). The 'maintain the adequate order' sentence is an assertion, not a derivation, and Theorem 1(2)-(4) lean on it while importing ERV complete-prefix reachability ('the final marking fm is reachable in sp, thus, also reachable in β') to an early-stopped directed prefix that is deliberately not a complete prefix.

full rationale

The paper's cost objective is self-contained: Z([e],ζ) sums a fixed per-transition cost (0 synchronous, 1 model/log, 0.0001 silent) over a local configuration, and Algorithm 1 chooses the first final-marking configuration in ≺-order. Minimizing one's own declared objective in an algorithm is legitimate, and the evaluation is externally anchored: PM4Py Astar/Dijkstra alignments on the same data and same cost function produce identical optimal costs, and the queued/visited-state and time measurements are independently reproducible from the released code. The self-citations are not load-bearing for the theorems: [13] (co-authored by Lu) supplies the problem statement and motivation for partial-order alignments, [8] (Geurtjens' thesis) is a priority claim, while Theorem 1's proof actually cites external works [3] and [6]. Two genuine circular/asserted steps remain in the proof chain. First, Theorem 3's proof of monotonicity for the heuristic order prices the alleged contradicting path at h(Mark([e2])) — the marking-equation estimate — which need not be a realizable firing sequence; since admissibility gives h ≤ d, the proof assumes the exactness of h at the intermediate marking to manufacture the contradiction, i.e., it presupposes the realizability property that the theorem must establish. Second, the adequacy of the Z-plus-Python-id order is asserted ('To break any ties and maintain the adequate order') rather than verified against Definition 12(3), where the tie-break's failure to be isomorphism-invariant is the salient risk; Theorem 1(2)-(4) additionally import ERV complete-prefix guarantees to a prefix that stops at the first final marking. These are proof-chain circularities and unproven premises, not fitted-input predictions: no parameter is fitted to data and renamed as a prediction, so the score is moderate rather than high. Appendix B's later 'we assume all nets to be 1-safe nets' also conflicts with the claimed unbounded easy-sound support (Section 2, Appendix A.2); that is a correctness gap, not circularity, but it is flagged as an in-paper limitation to weigh.

Assumptions & free parameters 1 free parameters · 4 assumptions · 0 invented entities

The central claim rests on standard Petri-net unfolding theory plus the paper-specific assertion that the cost-based order is adequate. The only hand-fitted quantity is the move-cost vector ζ; the heuristic is derived from the marking equation, not fitted. No new physical or formal entities are introduced.

free parameters (1)
  • move cost function ζ(t) = 0 for synchronous moves, 1 for model/log moves, 0.0001 for silent moves
    Defined in Algorithm 1 line 1; the optimality result is relative to this cost. The 0.0001 for silent transitions is a hand-chosen small penalty so silent moves are cheaper than deviations but do not dominate the cost.
assumptions (4)
  • domain assumption All nets are 1-safe (each place holds at most one token in any reachable marking).
    Appendix B below Definition 14 states: 'In the following, we assume all nets to be 1-safe nets.' The central algorithm and the unfolding theory rely on this, yet the paper later claims to handle unbounded easy sound nets, creating an inconsistency.
  • ad hoc to paper The cost-based order defined by Z([e], ζ) with Python id() tie-breaking is an adequate order.
    Section 4.1 after Algorithm 1 introduces this order and uses it for cut-off detection; adequacy (Definition 12) is required for the optimality proof but is asserted, not demonstrated.
  • domain assumption Easy soundness of the synchronous product: the final marking fm is reachable from the initial marking.
    Definition 1 and Algorithm 1's termination condition presuppose a reachable final marking; the paper assumes this for the model and constructs the event net so that fm is reachable.
  • standard math Completeness of the ERV/McMillan prefix-unfolding machinery: the generated branching process contains a configuration for every reachable marking (up to adequate-order cut-offs).
    The algorithm builds on [6,17] for cut-off events; Theorem 1's part (2) relies on this background result, though it is cited to [3] instead.

how reviews work

0 comments
Cite this review

Pith. "Pith review of FoldA: Computing Partial-Order Alignments Using Directed Net Unfoldings." pith.science (2026). https://pith.science/paper/T2EOYECT

@misc{pith2026250608627,
  author       = {Pith},
  title        = {Pith review of: FoldA: Computing Partial-Order Alignments Using Directed Net Unfoldings},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/T2EOYECT}},
  note         = {Machine review of arXiv:2506.08627}
}
read the original abstract

Conformance checking is a fundamental task of process mining, which quantifies the extent to which the observed process executions match a normative process model. The state-of-the-art approaches compute alignments by exploring the state space formed by the synchronous product of the process model and the trace. This often leads to state space explosion, particularly when the model exhibits a high degree of choice and concurrency. Moreover, as alignments inherently impose a sequential structure, they fail to fully represent the concurrent behavior present in many real-world processes. To address these limitations, this paper proposes a new technique for computing partial-order alignments {on the fly using directed Petri net unfoldings, named FoldA. We evaluate our technique on 485 synthetic model-log pairs and compare it against Astar- and Dijkstra-alignments on 13 real-life model-log pairs and 6 benchmark pairs. The results show that our unfolding alignment, although it requires more computation time, generally reduces the number of queued states and provides a more accurate representation of concurrency.

Figures

Figures reproduced from arXiv: 2506.08627 by the authors.

Figure 1
Figure 1. A Petri net M (left) and a partial-order trace σ (right). S,S A,A B,B C,C (t1, e1) (t2, e2) (t3, e3) (t4, e4) S,S A,A B,B (t5, e1) (t6, e2) (t7, e3) [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 3
Figure 3. [PITH_FULL_IMAGE:figures/full_fig_p004_3.png] view at source ↗
Figure 4
Figure 4. shows the resulting synchronous product of Nl and N1, which is constructed as follows: the transitions present in the model become model moves (colored blue), the transitions in the event net become log moves (colored yellow), and for each pair of transitions that have the same label, we create a synchronous move transition (colored green). By exploring the reachability graph of the synchronous product using a short… view at source ↗
Figures from the paper (11 more)
Figure 5
Figure 5. Figure 5: shows a branching process of the net in [PITH_FULL_IMAGE:figures/full_fig_p006_5.png]
Figure 6
Figure 6. Figure 6: An overview of the unfolding alignment approach [PITH_FULL_IMAGE:figures/full_fig_p007_6.png]
Figure 7
Figure 7. Figure 7: The branching process constructed by Algorithm 1 on the synchronous product in 4. The optimal partial-order alignment is highlighted in green [PITH_FULL_IMAGE:figures/full_fig_p009_7.png]
Figure 9
Figure 9. Figure 9: Examples of the artificially generated models used in experiment 1. To simulate deviations, we systematically removed one event per trace at the start, middle, or end. We decided not to insert or replace the events due to the combinatorial explosion of options. Each al…
Figure 10
Figure 10. Figure 10: #VS vs #SPT, across model types and deviation placements, comparing FoldAn (top four) with FoldAh (bottom four) [PITH_FULL_IMAGE:figures/full_fig_p013_10.png]
Figure 11
Figure 11. Figure 11: Elapsed time per #VS across model types and deviation placements, comparing FoldAn (top four) versus FoldAh (bottom four). alignments rely on a branching process, which requires the checking of multiple condition sets per transition to determine whether the transition…
Figure 12
Figure 12. Figure 12: (c) depicts the relationship between visited states and elapsed time, with the log-log plot suggesting a polynomial correlation. Similarly, [PITH_FULL_IMAGE:figures/full_fig_p015_12.png]
Figure 13
Figure 13. Figure 13: The partial order trace, converted to an event net [PITH_FULL_IMAGE:figures/full_fig_p018_13.png]
Figure 16
Figure 16. Figure 16: An unbounded, easy sound net, meaning the final marking is reachable, where the final marking is a token in the initial place and a token in the final place [PITH_FULL_IMAGE:figures/full_fig_p018_16.png]
Figure 17
Figure 17. Figure 17: The synchronous product between the easy sound net and the trace σ = ⟨SubmitPD, MakeBk⟩. Note that we added a dummy start and a dummy end transition to ease the checking of termination conditions [PITH_FULL_IMAGE:figures/full_fig_p018_17.png]
Figure 18
Figure 18. Figure 18: The directed unfolding, trying to find the target marking [PITH_FULL_IMAGE:figures/full_fig_p019_18.png]

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

20 extracted references · 16 canonical work pages

  1. [3]

    Adriansyah, A.: Aligning observed and modeled behavior (2014)

  2. [1]

    In: Process Mining Handbook, Lecture Notes in Business Information Processing, vol

    van der Aalst, W.M.P.: Process mining: A 360 degree overview. In: Process Mining Handbook, Lecture Notes in Business Information Processing, vol. 448, pp. 3–34. Springer (2022)

  3. [2]

    WIREs Data Mining Knowl

    van der Aalst, W.M.P., Adriansyah, A., van Dongen, B.F.: Replaying history on process models for conformance checking and performance analysis. WIREs Data Mining Knowl. Discov.2(2), 182–192 (2012)

  4. [4]

    Bonet, B., Haslum, P., Hickmott, S.L., Thiébaux, S.: Directed unfolding of petri nets. vol. 1, pp. 172–198 (2008)

  5. [5]

    Theoretical Computer Science551, 84–101 (2014)

    Bonet, B., Haslum, P., Khomenko, V., Thiébaux, S., Vogler, W.: Recent advances in unfolding technique. Theoretical Computer Science551, 84–101 (2014)

  6. [6]

    In: TACAS

    Esparza, J., Römer, S., Vogler, W.: An improvement of mcmillan’s unfolding algorithm. In: TACAS. LNCS, vol. 1055, pp. 87–106. Springer (1996)

  7. [7]

    IEEE Trans

    García-Bañuelos, L., van Beest, N., Dumas, M., Rosa, M.L., Mertens, W.: Complete and interpretable conformance checking of business processes. IEEE Trans. Software Eng. 44(3), 262–290 (2018)

  8. [8]

    Master’s thesis, Utrecht University (2024)

    Geurtjens, D.: Computing Partial Order Alignments Using Net Unfoldings. Master’s thesis, Utrecht University (2024)

Show all 20 references
  1. [9]

    https: //doi.org/10.5281/zenodo.15552463

    Geurtjens, D.: Douwegeurtjens/unfolding-alignments: v1.0 (may 2025). https: //doi.org/10.5281/zenodo.15552463

  2. [10]

    In: CAiSE

    Gianola, A., Montali, M., Winkler, S.: Object-centric conformance alignments with synchronization. In: CAiSE. LNCS, vol. 14663, pp. 3–19. Springer (2024)

  3. [11]

    IEEE Trans

    Greco, G., Guzzo, A., Pontieri, L., Saccà, D.: Discovering expressive process models by clustering log traces. IEEE Trans. Knowl. Data Eng.18(8), 1010–1027 (2006)

  4. [12]

    Leemans, S.J.J., van Zelst, S.J., Lu, X.: Partial-order-based process mining: a survey and outlook. Knowl. Inf. Syst.65(1), 1–29 (2023)

  5. [13]

    In: BPM Workshops

    Lu, X., Fahland, D., van der Aalst, W.M.P.: Conformance checking based on partially ordered event data. In: BPM Workshops. LNBIP, vol. 202, pp. 75–88. Springer (2014)

  6. [14]

    In: ETFA

    Lu, X., Mans, R., Fahland, D., van der Aalst, W.M.P.: Conformance checking in healthcare based on partially ordered event data. In: ETFA. pp. 1–8. IEEE (2014)

  7. [15]

    Mannhardt, F.: Sepsis cases - event log (2016).https://doi.org/10.4121/UUID: 915D2BFB-7E84-49AD-A286-DC35F063A460

  8. [16]

    Computing 98(4), 407–437 (2016)

    Mannhardt, F., de Leoni, M., Reijers, H.A., van der Aalst, W.M.P.: Balanced multi-perspective checking of process conformance. Computing 98(4), 407–437 (2016)

  9. [17]

    McMillan, K.L.: Using unfoldings to avoid the state explosion problem in the verification of asynchronous circuits. In: CAV. LNCS, vol. 663, pp. 164–177. Springer (1992)

  10. [18]

    Munoz-Gama, J., Carmona, J., van der Aalst, W.M.P.: Conformance checking in the large: Partitioning and topology. In: BPM. LNCS, vol. 8094, pp. 130–145. Springer (2013)

  11. [19]

    Rozinat, A., van der Aalst, W.M.P.: Conformance checking of processes based on monitoring real behavior. Inf. Syst.33(1), 64–95 (2008)

  12. [20]

    CoRR abs/2504.00550 (2025 (April 4)) 18 Geurtjens and Lu A Additional Examples A.1 Partial-order traces Fig.13: The partial order trace, converted to an event net

    Siddiqui, A., van der Aalst, W.M.P., Schuster, D.: Computing alignments for partially-ordered traces through petri net unfoldings. CoRR abs/2504.00550 (2025 (April 4)) 18 Geurtjens and Lu A Additional Examples A.1 Partial-order traces Fig.13: The partial order trace, converted...

Pith tools

Reviewed August 7, 2026 · model on record in the stance chip above.