On lazy soundness of robustness diagram with loop and time controls - Afable, Mar Elden C.
This study formalizes the notion of lazy soundness in Robustness Diagrams with Loop and Time controls (RDLT's), particularly in the context of systems exhibiting parallel activities. Lazy soundness is a relaxation of classical soundness that tolerates the non-completion of certain concurrent activities, provided that at least one valid execution path leads to system completion. To capture this, the study introduces the concept of Combined Activity Structures (CAS), derived from maximal activity structures (MAS), and proposes structural conditions and algorithms to verify lazy soundness in RDLTS. A modified complaint processing system is modeled to demonstrate the applicability of the framework, where lazy soundness is enforced through shared re-sources with limited availability. The study also presents the Lazy RDLT Soundness Verification Algorithm (LRSVA) and proves its time and space complexities. Additionally, it explores the decomposition of RDLTs into Petrinets, showing that lazy soundness is preserved under this transformation. This work advances the theoretical understanding of soundness in concurrent systems and opens avenues for future research on automated verification and generalized soundness in parallel workflows.