Qualitative Analysis of Interorganizational WorkFlow Nets Using Linear Logic: Soundness Verification

This paper presents a method for qualitative analysis of Interorganizational WorkFlow nets based on the proof trees of Linear Logic. This analysis is concerned with the proof of the Soundness correctness criterion defined for Interorganizational WorkFlow nets. To prove the Soundness property, a proof tree of Linear Logic is built for each different scenario of the IOWF-net and for the Local WorkFlow nets from which it is composed. The proposed method permits one to verify Soundness without deciding boundedness that is EXPSPACE-hard and considers the very structure of the net. Furthermore, the proposed approach gives guidance for the adjustment of interorganizational workflow processes that do not satisfy Soundness.