基于Pi演算的跨组织业务流程约简和死锁检测

eadlock detection is an important part of cross-organizational business process analysis. Due to the strong ability of algebraic deduction of Pi-calculus, it is suitable for the modelling and analysis of cross-organizational business process. Therefore Pi-calculus is chosen as the modelling and analysis means of cross-organizational business process in this paper. Furthermore, the formal deadlock detection method of cross-organizational business process is proposed and the formal descriptions of several typical reduction rules based on Pi-calculus are presented for the large-scale and complicated cross-organizational business process. Finally, a example is presented, and the result shows that the method proposed can achieve the deadlock detection of large-scale and complicated cross-organizational business process.