Petri Nets with Parameterised Data: Modelling and Verification (Extended
  Version)
  During the last decade, various approaches have been put forward to integrate
business processes with different types of data. Each of such approaches
reflects specific demands in the whole process-data integration spectrum. One
particular important point is the capability of these approaches to flexibly
accommodate processes with multiple cases that need to co-evolve. In this work,
we introduce and study an extension of coloured Petri nets, called
catalog-nets, providing two key features to capture this type of processes. On
the one hand, net transitions are equipped with guards that simultaneously
inspect the content of tokens and query facts stored in a read-only, persistent
database. On the other hand, such transitions can inject data into tokens by
extracting relevant values from the database or by generating genuinely fresh
ones. We systematically encode catalog-nets into one of the reference
frameworks for the (parameterised) verification of data and processes. We show
that fresh-value injection is a particularly complex feature to handle, and
discuss strategies to tame it. Finally, we discuss how catalog nets relate to
well-known formalisms in this area.
