Linear Logic as a Tool for Deadlock-Freeness Scenarios Detection in Interorganizational Workflow Processes

This paper presents a method for deadlock-freeness scenarios detection in interorganizational workflow processes. This method considers the Interorganizational WorkFlow nets theory and is based on the analysis of Linear Logic proof trees. To detect the deadlock-freeness scenarios, a Linear Logic proof tree is built for each different scenario of the Local WorkFlow nets from which the Interorganizational WorkFlow net is composed. These proof trees are analysed and some candidates to be used in deadlock-freeness scenarios are identified. These candidates are proven by the construction and analysis of a Linear Logic proof tree that considers the local scenarios involved within it. Then, the deadlock-freeness scenarios can be analysed by the organizations staff to decide if these scenarios can provide all their necessary business relationships.