Soundness is a key correctness criterion in Petri Net-based workflow models, yet it is not guaranteed to be preserved under composition of two disjoint sound nets. In this work, we tackle this problem and build on Portable Nets (P-Nets), a class of Petri Nets that generalizes soundness. We investigate how P-Nets can be composed in a soundness-preserving manner using an existing compositional operator such that the resulting net remains sound by design.
(a) Portable Net (b) Portable Net P-Net with an initial marking M2, see Figure 1.
Composition of Portable Nets Given and , which are sound based on the generalized
soundness notion [
Any P-Net consists of two components (i.e., subnets): an inner component and an interface component. While inner components are parts of a P-Net that are not afected by composition, interface components are directly afected by composition. An interface component consists of labelled ports. A port is a subnet of labelled elements within an interface component and serves as the gluing point for the composition with a port of another P-Net. A port of a P-Net is composable with a port of another P-Net if and only if both ports contain at least one equally labelled element. During composition, equally labelled elements of both ports become inner elements of the composed net. Elements that are not equally labelled become ports of the composed net. In this way, two disjoint P-Nets can be composed while retaining soundness.
For our running example, we compose place of with place of and of with of
. Hence, these places, and of , serve as interface components for the composition with
. The composed P-Net ⊗ remains sound exactly like its origin nets and . Note that
the composition of transitions is likewise applicable but not listed. Due to space restrictions, we
omit the application of the verification scheme of soundness from [
Related Work The idea of soundness-preserving composition of Petri nets is not new [
Conclusion We demonstrated, using an example, how the proposed soundness notion may be retained during the composition of two sound P-Nets using an existing composition operator. In future work, we aim to explore the general compositionality of arbitrary P-Nets that preserve the proposed notion of soundness producing a P-Net as a result. Moreover, we aim to establish refinement relations between High-Level and Low-Level P-Nets, allowing for systematic refinement or abstraction while preserving soundness. Additionally, we plan to investigate whether soundness of P-Nets can be decided in polynomial time.
Declaration on Generative AI The author(s) have not employed any Generative AI tools.