The Robustness Diagram with Loop and Time Controls, or RDLT, is a workflow model that captures the resource, process, and case dimensions. One property it has is classical soundness, which implies the two sub-properties of proper termination and liveness. Through weakening these sub-properties, other soundness notions can be formed, inspired by related literature. These notions can be used to describe real-world systems that may not adhere to the strictness of classical soundness. In recent literature, only two soundness notions have been defined in the context of RDLTs. This paper addresses this gap by formalizing the weak soundness property of RDLTs. This includes the definition of its behavioral and structural profiles. Furthermore, verification methods, including their time and space complexities, are provided to confirm the requirement satisfaction of the weak soundness of a given RDLT. The mapping of weak-sound RDLTs to Petri Nets and the comparison of the satisfaction of soundness notion requirements are also done in the study.

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

On Weak Soundness in Robustness Diagrams with Loop and Time Controls

  • Ronnie M. Ramirez,
  • Jasmine A. Malinao

摘要

The Robustness Diagram with Loop and Time Controls, or RDLT, is a workflow model that captures the resource, process, and case dimensions. One property it has is classical soundness, which implies the two sub-properties of proper termination and liveness. Through weakening these sub-properties, other soundness notions can be formed, inspired by related literature. These notions can be used to describe real-world systems that may not adhere to the strictness of classical soundness. In recent literature, only two soundness notions have been defined in the context of RDLTs. This paper addresses this gap by formalizing the weak soundness property of RDLTs. This includes the definition of its behavioral and structural profiles. Furthermore, verification methods, including their time and space complexities, are provided to confirm the requirement satisfaction of the weak soundness of a given RDLT. The mapping of weak-sound RDLTs to Petri Nets and the comparison of the satisfaction of soundness notion requirements are also done in the study.