Soundness in the basic composition patterns of workflow nets

Workflow nets, which are derived from Petri nets, are among the most common formalisms to describe services or business processes. The soundness property is used to indicate if a service or a business process can be carried out correctly. But with the improvement of service functions, especially after SOA and Cloud Computing are widely used, a service is no longer to be confined within a single organization. A combined service can be made up by services from different suppliers. And the structure of an underlying service may only be visible from inside. So it is difficult to confirm that a composed service will perform as expected. Meanwhile, the state space can grow exponentially according to the scale of composition. The main purpose of this paper is to provide a method to check the soundness of a service composition. Four most common composition patterns (sequence, parallel, selection and iteration) are discussed via liveness and conservation of each underlying workflow net. After that, a hierarchy analysis method is introduced for more generalized compositions, which will extremely simplify the structures. This method can be performed as long as the liveness and conservation of each underlying service are guaranteed and no detailed structures of underlying services are required.