Specifying and Verifying Business Process Models with Labeled Pi Calculus

Because of the strong expressive power and analysis capabilities, Pi calculus has been applied in the business process modeling area by more and more people. In existing works, Pi calculus is often used to capture the action execution logic of a business process. But the real situation is that some data and resource information are also critical for business process models besides action execution logic. Although it is possible to indirectly specify the behavior of data and resource with Pi processes, it is not intuitive for understanding and analyzing the holistic semantics of a business process. An extension for Pi calculus with state information, called labeled Pi calculus, is proposed in this paper. The main idea of labeled Pi calculus is to replace the abstract state name with the detailed state information, so that it can not only specify the semantics of action execution logic but also describe state transition of a business process. It can be regarded as an integrated formal method of state-based paradigm and event-based paradigm. Because state information is integrated to Pi calculus in a loosely coupled way, the theory and analysis capabilities of Pi calculus can be well-preserved in labeled Pi calculus. Moreover, new state simulation and equivalency relations are defined for labeled Pi calculus, which improve the analysis capability of Pi calculus considerably. A business process example is used to illustrate how to formalize the semantics of a business process with labeled Pi calculus and how to analyze the properties of it.