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 →
The pith
A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.
The reading
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.
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
- 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.
Editorial analysis
A structured set of objections, weighed in public.
Referee Report
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)
- [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.
- [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.
- [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.
- [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)
- [Algorithm 1, Data line] The word 'reachabile' should be 'reachable'.
- [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.
- [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.
- [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
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.
-
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.
-
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
free parameters (1)
- move cost function ζ(t) =
0 for synchronous moves, 1 for model/log moves, 0.0001 for silent moves
assumptions (4)
- domain assumption All nets are 1-safe (each place holds at most one token in any reachable marking).
- ad hoc to paper The cost-based order defined by Z([e], ζ) with Python id() tie-breaking is an adequate order.
- domain assumption Easy soundness of the synchronous product: the final marking fm is reachable from the initial marking.
- 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).
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 from the paper (11 more)
Reference graph
Works this paper leans on
-
[3]
Adriansyah, A.: Aligning observed and modeled behavior (2014)
2014
-
[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)
2022
-
[2]
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)
work page 2012
-
[4]
Bonet, B., Haslum, P., Hickmott, S.L., Thiébaux, S.: Directed unfolding of petri nets. vol. 1, pp. 172–198 (2008)
work page 2008
-
[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)
work page 2014
- [6]
-
[7]
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)
work page 2018
-
[8]
Master’s thesis, Utrecht University (2024)
Geurtjens, D.: Computing Partial Order Alignments Using Net Unfoldings. Master’s thesis, Utrecht University (2024)
work page 2024
Show all 20 references
-
[9]
https: //doi.org/10.5281/zenodo.15552463
Geurtjens, D.: Douwegeurtjens/unfolding-alignments: v1.0 (may 2025). https: //doi.org/10.5281/zenodo.15552463
2025 doi
-
[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)
2024
-
[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)
2006
-
[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)
2023
-
[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)
2014
-
[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)
2014
-
[15]
Mannhardt, F.: Sepsis cases - event log (2016).https://doi.org/10.4121/UUID: 915D2BFB-7E84-49AD-A286-DC35F063A460
2016 doi
-
[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)
2016
-
[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)
1992
-
[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)
2013
-
[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)
2008
-
[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...
2025 arXiv
Reviewed August 7, 2026 · model on record in the stance chip above.
Discussion (0). Sign in to comment.