Soundness Verification and Analysis of Interorganizational Logical Workflow Nets

Soundness is a vital property of Interorganizational Logical Workflow Nets (ILWN) which can efficiently model cooperative systems. But even though each logical workflow net (LWN) is sound, soundness of arbitrary ILWN is hard to decide. This study analyzes the causes of leading to deadlocks of interface transitions and unboundedness of interface data places: the incorrect order of transitions related to interface data places, conditional routing construct and accumulation of tokens in interface data places. Based on the analysis, this paper defines the concept of T-fair LWNs and proposes an important subclass of ILWNs: T-fair ILWNs. For T-fair ILWNs, this study presents the inheritable conditions of soundness and gives a rigorous analysis approach according to their static net structures only. And then an approach of verifying the soundness of ILWNs composed of n T-fair LWNs is proposed. The concepts and techniques proposed in this study are illustrated with a useful example: an online bookstore and customer system. In addition, this paper discusses some cases which have fewer requirements for interface data. Based on that, a rather simple criteria condition is provided for T-fair ILWNs which are marked by restricted logical expressions.