Philippine Journal of Science
152 (6B): 2327-2342, December 2023
ISSN 0031 – 7683
Date Received: 23 May 2023

Classical Soundness in Robustness Diagram
with Loop and Time Controls

Jasmine A. Malinao¹* and Richelle Ann B. Juayong²

¹Division of Natural Sciences and Mathematics,
University of the Philippines Tacloban College, Tacloban City, Leyte 6500 Philippines
²Department of Computer Science, College of Engineering,
University of the Philippines Diliman, Diliman, Quezon City 1101 Philippines

*Corresponding author: jamalinao1@up.edu.ph

[Download]
Malinao J, Juayong RA 2023. Classical Soundness in Robustness
Diagram with Loop and Time Controls. Philipp J Sci 152(6B): 2327–2342.
https://doi.org/10.56899/152.6B.06

 

ABSTRACT

This study introduces and formalizes the concept of classical soundness for robustness diagrams and loop controls. This concept has not been established and formalized in previous literature for this type of workflow model. Although this concept may vary in syntax across different types of workflows (e.g. workflow nets, business process modeling and notation, Petri nets), this study adopts the well-known overarching semantic of classical soundness, which requires that every activity or work done by a system that is determinable from its workflow model observes proper termination and liveness. In the meantime, we discount reset-bound subsystems in our analysis of the classical soundness of our target model. We define classical soundness, along with the formalism and design strategies, to achieve proper termination and liveness on this model in both structural and behavioral aspects of the activities therein. Finally, we establish and prove the time and space complexity of proving classical soundness under these aspects for this model.