Deadlock-Freeness Scenarios Detection in Web Service Composition

This paper presents a method for deadlock-freeness scenarios detection in Web services composition. This method considers the Petri 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 modules from which the composed system is built. 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 organization staff to decide if these scenarios can provide all their necessary business relationships.