The Study Of The Automated Verification Of The Polyadic Pi-calculus’s Bisimulation

With the arrival of the age of the Internet, the scale of the Internet and mobilecommunication network has been gradually builded up. At the same time, Multi-Processingcomputer operating system also has already walked into thousands of families and offices,is no longer a concept in the laboratory. All of these leave the computer scientists from thestart, the main concern order computation, namely a calculation from the input to the outputof the process to become more concerned about the process began concurrent andinteractive and mobile computing behavior. The theory of the Pi-calculus and the PolyadicPi-calculus is born in this background. Using it, people can define and describe interactivebehavior strictly, which is the basic of the design of the concurrent systems. Now, it hasbeen applied to several works of the design in large engineering. In these works of design,the nature of the bisimulation of the Pi-calculation, as a important method to describe, hasbeen repeatedly mentioned, and used. However, along with the definitions of the systembecoming more and more complicated, such work of verifying bisimulation is becomingmore and more complex. The automation of that work is very necessary.This paper first analyzes the algorithm mentioned by Bj rn Victor and others aboutveryfying strong open bisimulation of Polyadic Pi-calculus. And get known that, in theoperation process of the algorithm, the two inputed Pi-clause expressions need to bedisintegrates constantly according to the rules of commitment.And then, the algorithm willhandle the sets of descendants by the amount of Cartesian product. The algorithm alwaysgets into a situation of handling the sets growing explosively, and there is a lot of use ofrecursion internal the algorithm.Aim at these problems, the paper does the following works:1. According to the description of the processing of the algorithm, design a reasonableset of data structures, used to express Polyadic Pi-calculus formulas, which have noambiguity. At the same time it is convenient to the analysis of the subsequent mathematicalformula and processing, as far as possible in data structure on the level of improve theexecution of the algorithm efficiency. And designs a reasonable set of man-machineinteractive way, and the user input Pi calculus formula in the background that is generatedand the corresponding data structure, escape establishing concentration of the datastructure. 2. Improve the algorithm of verifying Polyadic Pi-calculus strong open bisimulation,and puts forward optimum method about the abstractions, condensations, Parallels andchooses in the formulas. Make algorithm in implementation process if encounter a lot ofabstractions, condensations, Parallels or chooses, recursion number reduced greatly,improve efficiency.3. As for traditional Polyadic Pi-calculus strong open bisimulation veryfying algorithmwill caused a lot of binary relation data structure redundancy, this paper puts forward thealgorithm in implementation process. And it is no longer generate large amount of binaryrelation data structure of the copy.4. Through the discussion, sums up the importance of the α equivalent to thebisimulation verifying algorithm. This paper design and implemented a feasible PolyadicPi-calculus α equivalent verifying algorithm. α Equivalent verification can be part ofPolyadic Pi-calculus bisimulation verifying algorithm, is also a function of alone.5. Through the experimental design, verified the Polyadic Pi-calculus bisimulationverification algorithm and the α equivalent verification algorithm is feasible. And accordingto the contrast control test cases that the situation the optimization of the algorithm issuitable to.In summary, after improving bisimulation verification algorithm, the algorithm Has abetter performance when handling a lot of abstractions, condensations, Parallels andchooses in the formulas, and α equivalent verification algorithm is feasible. In the situationof handling lots of match sequence in the formula, we need to do further research andauthentication, in the hope of getting better bisimulation verification algorithm with higherperformance through continuous improvement.