On The Simulation Of Petri Net System With Boundedness By Pi Calculus

The bisimulation of formal models is an important research issue in the field of formal methods.It can convert problems that are not easily analyzed in one model to another model by studying the mutual simulation of two formalized models.Petri nets and Pi calculus are two formalized models for studying concurrent systems and are widely used to describe and analyze concurrent systems.If the Petri net can be simulated by the Pi calculus,then the static structure and dynamic behavior of the Petri net can be transformed into the Pi calculus to express,so that the problems in the concurrent system that are not easily analyzed in the Petri net are converted into the Pi calculus for analysis.The existing conversion method of Petri net system with place capacities limited to Pi calculus,and achieved the Pi calculus simulation of the Petri net system with the place capacity limited.However,this method limits the scope of application,does not consider any nature of Petri net system,and does not apply to the Pi calculus simulation of the boundedness Petri net system.In addition,the method needs to define place process expressions and transition process expressions for all state combinations of places and transitions from zero to maximum place capacity.While some of the states included in all state combinations are not used,the process expressions defined for these states do not appear in the reduction sequence,and therefore it is not necessary to convert these redundant states into process expressions.This paper studies the simulation of the Pi calculus for the bounded Petri net system,and proposes a conversion method from the boundedness Petri net system to the Pi calculus.The conversion method proposed in this paper firstly needs to find all reachable states of the reachable set of a bounded Petri net system.Then the value of the token number in the preposition places of transition represented by each reachable state expressed is plus or minus 1 and the value of the token number in the postposition places of transition represented from the minimum reachable state to the maximum reachable state is combined,and each reachable state is represented by the value of the token number from the current reachable state plus 2 to the maximum reachable state and the value of the minimum reachable state of the token number in the preposition places of transition after adding and subtracting 1 are combined and find the state combination related to the reachable state,after according to the found reachable state and the state combination related to the reachable state,define the place process expression and the transition process expression respectively for the place and the transition,and finally use the parallel operator to connect the place process,transition process,and synchronizer process to get the Pi calculus expression.In order to verify the effect of the method of conversion from bounded Petri net system to Pi calculus,this paper designs a set of automatic transition procedure from bounded Petri net system to Pi calculus,and illustrates the transition process from bounded Petri net system to Pi calculus by an example..The conversion method proposed in this paper implements the Pi calculus simulation for the bounded Petri net system.In addition,the conversion method proposed in this paper does not need to define the place process expression and transition process expression for all state combinations.It only needs to define the expressions of the place process expressions and transition process expressions of the reachable state and the state related to the reachable state.It is reduced the number of place process expressions and transition process expressions that need to be defined.