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.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Matrix-Based Conversion of RDLT to PN with Multiple Abstract Arc Handling

  • Angelo Louis A. Flores,
  • Jasmine A. Malinao

摘要

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.