Business Process Compositions Preserving k-Soundness Property

A workflow process defines a set of activities and the specific order according to which they should be executed in order to achieve a common objective. The correctness and efficiency of the business process supported by the workflow management are vital, in particular the k-soundness property when processes are modeled by workflow nets (WF-nets). This property entails the proper termination of the workflow execution and the absence of tasks that do not contribute to the processing cases. Furthermore, business processes are not isolated and in order to support the global performance of a given organization, they should well articulated, and correctly synchronized to each other. Nevertheless, without specific conditions, the k-soundness criterion is not compositional while it should remain valid for the set articulated processes. We propose in this paper a set of compositional rules that allow to build complex workflows from single ones while preserving k-soundness property under elementary conditions. Moreover, for the free-choice Petri net class we show that the soundness property verification can be efficiently checked.