Correctness Notions for Petri Nets with Identifiers

Jan Martijn E.M. van der Werf*, Andrey Rivkin, Marco Montali, Artem Polyvyanyy

*Corresponding author for this work

Research output: Contribution to journalJournal articleResearchpeer-review

15 Downloads (Pure)


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.
Original languageEnglish
JournalFundamenta Informaticae
Issue number2-4
Pages (from-to)159-207
Publication statusPublished - 2024


  • Information System
  • Verification
  • Data Correctness
  • Resource Correctness


Dive into the research topics of 'Correctness Notions for Petri Nets with Identifiers'. Together they form a unique fingerprint.

Cite this