Model Decomposition of Multi-dimensional Workflows to Petri Nets for Well-Handledness Verification
摘要
The Robustness Diagrams with Loop and Time Controls (RDLT) is a multi-dimensional workflow model that captures all three workflow dimensions: case, process, and resource. Although RDLT provides a comprehensive representation of these dimensions, its complexity often necessitates its decomposition into simpler models, such as Petri Nets (PNs), for analysis and verification. RDLT adopts and contextualizes several model properties from Petri Nets, including soundness, free-choiceness, conflict-freeness, and well-handledness, enabling their verification through model decomposition. Well-handledness in PNs ensures the absence of deadlocks and improper synchronization. In RDLT, well-handledness is satisfied when specific structural requirements such as having loop-safe non-critical arcs, safe-critical arcs, equal L-values at AND-joins, loop-safe components of every related process and being balanced, are met. This study investigates the conversion of a well-handled RDLT to PN to determine whether the resulting PN maintains well-handledness in the context of Workflow nets (WF-nets). Using the RDLT-to-PN mapping and a grammar-based approach for detecting well-handledness in Workflow nets from literature, this study revealed that a well-handled RDLT with an OR-split-join pairing does not result in a well-handled PN. These findings underscore the critical implications of workflow decomposition on model integrity and emphasize the need for precise mapping techniques to ensure the preservation of workflow properties during the conversion between workflow models.