On weak, lazy, and easy soundness in robustness diagrams with loop and time controls - Ramirez, Ronnie II M.
The Robustness Diagram with Loop and Time Controls (RDLT) is a workflow model that captures the resource, process, and case workflow dimensions. Among the properties that such model has is classical soundness which implies two sub-properties of proper termination and liveness. Through weakening these two sub-properties, other notions of soundness can be identified. These notions can be used to describe real-world systems that may not adhere to the strictness of classical soundness. In recent literature, the notions of classical and relaxed soundness have only been defined in the context of RDLTs. This study addresses this gap by formalizing the weak and easy soundness property of RDLTs. This includes the definition of its behavioral and structural profiles. Furthermore, verification methods, including its time and space complexities, are provided to confirm the requirement satisfaction of the weak and easy soundness of a given RDLT. Using RDLTs as representations of real-world systems, their structures that satisfy the weaker notions of soundness are illustrated as well, specifically the chiller system. The mapping of weak-sound RDLTs to Petri Nets and comparing the satisfaction of soundness notion requirements is accomplished in the study as well.