Pith. sign in

REVIEW 4 major objections 6 minor 35 references

Object-centric Processes with Structured Data and Exact Synchronization (Extended Version)

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

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read 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…

desk verdict 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. read the letter →

arxiv 2505.15409 v1 pith:FQIVUVJ2 submitted 2025-05-21 cs.MA

Alessandro Gianola , Marco Montali , Sarah Winkler This is my paper · ORCID
classification cs.MA
keywords DOPIDobject-centricprocessesconformancecheckingexactsynchronizationstructureddataPetrinetswithidentifiersSMTalignment
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 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.

What carries the argument

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.

What would settle it

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.

Watch

Extended reading notes

Core claim

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.

Load-bearing premise

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.

Editorial extensions

If this is right

  • 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.

Reading between the lines

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

  • 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.
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 / 6 minor

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.

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 (4)
  1. [Appendix A, φ_move / synced] 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.
  2. [Appendix A, Theorem 1 proof] 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.
  3. [Appendix A, variables (f)–(g) and φ_guard] 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.
  4. [Appendix A, Lemma 1] 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.
minor comments (6)
  1. [Section 4, after Definition 4] 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.
  2. [Appendix A, synced definition] 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.
  3. [Section 5, SMT encoding paragraph] 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.
  4. [References [19][20]] 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.
  5. [Example 6] 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.
  6. [Definition 9] 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].

Circularity Check

0 steps flagged · score 1.0 of 10

No significant circularity: the SMT encoding is a direct reduction, and Theorem 1 is an internal edit-distance optimality proof. The main caveat is reliance on the authors' prior Lemma 1, a support gap rather than a circular derivation.

full rationale

Walking the derivation chain: the paper fixes DOPID semantics in Definitions 4-7, then builds an SMT formula whose constraints (phi_init, phi_fin, phi_move, phi_rem, phi_type, phi_fresh, phi_guard, phi_delta) directly encode initial/final markings, enablement, token flow, typing, freshness, guards, and the Definition 10 cost. Lemma 2 verifies that a satisfying assignment decodes to a run, and Theorem 1 shows the decoded graph is an optimal alignment by induction on the same edit-distance recurrence used to define delta_{m,n}. This is a standard reduction/verification argument, not a definitional equivalence: the recurrence is derived from Definition 10, and the penalty expressions [PL], [PM], and [P=] are defined independently from events, transition labels, and object counts. No fitted parameter is renamed as a prediction, and no external benchmark is used to tune the model. The main self-citation is Lemma 1, imported from the same authors' OPIDs paper [19], with the assertion that data and exact synchronization 'do not affect the reasoning of that proof'; this is an unverified transfer and hence a support gap, and Section 5 defers details to the self-archived [20]. These are citation-reliance concerns, not circular steps: the central claim that satisfying assignments correspond to optimal alignments is not equivalent to its assumptions. The synced(p,tl,j) cardinality equation is a possible mis-encoding of Definition 6's maximality condition, since it counts all tokens in a place rather than only tokens matching the non-list components; that would be a soundness/completeness bug in Theorem 1, i.e., a correctness risk rather than circularity. Score 1 reflects the modest self-citation reliance, not a circular derivation.

Assumptions & free parameters 0 free parameters · 5 assumptions · 0 invented entities

This is a theoretical model paper, not an empirical one, so there are no fitted parameters. The main load-bearing assumptions are the transfer of the alignment-size bound from prior work and the correctness of the SMT encoding of all-matching-token consumption.

assumptions (5)
  • domain assumption Object id domains are uninterpreted and equality-comparable only.
    Section 3 and Definition 4; standard in the PNID literature.
  • domain assumption For every nu variable, dom(type(nu)) is infinite, providing unbounded supply of fresh objects.
    Section 4, paragraph before Definition 2; inherited from [31].
  • ad hoc to paper Lemma 1 from [19] bounding optimal alignment size holds for DOPIDs.
    Appendix A, Lemma 1; asserted without a transfer proof despite the new data and synchronization features.
  • domain assumption SMT solvers natively support arithmetic, uninterpreted functions, and aggregation functions.
    Section 5, item (7) on guards; relies on solver capabilities of Yices 2.
  • ad hoc to paper The encoding of synced(p,tl,j) correctly implements Definition 6's all-matching-tokens semantics.
    Appendix A, item (3); as written it counts all tokens in a place, not only matching tokens.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Object-centric Processes with Structured Data and Exact Synchronization (Extended Version)." pith.science (2026). https://pith.science/paper/FQIVUVJ2

@misc{pith2026250515409,
  author       = {Pith},
  title        = {Pith review of: Object-centric Processes with Structured Data and Exact Synchronization (Extended Version)},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/FQIVUVJ2}},
  note         = {Machine review of arXiv:2505.15409}
}
read the original abstract

Real-world processes often involve interdependent objects that also carry data values, such as integers, reals, or strings. However, existing process formalisms fall short to combine key modeling features, such as tracking object identities, supporting complex datatypes, handling dependencies among them, and object-aware synchronization. Object-centric Petri nets with identifiers (OPIDs) partially address these needs but treat objects as unstructured identifiers (e.g., order and item IDs), overlooking the rich semantics of complex data values (e.g., item prices or other attributes). To overcome these limitations, we introduce data-aware OPIDs (DOPIDs), a framework that strictly extends OPIDs by incorporating structured data manipulation capabilities, and full synchronization mechanisms. In spite of the expressiveness of the model, we show that it can be made operational: Specifically, we define a novel conformance checking approach leveraging satisfiability modulo theories (SMT) to compute data-aware object-centric alignments.

Figures

Figures reproduced from arXiv: 2505.15409 by the authors.

Figure 1
Figure 1. DOPID of an order-to-ship process. As a well-formedness condition, we assume that in Fin one can only use only simple, ⊆-template and =-template inscriptions, while in Fout one can only use simple and transfer-template inscriptions (cf. Def. 2). For a DOPID N as in Def. 4, we also use the common notations for presets •t = {p | (p, t) ∈ dom(Fin)} and postsets t• = {p | (t, p) ∈ dom(Fout)}. Simple flows (i.e., flows w… view at source ↗

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

35 extracted references · 30 canonical work pages

  1. [19]

    In: Proc

    Gianola, A., Montali, M., Winkler, S.: Object-centric conformance alignments with synchronization. In: Proc. 36th CAiSE. LNCS, vol. 14663, pp. 3–19 (2024). https: //doi.org/10.1007/978-3-031-61057-8_1

    work page doi:10.1007/978-3-031-61057-8_1 2024

  2. [20]

    Gianola, A., Montali, M., Winkler, S.: Object-centric processes with structured data and universal synchronization (extended version) (2024), available from https: //www.inf.unibz.it/montali/papers/dopid-long-version.pdf

    work page 2024

  3. [1]

    In: Proc

    van der Aalst, W.M.P.: Object-centric process mining: Dealing with divergence and convergence in event data. In: Proc. 17th SEFM (2019). https://doi.org/10. 1007/978-3-030-30446-1_1

    work page 2019

  4. [2]

    In: Proc

    van der Aalst, W.M.P.: Toward more realistic simulation models using object- centric process mining. In: Proc. 37th ECMS. pp. 5–13 (2023). https://doi.org/10. 7148/2023-0005, https://doi.org/10.7148/2023-0005

    work page doi:10.7148/2023-0005 2023

  5. [3]

    In: Joint Work- shop Proc

    van der Aalst, W.M.P.: Twin transitions powered by event data - using object- centric process mining to make processes digital and sustainable. In: Joint Work- shop Proc. ATAED/PN4TT (2023)

    work page 2023

  6. [4]

    van der Aalst, W.M.P., Berti, A.: Discovering object-centric Petri nets. Fundam. Informaticae175(1-4), 1–40 (2020). https://doi.org/10.3233/FI-2020-1946

    doi:10.3233/fi-2020-1946 2020

  7. [5]

    Data Knowl

    van der Aalst, W.M.P., Weske, M., Grünbauer, D.: Case handling: a new paradigm for business process support. Data Knowl. Eng.53(2), 129–162 (2005). https:// doi.org/10.1016/J.DATAK.2004.07.003

    work page doi:10.1016/j.datak.2004.07.003 2005

  8. [6]

    Advancements and Challenges in Object-Centric Process Mining: A Systematic Literature Review

    Berti, A., Montali, M., van der Aalst, W.M.P.: Advancements and chal- lenges in object-centric process mining: A systematic literature review. CoRR abs/2311.08795(2023). https://doi.org/10.48550/ARXIV.2311.08795

    work page Pith review arXiv doi:10.48550/arxiv.2311.08795 2023

Show all 35 references
  1. [7]

    Computing103(1), 29–50 (2021)

    Boltenhagen, M., Chatain, T., Carmona, J.: Optimized SAT encoding of confor- mance checking artefacts. Computing103(1), 29–50 (2021)

    2021

  2. [8]

    In: Proc

    Breitmayer, M., Arnold, L., Pejic, M., Reichert, M.: Transforming object-centric process models into BPMN 2.0 models in the PHILharmonicFlows framework. In: Proc. Modellierung 2024. LNI, vol. P-348, pp. 83–98 (2024). https://doi.org/10. 18420/MODELLIERUNG2024_009

    2024

  3. [9]

    In: Proc

    Calvanese, D., Ghilardi, S., Gianola, A., Montali, M., Rivkin, A.: Formal mod- eling and SMT-based parameterized verification of data-aware BPMN. In: Proc. of BPM 2019. LNCS, vol. 11675, pp. 157–175 (2019), https://doi.org/10.1007/ 978-3-030-26619-6_12

    2019

  4. [10]

    IEEE Data Eng

    Cohn, D., Hull, R.: Business artifacts: A data-centric approach to modeling busi- ness operations and processes. IEEE Data Eng. Bull.32(3), 3–9 (2009)

    2009

  5. [11]

    In: Proc

    Damaggio, E., Deutsch, A., Hull, R., Vianu, V.: Automatic verification of data- centric business processes. In: Proc. of BPM 2011. LNCS, vol. 6896, pp. 3–16 (2011). https://doi.org/10.1007/978-3-642-23059-2_3

    2011 doi

  6. [12]

    In: Proc

    Fahland, D.: Describing behavior of processes with many-to-many interactions. In: Proc. PETRI NETS (2019). https://doi.org/10.1007/978-3-030-21571-2_1 Object-centric processes with structured data and exact synchronization 17

    2019 doi

  7. [13]

    Felli,P.,Gianola,A.,Montali,M.,Rivkin,A.,Winkler,S.:Data-awareconformance checking with SMT. Inf. Syst.117, 102230 (2023). https://doi.org/10.1016/J.IS. 2023.102230

    2023

  8. [14]

    Felli, P., Gianola, A., Montali, M., Rivkin, A., Winkler, S.: Multi-perspective con- formance checking of uncertain process traces: An SMT-based approach. Eng. Appl. Artif. Intell.126, 106895 (2023). https://doi.org/10.1016/J.ENGAPPAI. 2023.106895, https://doi.org/10.1016/j.en...

    2023

  9. [15]

    Felli, P., de Leoni, M., Montali, M.: Soundness verification of data-aware process models with variable-to-variable conditions. Fundam. Informaticae182(1), 1–29 (2021). https://doi.org/10.3233/FI-2021-2064

    2021 doi

  10. [16]

    In: Proc

    Ghilardi, S., Gianola, A., Montali, M., Rivkin, A.: Delta-BPMN: A concrete lan- guage and verifier for data-aware BPMN. In: Proc. of BPM 2021. Lecture Notes in Computer Science, vol. 12875, pp. 179–196. Springer (2021). https://doi.org/10. 1007/978-3-030-85469-0_13, https://do...

    2021 doi

  11. [17]

    Ghilardi, S., Gianola, A., Montali, M., Rivkin, A.: Petri net-based object-centric processes with read-only data. Inf. Syst.107, 102011 (2022). https://doi.org/10. 1016/J.IS.2022.102011

    2022

  12. [18]

    Gianola, A.: Verification of Data-Aware Processes via Satisfiability Modulo Theo- ries, Lecture Notes in Business Information Processing, vol. 470. Springer (2023). https://doi.org/10.1007/978-3-031-42746-6

    2023 doi

  13. [21]

    In: La Rosa, M., Sadiq, S., Teniente, E

    Haarmann, S., Montali, M., Weske, M.: Refining case models using cardinality constraints. In: La Rosa, M., Sadiq, S., Teniente, E. (eds.) Proc. 33rd CAiSE. pp. 296–310 (2021). https://doi.org/10.1007/978-3-030-79382-1_18

    2021 doi

  14. [22]

    In: Proc

    Hewelt, M., Weske, M.: A hybrid approach for flexible case modeling and execution. In: Proc. Business Process Management Forum. LNBIP, vol. 260, pp. 38–54 (2016). https://doi.org/10.1007/978-3-319-45468-9_3

    2016 doi

  15. [23]

    Künzle, V., Reichert, M.: PHILharmonicFlows: towards a framework for object- aware process management. J. Softw. Maintenance Res. Pract.23(4), 205–244 (2011). https://doi.org/10.1002/SMR.524, https://doi.org/10.1002/smr.524

    2011 doi

  16. [24]

    de Leoni, M., Felli, P., Montali, M.: A holistic approach for soundness verification of decision-aware process models. In: ER. LNCS, vol. 11157, pp. 219–235 (2018). https://doi.org/10.1007/978-3-030-00847-5_17

    2018 doi

  17. [25]

    In: Proc

    Liss, L., Adams, J.N., van der Aalst, W.M.P.: Object-centric alignments. In: Proc. ER (2023). https://doi.org/10.1007/978-3-031-47262-6_11

    2023 doi

  18. [26]

    In: Service-Oriented Com- puting

    Lohmann, N., Wolf, K.: Artifact-centric choreographies. In: Service-Oriented Com- puting. pp. 32–46 (2010). https://doi.org/10.1007/978-3-642-17358-5_3

    2010 doi

  19. [27]

    Computing98(4), 407–437 (2016)

    Mannhardt,F.,deLeoni,M.,Reijers,H.A.,vanderAalst,W.M.P.:Balancedmulti- perspective checking of process conformance. Computing98(4), 407–437 (2016). https://doi.org/10.1007/S00607-015-0441-1

    2016 doi

  20. [28]

    Montali, M., Calvanese, D.: Soundness of data-aware, case-centric processes. Int. J. Softw. Tools Technol. Transf.18(5), 535–558 (2016). https://doi.org/10.1007/ S10009-016-0417-2

    2016

  21. [29]

    Montali, M., Rivkin, A.: DB-Nets: on the marriage of colored petri nets and re- lational databases. Trans. Petri Nets Other Model. Concurr.12, 91–118 (2017). https://doi.org/10.1007/978-3-662-55862-1_5 18 A. Gianola et al

    2017 doi

  22. [30]

    In: Proc

    Polyvyanyy, A., van der Werf, J.M.E.M., Overbeek, S., Brouwers, R.: Information systems modeling: Language, verification, and tool support. In: Proc. 31st CAiSE (2019). https://doi.org/10.1007/978-3-030-21290-2_13

    2019 doi

  23. [31]

    Rosa-Velardo, F., de Frutos-Escrig, D.: Decidability problems in Petri nets with names and replication. Fundam. Informaticae105(3), 291–317 (2010). https://doi. org/10.3233/FI-2010-368

    2010 doi

  24. [32]

    Snoeck, M., Verbruggen, C., Smedt, J.D., Weerdt, J.D.: Supporting data-aware processes with MERODE. Softw. Syst. Model.22(6), 1779–1802 (2023). https: //doi.org/10.1007/S10270-023-01095-4

    2023 doi

  25. [33]

    In: Proc

    Sommers, D., Sidorova, N., van Dongen, B.: Aligning event logs to resource-con- strainedν-petri nets. In: Proc. 43rdPETRINETS. LNCS, vol. 13288, pp. 325–345 (2022). https://doi.org/10.1007/978-3-031-06653-5_17

    2022 doi

  26. [34]

    In: Proc

    TerryHeathIII,F.F.,Boaz,D.,Gupta,M.,Vaculín,R.,Sun,Y.,Hull,R.,Limonad, L.: Barcelona: A design and runtime environment for declarative artifact-centric BPM. In: Proc. 11th ICSOC. LNCS, vol. 8274, pp. 705–709 (2013). https://doi. org/10.1007/978-3-642-45005-1_65

    2013 doi

  27. [35]

    https://doi.org/10.1007/978-3-031-06653-5_19 A Encoding We detail the encoding outlined in the main body of the paper

    van der Werf, J.M.E.M., Rivkin, A., Polyvyanyy, A., Montali, M.: Data and process resonance-identifiersoundnessformodelsofinformationsystems.In:Proc.PETRI NETS (2022). https://doi.org/10.1007/978-3-031-06653-5_19 A Encoding We detail the encoding outlined in the main body of t...

    2022 doi

Pith tools

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