Grid computing simulation and verification based on pi calculus

Abstract

As weakness exists in describing behaviors and mobility in Petri Net theory, we put forward a mode using pi calculus to describe the gird computing, and present its simulation and verification. We briefly introduce the pi calculus at first. Then, it is drawn in detail how to outline single node computing and grid computing by pi calculus: it can be described as a two-player game. The first player moves the first token from the node to a neighboring node along an outgoing edge. On the other hand, the second player can respond only by moving the other token from the node it is on to adjacent node along an outgoing edge. It can be defined the winning mechanism which is related to the relation of the two computing ways: strong bi-simulation, weak simulation or reduction simulation. Many properties (such as deadlock or mutual exclusion violation) may be checked in this fashion. At last an example scenario is presented.