Correctness Notions for Petri Nets with Identifiers

TL;DR

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.

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.

Figures (12)

• Figure 1: The life cycles of products, customers and orders in the retail shop.
• Figure 2: t-PNID $N_{\mathit{rs}}$ 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.
• Figure 3: Type projections of Figure \ref{['fig:overallModel']}. The customer projection is not sound, as place $p$ is not bounded.
• Figure 4: A transition-bordered WF-Net (a) and its closure (b) HeeSW13.
• Figure 5: Simulation of a Minksy $2$-counter machine via t-PNIDs. Here, $q_i$, $q_k$ and $q_l$ correspond to control states of the machine.

Theorems & Definitions (69)

• Definition 2.1: Strong and weak bisimulation
• Definition 3.1: Identifier Types
• Definition 3.2: Typed Petri nets with identifiers
• Definition 3.3: Marking
• Definition 3.4: Variable sets, emitter and collector transitions, object types
• Definition 3.5: Firing rule
• Definition 3.6: Induced transition system
• Corollary 3.7
• Proposition 3.8
• Definition 4.1: Liveness