pith. sign in

arxiv: 2212.07363 · v6 · submitted 2022-12-14 · 💻 cs.FL

Correctness Notions for Petri Nets with Identifiers

Jan Martijn E. M. van der Werf , Andrey Rivkin , Marco Montali , Artem Polyvyanyy This is my paper

Pith reviewed 2026-05-24 10:39 UTC · model grok-4.3

classification 💻 cs.FL
keywords Petri netsidentifierscorrectness criteriasoundnessinformation systemsworkflow modelsdecidabilityobject-aware systems
0
0 comments X

The pith

Petri nets with identifiers support new correctness criteria that generalize classical soundness to verify object- and resource-aware information systems.

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

The paper equips standard Petri nets with tokens that carry identifiers for distinct object instances of predefined types, treating resources as instances of special object types. It then defines several correctness criteria for the resulting models that check not only control flow but also proper creation, manipulation, and deletion of objects alongside resource usage. These criteria are presented as direct generalizations of the classical soundness property used for workflow nets. The work includes analysis of decidability for restricted but interesting classes of such nets. A reader would care because information systems routinely track multiple object instances and resources, so control-flow-only checks are insufficient for reliable verification.

Core claim

The paper claims that correctness notions for information systems can be obtained by lifting the soundness property of workflow nets to Petri nets whose tokens are labeled with identifiers; the new criteria ensure that every object instance is properly created and terminated, every resource is acquired and released correctly, and the overall process reaches completion without deadlocks or leaks, while decidability holds for bounded or acyclic subclasses.

What carries the argument

Petri nets with identifiers, in which each token carries an identifier naming a specific instance of a predefined object type and resources appear as instances of distinguished resource types.

If this is right

  • Verification tools can check object creation, usage, and termination in addition to control-flow soundness.
  • Decidability results apply directly to restricted but practically relevant classes such as acyclic or bounded nets with identifiers.
  • Resource acquisition and release become part of the same correctness check as process termination.
  • The criteria remain compositional with respect to object types, allowing modular verification when new object types are added.

Where Pith is reading between the lines

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

  • The same identifier mechanism could be used to encode database keys or case identifiers in business-process models.
  • Integration with existing soundness-checking algorithms for ordinary workflow nets would require only an additional identifier-tracking layer.
  • Real-world case studies on ERP or CRM systems could test whether the criteria catch bugs missed by control-flow-only checks.
  • Relaxing the fixed-type assumption to allow dynamic object-type creation would require new decidability arguments.

Load-bearing premise

Information-system states and behavior can be faithfully represented by Petri nets whose tokens carry identifiers for object instances of fixed types.

What would settle it

An information-system model whose execution trace violates one of the proposed criteria yet satisfies every intuitive correctness requirement, or a bounded net family for which one of the criteria is shown to be undecidable.

Figures

Figures reproduced from arXiv: 2212.07363 by Andrey Rivkin, Artem Polyvyanyy, Jan Martijn E. M. van der Werf, Marco Montali.

Figure 1
Figure 1. Figure 1: The life cycles of products, customers and orders in the retail shop. [PITH_FULL_IMAGE:figures/full_fig_p005_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: t-PNID Nrs for a retail shop that manipulates products, customers and orders. Each place is colored according to its type. Place p carries pairs of identifiers: an order and a customer [PITH_FULL_IMAGE:figures/full_fig_p006_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Type projections of Figure 2. The customer projection is not sound, as place [PITH_FULL_IMAGE:figures/full_fig_p011_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: A transition-bordered WF-Net (a) and its closure (b) [15]. [PITH_FULL_IMAGE:figures/full_fig_p011_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: Simulation of a Minksy 2-counter machine via t-PNIDs. Here, qi , qk and ql correspond to control states of the machine. 3Notice that transitions of net components simulating instructions with dec, according to Definition 3.4, are also col￾lectors for λ [PITH_FULL_IMAGE:figures/full_fig_p014_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: Two t-PNIDs. Net N1 is identifier sound, whereas net N2 is not identifier sound. The underlying idea of identifier soundness is that each type projection should behave well, i.e., each type projection should be sound. Consider in t-PNID Nrs of [PITH_FULL_IMAGE:figures/full_fig_p015_6.png] view at source ↗
Figure 7
Figure 7. Figure 7: EC-closure of a WF-net N. 5.1. EC-closed workflow nets WF-nets are widely used to model business processes. The initial place of the WF-net signifies the start of a case, the final place represents the goal state, i.e., the process case completion. A firing sequence from initial state to final state represents the activities that are performed for a single case. Thus, a WF-net describes all possible sequen… view at source ↗
Figure 8
Figure 8. Figure 8: Construction rules of the typed Jackson Nets. [PITH_FULL_IMAGE:figures/full_fig_p022_8.png] view at source ↗
Figure 9
Figure 9. Figure 9: The example of the retailer shop as a typed Jackson Net. [PITH_FULL_IMAGE:figures/full_fig_p031_9.png] view at source ↗
Figure 10
Figure 10. Figure 10: Several intermediate steps while creating the typed Jackson Net of Fig. 9. [PITH_FULL_IMAGE:figures/full_fig_p031_10.png] view at source ↗
Figure 11
Figure 11. Figure 11: Three examples of resource-aware t-PNIDs. Nets (a) and (b) are not managing resources [PITH_FULL_IMAGE:figures/full_fig_p036_11.png] view at source ↗
Figure 12
Figure 12. Figure 12: An identifier-sound t-PNID and two alternative resource closures [PITH_FULL_IMAGE:figures/full_fig_p039_12.png] view at source ↗
Figure 13
Figure 13. Figure 13: An identifier-unsound t-PNID and one of its resource closures [PITH_FULL_IMAGE:figures/full_fig_p040_13.png] view at source ↗
read the original abstract

A model of an information system describes its processes and how resources are involved in these processes to manipulate data objects. This paper presents an extension to the Petri nets formalism suitable for describing information systems in which states refer to object instances of predefined types and resources are identified as instances of special object types. Several correctness criteria for resource- and object-aware information systems models are proposed, supplemented with discussions on their decidability for interesting classes of systems. These new correctness criteria can be seen as generalizations of the classical soundness property of workflow models concerned with process control flow correctness.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 3 minor

Summary. The manuscript introduces Petri nets with identifiers (PNIDs), an extension of classical Petri nets in which tokens carry identifiers for object instances of predefined types and resources are modeled as instances of special object types. It defines several correctness criteria that generalize the classical soundness property of workflow nets (concerned with control-flow correctness) to resource- and object-aware information systems, and discusses decidability of these criteria for interesting classes of systems.

Significance. If the definitions are internally consistent and the decidability results hold, the work provides a principled way to lift soundness-style verification from pure control-flow models to data- and resource-aware settings common in information systems. The explicit generalization of an established property and the focus on decidability for restricted classes are strengths that could support tool development in business-process verification.

minor comments (3)
  1. [Abstract] The abstract states that 'several correctness criteria' are proposed but does not name them; a short enumeration in the abstract or introduction would improve readability.
  2. [§2–3] Notation for identifier types, resource types, and the transition firing rule with identifier substitution is introduced without an early running example; adding a small illustrative net (e.g., in §2 or §3) would help readers follow subsequent definitions.
  3. [§5] The decidability statements refer to 'interesting classes of systems' without a compact summary table listing the classes, the criteria, and the complexity results; such a table would make the contribution easier to survey.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive summary of our manuscript and the recommendation of minor revision. No specific major comments were provided in the report, so we have no points to address point-by-point at this stage. We will incorporate any minor suggestions during revision.

Circularity Check

0 steps flagged

No significant circularity identified

full rationale

The paper proposes definitional extensions to Petri nets (tokens with identifiers, resources as special object types) and new correctness criteria that generalize classical soundness, along with decidability results for classes of systems. No equations, fitted parameters, predictions, or self-citations appear that reduce any claimed result to its own inputs by construction. The contribution consists of explicit definitions and complexity statements that stand independently of any internal reduction or self-referential premise.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 1 invented entities

The central claim rests on the standard theory of Petri nets plus the modeling adequacy of the identifier extension; no numerical parameters are mentioned.

axioms (1)
  • standard math Standard firing semantics and reachability for Petri nets
    Invoked as the base formalism on which the identifier extension is built.
invented entities (1)
  • Petri nets with identifiers no independent evidence
    purpose: To represent object instances and identified resources in information-system models
    The extension is introduced by the paper itself; no independent evidence outside the proposal is supplied in the abstract.

pith-pipeline@v0.9.0 · 5624 in / 1262 out tokens · 28860 ms · 2026-05-24T10:39:38.064913+00:00 · methodology

discussion (0)

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

Lean theorems connected to this paper

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

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

Reference graph

Works this paper leans on

52 extracted references · 52 canonical work pages

  1. [1]

    Understanding Petri Nets – Modeling Techniques, Analysis Methods, Case Studies

    Reisig W. Understanding Petri Nets – Modeling Techniques, Analysis Methods, Case Studies. Springer Berlin Heidelberg, 2013. ISBN 978-3-642-33277-7. doi:10.1007/978-3-642-33278-4

    work page doi:10.1007/978-3-642-33278-4 2013

  2. [2]

    Generation of Database Transactions with Petri Nets

    van Hee KM, Sidorova N, V oorhoeve M, van der Werf JMEM. Generation of Database Transactions with Petri Nets. Fundam. Inform., 2009. 93(1-3):171–184

    work page 2009

  3. [3]

    Parallel Program Schemata

    Karp RM, Miller RE. Parallel Program Schemata. J. Comput. Syst. Sci. , 1969. 3(2):147–195. doi: 10.1016/S0022-0000(69)80011-5

    work page doi:10.1016/s0022-0000(69)80011-5 1969

  4. [4]

    The Recursive Equivalence of the Reachability Problem and the Liveness Problem for Petri Nets and Vector Addition Systems

    Hack M. The Recursive Equivalence of the Reachability Problem and the Liveness Problem for Petri Nets and Vector Addition Systems. In: Proc. of SW AT 1974. IEEE Computer Society, 1974 pp. 156–164. doi:10.1109/SW AT.1974.28

    work page doi:10.1109/sw 1974

  5. [5]

    Transition Systems of Elementa ry Net Systems with Inhibitor Arcs

    van der Aalst WMP. Verification of Workflow Nets. In: Proc. of Petri Nets, volume 1248 of LNCS. Springer, 1997 pp. 407–426. doi:10.1007/3-540-63139-9 \ 48

    work page doi:10.1007/3-540-63139-9 1997

  6. [6]

    Information Systems Modeling: Language, Verification, and Tool Support

    Polyvyanyy A, van der Werf JMEM, Overbeek S, Brouwers R. Information Systems Modeling: Language, Verification, and Tool Support. In: Proc. of CAiSE 2019, volume 11483 ofLNCS. Springer, 2019 pp. 194–

    work page 2019

  7. [7]

    doi:10.1007/978-3-030-21290-2 \ 13

    work page doi:10.1007/978-3-030-21290-2

  8. [8]

    The Information Systems Modeling Suite - Modeling the Interplay Between Information and Processes

    van der Werf JMEM, Polyvyanyy A. The Information Systems Modeling Suite - Modeling the Interplay Between Information and Processes. In: Proc. of Petri Nets 2020, volume 12152 of LNCS. Springer, 2020 pp. 414–425. doi:10.1007/978-3-030-51831-8 22

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

  9. [9]

    An Assignment on Information System Modeling - On Teaching Data and Process Integration

    van der Werf JMEM, Polyvyanyy A. An Assignment on Information System Modeling - On Teaching Data and Process Integration. In: Business Process Management Workshops, volume 342 of LNBIP. Springer, 2018 pp. 553–566. doi:10.1007/978-3-030-11641-5 \ 44

    work page doi:10.1007/978-3-030-11641-5 2018

  10. [10]

    The Linear Time - Branching Time Spectrum II: The Semantics of Sequential Systems with Silent Moves

    Glabbeek R. The Linear Time - Branching Time Spectrum II: The Semantics of Sequential Systems with Silent Moves. In: CONCUR 1993, volume 715 of LNCS. Springer, 1993 pp. 66–81

    work page 1993

  11. [11]

    Soundness and Separability of Workflow Nets in the Stepwise Refinement Approach

    van Hee KM, Sidorova N, V oorhoeve M. Soundness and Separability of Workflow Nets in the Stepwise Refinement Approach. In: Proc. of Petri Nets 2003, volume 2679 of LNCS. Springer, 2003 pp. 337–356. doi:10.1007/3-540-44919-1 22

    work page doi:10.1007/3-540-44919-1 2003

  12. [12]

    Describing Behavior of Processes with Many-to-Many Interactions

    Fahland D. Describing Behavior of Processes with Many-to-Many Interactions. In: Proc. of Petri Nets

    work page

  13. [13]

    Springer, 2019 pp. 3–24. doi:10.1007/978-3-030-21571-2 1

    work page doi:10.1007/978-3-030-21571-2 2019

  14. [14]

    Decidability and complexity of Petri nets with unordered data.Theor

    Rosa-Velardo F, de Frutos-Escrig D. Decidability and complexity of Petri nets with unordered data.Theor. Comput. Sci., 2011. 412(34):4439–4451. doi:10.1016/j.tcs.2011.05.007. Van der Werf et al./ Correctness Notions for Petri Nets with Identifiers 205

    work page doi:10.1016/j.tcs.2011.05.007 2011

  15. [15]

    Mobile Synchronizing Petri Nets: A Choreographic Ap- proach for Coordination in Ubiquitous Systems

    Rosa-Velardo F, Alonso OM, de Frutos-Escrig D. Mobile Synchronizing Petri Nets: A Choreographic Ap- proach for Coordination in Ubiquitous Systems. Electron. Notes Theor. Comput. Sci., 2006. 150(1):103–

    work page 2006

  16. [16]

    URL https://doi.org/10.1016/j.entcs.2005.12.026

    doi:10.1016/j.entcs.2005.12.026. URL https://doi.org/10.1016/j.entcs.2005.12.026

    work page doi:10.1016/j.entcs.2005.12.026 2005

  17. [17]

    Forward Analysis for Petri Nets with Name Creation

    Rosa-Velardo F, de Frutos-Escrig D. Forward Analysis for Petri Nets with Name Creation. In: Ap- plications and Theory of Petri Nets, volume 6128 of LNCS. Springer, Berlin, 2010 pp. 185–205. doi:10.1007/978-3-642-13675-7 12

    work page doi:10.1007/978-3-642-13675-7 2010

  18. [18]

    Business Process Modeling Using Petri Nets.Trans

    van Hee KM, Sidorova N, van der Werf JMEM. Business Process Modeling Using Petri Nets.Trans. Petri Nets Other Model. Concurr., 2013. 7:116–161. doi:10.1007/978-3-642-38143-0 4

    work page doi:10.1007/978-3-642-38143-0 2013

  19. [20]

    Petri net-based object-centric processes with read-only data

    Ghilardi S, Gianola A, Montali M, Rivkin A. Petri net-based object-centric processes with read-only data. Inf. Syst., 2022. 107:102011. doi:10.1016/j.is.2022.102011

    work page doi:10.1016/j.is.2022.102011 2022

  20. [21]

    Decidability Border for Petri Nets with Data: WQO Dichotomy Conjecture

    Lasota S. Decidability Border for Petri Nets with Data: WQO Dichotomy Conjecture. In: Kordon F, Moldt D (eds.), Application and Theory of Petri Nets and Concurrency - 37th International Conference, PETRI NETS 2016, Toru´n, Poland, June 19-24, 2016. Proceedings, volume 9698 ofLNCS. Springer, 2016 pp. 20–36. doi:10.1007/978-3-319-39086-4 3

    work page doi:10.1007/978-3-319-39086-4 2016

  21. [22]

    Dynamic Soundness in Resource-Constrained Workflow Nets

    Martos-Salgado M, Rosa-Velardo F. Dynamic Soundness in Resource-Constrained Workflow Nets. In: Formal Techniques for Distributed Systems. FMOODS FORTE, volume 6722 of LNCS. Springer, 2011 pp. 259–273. doi:10.1007/978-3-642-21461-5 17

    work page doi:10.1007/978-3-642-21461-5 2011

  22. [24]

    First-order µ-calculus over generic transition systems and applications to the situation calculus

    Calvanese D, Giacomo GD, Montali M, Patrizi F. First-order µ-calculus over generic transition systems and applications to the situation calculus. Inf. Comput., 2018. 259(3):328–347. doi:10.1016/j.ic.2017.08. 007

    work page doi:10.1016/j.ic.2017.08 2018

  23. [25]

    Verification and Monitoring for First-Order LTL with Persistence-Preserving Quantification over Finite and Infinite Traces

    Calvanese D, Giacomo GD, Montali M, Patrizi F. Verification and Monitoring for First-Order LTL with Persistence-Preserving Quantification over Finite and Infinite Traces. In: Raedt LD (ed.), Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence, IJCAI 2022, Vienna, Austria, 23-29 July 2022. ijcai.org, 2022 pp. 2553–2560...

    work page doi:10.24963/ijcai.2022/354 2022

  24. [26]

    Verification of relational data-centric dy- namic systems with external services

    Hariri BB, Calvanese D, Giacomo GD, Deutsch A, Montali M. Verification of relational data-centric dy- namic systems with external services. In: Hull R, Fan W (eds.), Proceedings of the 32nd ACM SIGMOD- SIGACT-SIGART Symposium on Principles of Database Systems, PODS 2013, New York, NY , USA - June 22 - 27, 2013. ACM, 2013 pp. 163–174. doi:10.1145/2463664.2465221

    work page doi:10.1145/2463664.2465221 2013

  25. [27]

    Foundations of Databases

    Abiteboul S, Hull R, Vianu V . Foundations of Databases. Addison-Wesley, 1995. ISBN 0-201-53771-0

    work page 1995

  26. [28]

    Yasper: a tool for workflow modeling and analysis

    van Hee KM, Oanea O, Post R, Somers LJ, van der Werf JMEM. Yasper: a tool for workflow modeling and analysis. In: Proc. of ACSD 2006. IEEE, 2006 pp. 279–282. doi:10.1109/ACSD.2006.37

    work page doi:10.1109/acsd.2006.37 2006

  27. [29]

    Model checking Petri nets with names using data-centric dynamic systems

    Montali M, Rivkin A. Model checking Petri nets with names using data-centric dynamic systems. Formal Aspects Comput., 2016. 28(4):615–641. doi:10.1007/s00165-016-0370-6. URL https://doi.org/10. 1007/s00165-016-0370-6

    work page doi:10.1007/s00165-016-0370-6 2016

  28. [30]

    Discovering Block-Structured Process Models from Event Logs - A Constructive Approach

    Leemans SJJ, Fahland D, van der Aalst WMP. Discovering Block-Structured Process Models from Event Logs - A Constructive Approach. In: Proc. of Petri Nets 2013, volume 7927 of LNCS. Springer, 2013 pp. 311–329. doi:10.1007/978-3-642-38697-8 \ 17. 206 Van der Werf et al./ Correctness Notions for Petri Nets with Identifiers

    work page doi:10.1007/978-3-642-38697-8 2013

  29. [31]

    Causal Behavioural Profiles - Efficient Computation, Applications, and Evaluation.Fundam

    Weidlich M, Polyvyanyy A, Mendling J, Weske M. Causal Behavioural Profiles - Efficient Computation, Applications, and Evaluation.Fundam. Informaticae, 2011. 113(3-4):399–435. doi:10.3233/FI-2011-614

    work page doi:10.3233/fi-2011-614 2011

  30. [32]

    On the relationship between workflow models and document types

    van Hee KM, Hidders J, Houben GJ, Paredaens J, Thiran P. On the relationship between workflow models and document types. Information Systems, 2009. 34(1):178–208. doi:10.1016/j.is.2008.06.003

    work page doi:10.1016/j.is.2008.06.003 2009

  31. [33]

    Petri Nets: Properties, Analysis and Applications

    Murata T. Petri Nets: Properties, Analysis and Applications. Proceedings of the IEEE, 1989. 77(4):541– 580

    work page 1989

  32. [34]

    Verification de Reseaux de Petri

    Berthelot G. Verification de Reseaux de Petri. Ph.D. thesis, Universit´e Pierre et Marie Curie (Paris), 1978

    work page 1978

  33. [35]

    Resource-Constrained Workflow Nets

    van Hee KM, Sidorova N, V oorhoeve M. Resource-Constrained Workflow Nets. Fundam. Inform., 2006. 71(2-3):243–257

    work page 2006

  34. [36]

    Resource Bisimilarity in Petri Nets is Decidable

    Lomazova IA, Bashkin V A, Jancar P. Resource Bisimilarity in Petri Nets is Decidable. Fundam. Infor- maticae, 2022. 186(1-4):175–194. doi:10.3233/FI-222125

    work page doi:10.3233/fi-222125 2022

  35. [37]

    Inferring Unobserved Events in Systems with Shared Re- sources and Queues

    Fahland D, Denisov V , van der Aalst WMP. Inferring Unobserved Events in Systems with Shared Re- sources and Queues. Fundam. Informaticae, 2021. 183(3-4):203–242. doi:10.3233/FI-2021-2087

    work page doi:10.3233/fi-2021-2087 2021

  36. [38]

    Object-Centric Process Mining: Dealing with Divergence and Convergence in Event Data

    van der Aalst WMP. Object-Centric Process Mining: Dealing with Divergence and Convergence in Event Data. In: ¨Olveczky PC, Sala¨un G (eds.), Proc. of SEFM 2019, volume 11724 ofLecture Notes in Computer Science. Springer, 2019 pp. 3–25. doi:10.1007/978-3-030-30446-1 \ 1

    work page doi:10.1007/978-3-030-30446-1 2019

  37. [39]

    Modeling and Reasoning over Declarative Data- Aware Processes with Object-Centric Behavioral Constraints

    Artale A, Kovtunova A, Montali M, van der Aalst WMP. Modeling and Reasoning over Declarative Data- Aware Processes with Object-Centric Behavioral Constraints. In: Proc. of BPM 2019, volume 11675 of LNCS. Springer, 2019 pp. 139–156. doi:10.1007/978-3-030-26619-6 11

    work page doi:10.1007/978-3-030-26619-6 2019

  38. [40]

    Soundness of Data-Aware, Case-Centric Processes

    Montali M, Calvanese D. Soundness of Data-Aware, Case-Centric Processes. Int. Journal on Software Tools for Technology Transfer, 2016. doi:10.1007/s10009-016-0417-2

    work page doi:10.1007/s10009-016-0417-2 2016

  39. [41]

    Petri Nets with Parameterised Data - Modelling and Verifi- cation

    Ghilardi S, Gianola A, Montali M, Rivkin A. Petri Nets with Parameterised Data - Modelling and Verifi- cation. In: Fahland D, Ghidini C, Becker J, Dumas M (eds.), BPM’20, volume 12168 of LNCS. Springer, 2020 pp. 55–74. doi:10.1007/978-3-030-58666-9 \ 4

    work page doi:10.1007/978-3-030-58666-9 2020

  40. [42]

    State-Boundedness in Data-Aware Dynamic Systems

    Bagheri Hariri B, Calvanese D, Montali M, Deutsch A. State-Boundedness in Data-Aware Dynamic Systems. In: Proc. of KR 2014. AAAI Press, 2014

    work page 2014

  41. [43]

    Discovering Object-centric Petri Nets

    van der Aalst WMP, Berti A. Discovering Object-centric Petri Nets. Fundam. Informaticae, 2020. 175(1- 4):1–40. doi:10.3233/FI-2020-1946

    work page doi:10.3233/fi-2020-1946 2020

  42. [44]

    Soundness in Object-centric Workflow Petri Nets

    Lomazova IA, Mitsyuk AA, Rivkin A. Soundness in Object-centric Workflow Petri Nets. CoRR, 2021. abs/2112.14994

    work page arXiv 2021

  43. [45]

    In: Fodor, P., Montali, M., Calvanese, D., Roman, D

    de Leoni M, Felli P, Montali M. A Holistic Approach for Soundness Verification of Decision-Aware Process Models. In: ER, volume 11157 of LNCS. Springer, 2018 pp. 219–235. doi:10.1007/978-3-030- 00847-5 17

    work page doi:10.1007/978-3-030- 2018

  44. [46]

    Soundness Verification of Decision-Aware Process Models with Variable- to-Variable Conditions

    Felli P, de Leoni M, Montali M. Soundness Verification of Decision-Aware Process Models with Variable- to-Variable Conditions. In: Proc. of ACSD 2019. IEEE, 2019 pp. 82–91. doi:10.1109/ACSD.2019.00013

    work page doi:10.1109/acsd.2019.00013 2019

  45. [47]

    Strategy Synthesis for Data-Aware Dynamic Systems with Multiple Actors

    de Leoni M, Felli P, Montali M. Strategy Synthesis for Data-Aware Dynamic Systems with Multiple Actors. In: KR. 2020 pp. 315–325. doi:10.24963/kr.2020/32

    work page doi:10.24963/kr.2020/32 2020

  46. [48]

    Cross-Case Data Objects in Business Processes: Semantics and Analysis

    Haarmann S, Weske M. Cross-Case Data Objects in Business Processes: Semantics and Analysis. In: BPM (Forum), volume 392 of Lecture Notes in Business Information Processing . Springer, 2020 pp. 3–

    work page 2020

  47. [49]

    Van der Werf et al./ Correctness Notions for Petri Nets with Identifiers 207

    doi:10.1007/978-3-030-58638-6 1. Van der Werf et al./ Correctness Notions for Petri Nets with Identifiers 207

    work page doi:10.1007/978-3-030-58638-6

  48. [50]

    Technical Report: Refining Case Models Using Cardinality Con- straints

    Haarmann S, Montali M, Weske M. Technical Report: Refining Case Models Using Cardinality Con- straints. CoRR, 2020. abs/2012.02245

    work page arXiv 2020

  49. [51]

    Workflow Soundness Verification Based on Structure Theory of Petri Nets

    Barkaoui K, Benayed R, Sbai Z. Workflow Soundness Verification Based on Structure Theory of Petri Nets. International Journal of Computing and Information Sciences (IJCIS), 2007. 5:51–62

    work page 2007

  50. [52]

    Soundness of Resource-Constrained Workflow Nets

    van Hee KM, Serebrenik A, Sidorova N, V oorhoeve M. Soundness of Resource-Constrained Workflow Nets. In: ICATPN, volume 3536 of LNCS. Springer, 2005 pp. 250–267. doi:10.1007/11494744 15

    work page doi:10.1007/11494744 2005

  51. [53]

    Soundness for Resource-Constrained Workflow Nets Is Decidable

    Sidorova N, Stahl C. Soundness for Resource-Constrained Workflow Nets Is Decidable. IEEE Trans. Syst. Man Cybern. Syst., 2013. 43(3):724–729. doi:10.1109/TSMCA.2012.2210415

    work page doi:10.1109/tsmca.2012.2210415 2013

  52. [54]

    Linear-Time Verification of Data-Aware Dynamic Systems with Arithmetic

    Felli P, Montali M, Winkler S. Linear-Time Verification of Data-Aware Dynamic Systems with Arithmetic. In: Proc. of AAAI 2022. AAAI Press, 2022

    work page 2022