Abstract
During the last decade, various approaches have been put forward to integrate business processes with different types of data. Each of these approaches reflects specific demands in the whole process-data integration spectrum. One particularly important point is the capability of these approaches to flexibly accommodate processes with multiple case objects that need to co-evolve. In this work, we introduce and study an extension of coloured Petri Nets, called catalogue and object-aware nets (COA-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 demonstrate that this class of nets can be used for representing various multi-case modelling scenarios involving objects with one-to-many correlations. We then study a parameterised verification problem of COA-nets and show how to systematically encode them into one of the reference frameworks for attacking that kind of problem in the context of infinite-state systems with data. We demonstrate that different fragments of COA-nets can have different expressive power that can affect the decidability of not only the verification problem at hand, but also the standard problem of place nonemptiness checking. Finally, we discuss how COA-nets relate to well-known formalisms in the area of multi-case and data-aware process modelling and analysis.