{"id":"ea63ad99-783f-41f3-958f-fbbc6e0dcd6a","arxiv_id":"2505.15409","paper_version":1,"verdict":"REJECT","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"high","formal_verification":"none","parameter_count":0,"one_line_summary":"DOPIDs extend object-centric Petri nets with structured data, aggregation guards, and exact synchronization, and are paired with an SMT-based conformance checking method.","lead":"The paper introduces DOPIDs, a modeling language for business processes in which objects such as orders and products carry data values, and activities can wait until all connected objects are ready. It also gives a method based on SMT solvers to check how well a recorded event log matches such a model.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The SMT encoding's synced(p,t,j) counts all tokens in a place rather than only tokens matching the =-inscription, so Definition 6 is mis-encoded and Theorem 1's completeness fails on a two-parent-object instance.","rationale":"The reader's weakest assumption is exactly the point I would stress: the synced(p,tl,j) constraint in the Appendix equates the total number of tokens in a place with the size of the list instantiation, whereas Definition 6 only demands maximality among matching tokens. My concrete two-parent-object counterexample shows this is not a mere proof gap but a false encoding: a firing that is valid according to the semantics is rejected by the SMT formula, so Theorem 1's completeness direction fails. This is load-bearing because the paper's 'operational' claim and its novelty (exact synchronization with structured data) rest entirely on this theorem. The concern is not about the DOPID formalism itself, which is carefully developed, nor about the general SMT approach, which may be repairable by changing synced to a cardinality constraint over matching tokens. But as written, the central correctness claim does not hold, so I agree with the reader's REJECT verdict and do not see a reason to change it.","tokens_in":21891,"tokens_out":7624,"duration_ms":72234,"concrete_test":"Hand-encode or run in the released CoCoMoT implementation the minimal DOPID with initial marking p={<a,x>,<b,y>}, q={<a>}; transition t (label A) with input flows q:<o> and p:<o,P=>, output flows p:<o,P> and r:<o>; final marking r={<a>}. The trace graph is one event A on object {a}. Definition 6 says t is enabled with o=a and P=[x], so the optimal alignment is the single synchronous move with cost 0. Solve the published formula Phi from Appendix A: if it is unsatisfiable or returns cost > 0, the synced equation is confirmed wrong. Then patch synced to count only tokens in p whose fixed components equal the binding, and verify the same instance becomes satisfiable with cost 0.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central claim is Theorem 1 in Appendix A: every satisfying assignment of the SMT formula Phi decodes to an optimal alignment. The proof of Theorem 1 rests on the encoding of =-template flows in phi_move, specifically synced(p,tl,j). For an =-inscription with list variable V1, the paper sets synced(p,tl,j) equal to the total number of tokens in place p at time j-1 being equal to the number of objects used to instantiate V1. This is a whole-place cardinality constraint. Definition 6, however, requires maximality only among tokens matching the other fixed components of the inscription: a binding b is enabled iff no binding b' differing only on V= consumes a strict superset of b(F_in(p,t)). Tokens in p whose non-list components differ from b's assignment are irrelevant. Concretely, if p contains <a,x> and <b,y>, and t has input <o,P=> with o bound to a, Definition 6 permits firing with P=[x], because no larger list for the same a exists in p. The encoding's synced equation forces 2=1 and blocks this firing. The solver can only satisfy the formula by renaming the object or by adding extra model moves, so the decoded alignment is not optimal and alpha(delta_{m,n}) overestimates the true optimum. Since exact synchronization is the paper's headline extension over OPIDs, this invalidates Theorem 1 as stated.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper introduces data-aware object-centric Petri nets with identifiers (DOPIDs), a formalism that extends OPIDs with structured data types and exact synchronization, and proposes an SMT-based conformance checking approach. The paper defines the DOPID semantics (Definitions 4–7), formulates alignment-based conformance checking (Definitions 8–11), and gives an SMT encoding in Appendix A with a claimed correctness theorem (Theorem 1) stating that any satisfying assignment decodes to an optimal alignment. A proof-of-concept implementation extending CoCoMoT is also reported.","tokens_in":22132,"tokens_out":11757,"duration_ms":95157,"significance":"If the proposed encoding were correct, the paper would make a significant contribution: DOPIDs would be the first PNID-based formalism supporting both structured data and exact synchronization with a conformance checking algorithm, and the SMT approach would be a natural and operational way to compute alignments. The formalism itself is well motivated, the running example is instructive, and the semantics are carefully presented. The paper also honestly states the lack of experimental evaluation and the reliance on a technical report for some details. However, the central correctness claim is not established by the material in the manuscript because the synchronization encoding is inconsistent with the formal semantics and the data-related constraints are absent from the appendix.","major_comments":[{"comment":"The encoding of =-template synchronization contradicts Definition 6. The paper defines synced(p,t_l,j) as the equality between the total number of tokens in place p at time j−1 and the number of objects used to instantiate the list variable. Definition 6, however, requires maximality only among tokens matching the other fixed components of the inscription, not among all tokens in the place. Concretely, if place p contains ⟨a,x⟩ and ⟨b,y⟩, and transition t has input inscription ⟨o,P=⟩ with o bound to a, then Definition 6 permits firing with P=[x] because no binding b′ differing only on P= consumes a strict superset of {⟨a,x⟩} among tokens matching o=a. The encoding's synced equation forces 2=1 and blocks this firing. The solver can then only satisfy the formula by renaming the object or by inserting additional model moves, so the decoded alignment is not optimal and the computed cost α(δ_{m,n}) can overestimate the true optimum. This makes the SMT encoding incomplete with respect to the formal semantics, so the conformance checking method does not, as claimed, compute optimal alignments in general.","section":"Appendix A, φ_move / synced"},{"comment":"The proof of Theorem 1 establishes only that Γ(α) is an optimal alignment of T_X and the fixed decoded run ρ_α; it does not show that ρ_α is an optimal run of the net N. The minimization over δ_{m,n} in (Φ) can yield a globally optimal alignment only if the encoding faithfully represents every run of N, i.e., if for every run there is a corresponding satisfying assignment. The paper never proves this completeness direction, and the synced flaw described above is a concrete counterexample to it. Consequently, the theorem as stated does not support the paper's operational claim that optimal alignments for N and T_X can be decoded from satisfying assignments.","section":"Appendix A, Theorem 1 proof"},{"comment":"The data variables D_{i,x} and S_{i,p,o,l} introduced in the 'Variables' subsection are never used in any of the constraints (1)–(7) or in φ_δ. Moreover, φ_guard is written as guard(t_l)(O_{j,1},…,O_{j,K}), i.e., only over object variables, so guards involving data variables such as d≤5 or sum(cost(P))≤1000 from Sections 3–4 have no encoding in the presented appendix. The paper claims structured data support as a main contribution, but the encoding as written is an encoding of object identities only. The missing data constraints must be supplied, or the theorem must be restricted to a data-free fragment, or the appendix must explicitly defer to reference [20] for the data part.","section":"Appendix A, variables (f)–(g) and φ_guard"},{"comment":"Lemma 1 is imported from the authors' prior work [19] with the assertion that the presence of data and synchronization 'does not affect the reasoning of that proof'. This assertion is not justified. In particular, =-template synchronization allows a single transition to consume arbitrarily many tokens, which could affect the bound on the number of moves and objects in an optimal alignment. Since the SMT encoding fixes the parameters n and K based on Lemma 1, a rigorous justification of the bound for DOPIDs is load-bearing for the completeness of the encoding.","section":"Appendix A, Lemma 1"}],"minor_comments":[{"comment":"The prose here correctly states that =-template inscriptions 'do not consume all tokens contained in a place, but all those that match the inscription', which directly conflicts with the synced constraint in Appendix A; this inconsistency should be resolved.","section":"Section 4, after Definition 4"},{"comment":"The notation in the synced equation is ambiguous: it sums over i=1..h of (O_{j,k_i}≠0), but for a list variable there are multiple object indices, so the intended count of consumed list elements is unclear. The definition should use the explicit list indices ℓ_1,…,ℓ_x.","section":"Appendix A, synced definition"},{"comment":"The statement 'we show that from a satisfying assignment to all constraints, an optimal alignment for N and T_X can be decoded' is stronger than what Theorem 1 actually proves; the theorem only asserts optimality with respect to the decoded run. This overstatement should be corrected.","section":"Section 5, SMT encoding paragraph"},{"comment":"The paper defers details of the encoding to reference [20], yet Appendix A is titled 'Encoding' and claims to detail the approach. The appendix should be self-contained or should explicitly state which parts are deferred and what the deferred parts contain.","section":"References [19][20]"},{"comment":"The alignment table in Example 6 is difficult to parse because the layout of log moves, model moves, and the note about the synchronous ship move is not immediately clear; a labeled table with separate columns for log and model moves would improve readability.","section":"Example 6"},{"comment":"The condition on the model projection 'for all ⟨r,r′⟩∈B_m there are 1≤i<j≤n such that f(t_i,b_i)=r and f(t_j,b_j)=r′' is imprecise about edges between consecutive transitions; it should either require j=i+1 or explicitly allow shortcut edges consistent with the projection definition in [25,19].","section":"Definition 9"}],"recommendation":"major_revision","confidential_remarks":"The central technical claim of the paper is not supported by the presented encoding: the synchronization constraint in Appendix A is inconsistent with Definition 6, and the data-related constraints are entirely absent from the appendix. These are serious issues, but they are locally fixable (in principle) by rewriting the synced constraint, adding the missing data constraints, and proving completeness of the encoding. The paper also leans heavily on the authors' own prior work, both for the alignment bound (Lemma 1) and for the encoding details ([20]); the submitted manuscript should be self-contained on these points. Given the load-bearing nature of the errors, I recommend major revision rather than rejection, provided the authors can supply a correct encoding and a complete proof of Theorem 1."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Here's the bottom line: the paper's DOPID formalism is careful and the motivation is real, but the main algorithmic claim—Theorem 1—rests on an SMT encoding that mis-handles exact synchronization. The synced(p,tl,j) constraint counts every token in a place, while Definition 6 requires consuming all tokens matching the inscription's fixed components. With two parent objects in the same place, a valid firing can be blocked or the solver renames objects, so the decoded alignment is not necessarily optimal. This is not a nitpick; it is the load-bearing part of the conformance checking claim.\n\nWhat's good: DOPIDs are a natural and well-defined extension of OPIDs with structured data and full synchronization. The running example (order-to-shipment) convincingly shows what exact synchronization buys you, and the formal semantics (Definitions 5–7) are coherent. The idea of lifting the SMT-based alignment encoding from OPIDs and DPNs is sensible, and the paper is honest about what it borrows. The appendix contains a real correctness proof attempt, which is more than many papers do.\n\nThe soft spots are in proportion: the main one is the encoding bug. The transfer of Lemma 1 from [19] is asserted without re-derivation; this may be fine, but it should be checked because data and synchronization could affect the bound. The experimental evidence is anecdotal—one example, sub-second runtime—so the 'operational' claim is not backed by a real evaluation. These are minor compared to the encoding issue.\n\nWho is this for? Researchers working on object-centric process mining and formal verification of data-aware processes. They will want to know about DOPIDs even if the current algorithm is flawed. I would send this to peer review, because the formalism and the direction are valuable; the reviewer should ask for a corrected encoding and a proof that the constraint can be fixed (or a statement of what fragment it works for). But as submitted, the central claim does not hold.","headline":"The DOPID formalism is solid and well-motivated, but the SMT encoding for =-template synchronization counts all tokens in a place rather than only matching ones, so Theorem 1 as stated does not hold.","tokens_in":22683,"tokens_out":2250,"would_cite":true,"duration_ms":20243,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"The paper claims that data-aware object-centric Petri nets with identifiers—supporting structured attributes, aggregation guards, and exact synchronization—can be conformance-checked by an SMT encoding that decodes satisfying assignments…","keywords":["DOPID","object-centric processes","conformance checking","exact synchronization","structured data","Petri nets with identifiers","SMT","alignment"],"falsifier":"Exhibit a DOPID and event log where a correlation place holds tokens for two distinct parent objects, an =-inscription on a transition consumes only one parent's tokens, and a valid optimal alignment exists; if the SMT formula is unsatisfiable or forces extra model moves under those conditions, the encoding's $synced$ equation fails to enforce the paper's Definition 6, which requires consuming all matching tokens rather than all tokens.","tokens_in":21613,"feed_emoji":"⚙️","tokens_out":6790,"duration_ms":53788,"temperature":0.7,"pith_summary":"This paper introduces data-aware object-centric Petri nets with identifiers (DOPIDs), a formalism that extends OPIDs with two capabilities no previous PNID variant combined: structured data values (integers, rationals, strings, finite sets, uninterpreted functions) attached to tokens, and exact synchronization, in which a transition may fire only when all objects related to a given parent flow through it together. Against the expectation that combining these features would make analysis intractable, the paper claims conformance checking remains operational: it gives an SMT encoding of the alignment problem, and proves (Theorem 1) that any satisfying assignment to the formula decodes into an optimal alignment of the observed trace graph and the decoded model run, with cost equal to the formula's optimization value. The practical upshot is that processes like order-to-shipment, where an order must be shipped with all its products and the shipment mode depends on numeric attributes and aggregation guards, can be checked against event logs automatically.","feed_headline":"SMT formula finds optimal alignments for object-and-data-aware nets","feed_subtitle":"A new Petri net variant pairs object identities with prices, strings, and all-items-must-ship logic, checkable by SMT.","key_machinery":"The mechanism that carries the argument is the =-template inscription, a list variable annotated with '=' that, when used on an input arc, requires every token in the place matching the inscription's non-list components to be consumed in the same firing; this is what implements exact synchronization and wholeplace-like operations over a correlation set. In the SMT encoding, the corresponding constraint is the $synced(p, t_l, j)$ formula, which forces the total number of tokens in place $p$ at the previous marking to equal the number of objects used to instantiate the list variable. Around that core sit the variables inherited from the OPID encoding—transition variables $T_j$, marking variables $M_{j,p,o}$, object variables $O_{j,k}$, and distance variables $\\delta_{i,j}$—augmented with data inscription variables $D_{i,x}$ and data store variables $S_{i,p,o,l}$ to handle attribute values, plus the constraints $\\varphi_{init}$ through $\\varphi_{guard}$ that fix initial and final markings, token movement, freshness of $\\nu$-variables, and guard satisfaction, and the Lemma 1 bound on the number of moves and objects that makes the encoding finite.","core_discovery":"The central claim is that DOPIDs are not just an expressive modelling language but a computationally manageable one. The paper defines tokens that carry object identifiers together with data values, arc inscriptions that may match one object, a list of objects, or (when annotated with =) all objects matching a pattern, and transition guards built from arithmetic, strings, uninterpreted functions, and aggregation such as sum, min, max, and mean over lists. It then shows that the conformance checking problem for DOPIDs reduces to satisfiability modulo theories: a finite SMT formula $\\Phi$ encodes the existence of a model run together with an alignment between that run and the event log's trace graph, and the minimal value of the distance variable $\\delta_{m,n}$ equals the cost of an optimal alignment. Theorem 1 states that from any satisfying assignment one can decode a run of the net and an alignment whose cost is exactly $\\alpha(\\delta_{m,n})$. In the author's terms, this makes DOPIDs the first PNID-based formalism to support structured data and exact synchronization while still offering a conformance checking algorithm.","pith_inferences":["The $synced$ equation's reliance on total token count suggests a concrete repair: quantify over tokens whose non-list components match the binding before counting, which would extend Theorem 1 to markings with multiple parents; this is testable by modifying the encoding.","If the equation is left as is, practitioners must either keep correlation places partitioned per parent object or accept token renaming, which changes the semantics of exact synchronization; the paper does not spell out this restriction.","The same SMT variable scheme could support automated discovery of DOPIDs from logs, since the encoding already exposes object and data flow structure as constraints.","The cost model counts every differing attribute equally; a natural extension, not considered here, is to weight attribute mismatches by data type or business relevance."],"forward_implications":["DOPIDs subsume OPIDs, Data Petri Nets, and synchronous proclets, so a single SMT-based approach can now handle conformance for all three classes.","Exact synchronization patterns—such as an order shipping only when every product in it has been picked—can be checked automatically against object-centric logs.","Aggregation guards (sum, min, max, mean) over object attributes are expressible and decidable in the alignment setting.","The decoded alignment is provably optimal with cost $\\alpha(\\delta_{m,n})$, so the SMT optimization value is a true conformance cost, not an approximation.","A proof-of-concept implementation handles the running example's scale in under one second."],"supporting_citations":[{"why":"Supplies the OPID conformance encoding, the Lemma 1 bound on alignment size, and the alignment framework that DOPIDs extend.","marker":"[19]"},{"why":"Supplies the SMT treatment of data-aware guards and aggregation for Data Petri Nets that the DOPID encoding lifts.","marker":"[13]"},{"why":"Defines synchronous proclets whose exact synchronization semantics DOPIDs generalize via correlation places.","marker":"[12]"},{"why":"Introduces object-centric Petri nets and the trace-graph and object-graph notions reused for event logs.","marker":"[4]"},{"why":"Defines object-centric alignments and the cost function that the paper extends with data-mismatch costs.","marker":"[25]"},{"why":"The extended version of this paper containing the full details of the SMT encoding referenced in the main body.","marker":"[20]"}],"fun_headline_variants":["Data-aware object Petri nets with exact sync, checked via SMT","Object-and-data-aware nets: SMT for optimal alignments","DOPIDs: Petri nets with data and sync, solvable by SMT","SMT conformance checking for object-centric nets with data"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The encoding's synchronization constraint assumes that when a transition consumes 'all matching tokens,' the number of tokens in the place can be equated with the number of objects bound to the list variable; that equation also counts tokens that do not match the inscription, so the encoding only works if the place holds tokens for exactly one parent object at a time.","fun_headline_variants_meta":{"raw":{"variants":["Data-aware object Petri nets with exact sync, checked via SMT","Object-and-data-aware nets: SMT for optimal alignments","DOPIDs: Petri nets with data and sync, solvable by SMT","SMT conformance checking for object-centric nets with data"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000303,"raw_usage":{"total_tokens":1738,"prompt_tokens":933,"completion_tokens":805,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":549,"completion_tokens_details":{"reasoning_tokens":730}},"tokens_in":549,"tokens_out":805,"duration_ms":7012,"temperature":1.0,"reasoning_tokens":730,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-07T15:18:23.390460+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Exhibit a DOPID and event log where a correlation place holds tokens for two distinct parent objects, an =-inscription on a transition consumes only one parent's tokens, and a valid optimal alignment exists; if the SMT formula is unsatisfiable or forces extra model moves under those conditions, the encoding's $synced$ equation fails to enforce the paper's Definition 6, which requires consuming all matching tokens rather than all tokens.","supporting_citations":[{"cited_title":"In: Proc","cited_arxiv_id":null,"evidence_quote":"Supplies the OPID conformance encoding, the Lemma 1 bound on alignment size, and the alignment framework that DOPIDs extend."},{"cited_title":"In: Proc","cited_arxiv_id":null,"evidence_quote":"Defines synchronous proclets whose exact synchronization semantics DOPIDs generalize via correlation places."},{"cited_title":"In: Proc","cited_arxiv_id":null,"evidence_quote":"Defines object-centric alignments and the cost function that the paper extends with data-mismatch costs."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"The extended version of this paper containing the full details of the SMT encoding referenced in the main body."}],"review_version":1}