Verification of multiple input/multiple output business processes

In many business process modelling situations using Petri nets, the resulting model does not have a single input place and a single output place. Therefore, the correctness of the model cannot be assessed within the existing frameworks, which are devised for workflow nets - a particular class of Petri nets with a single input place and a single output place. Moreover, the existing approaches for tackling this problem are rather simplistic and they do not work even for simple examples. This paper shows that, by an appropriate reduction of a multiple input/multiple output Petri net, it is possible to use the existing techniques to check the correctness of the original process. The approach is demonstrated with an appropriate example.