Matrix-Based Conversion of RDLT to PN with Multiple Abstract Arc Handling
摘要
Robustness Diagrams with Loop and Time Controls (RDLTs) provide a rich, multi-dimensional framework for modeling complex workflows, while Petri Nets (PNs) offer powerful formal analysis capabilities. Converting RDLTs to PNs allows leveraging PN analysis tools, but existing methods often lack full automation, especially when operating directly on formal representations. A significant challenge arises from RDLT preprocessing techniques (like Expanded Vertex Simplification) which can generate multiple abstract arcs between vertex pairs in the simplified model, summarizing distinct internal paths. Current RDLT-to-PN mappings do not adequately address the automated, matrix-based conversion of these multi-arc structures. This paper presents a novel algorithm for the direct conversion of RDLT matrix representations into PN matrix representations. Crucially, our algorithm incorporates a formally verified mapping strategy to correctly handle multiple abstract arcs, preserving their distinct semantics and traversal limits. This matrix-based approach enables fully automated transformation. Through matrix analysis, we establish that the proposed RDLT-to-PN conversion maintains easy soundness; however, weak soundness is not preserved in the generated PN.