A Model Based On The Key Actions Of Index π-Calculus And Research On Translation Of Index π-Net

This paper builds up a model which can reflect the related action of label places in index calculus. It also describes the process of exposing a hiding channel to external environment. Using semaphore system in the process of modeling can outstand the hands in ports which happening in communicating and mobile systems. And compared with p-net it reserved more nature of concurrent interaction in the mobile communication. This paper also adds new mechanisms named buffer semaphore and listening semaphore. The works includes solving the state transition scheduling problem and the proving the equivalence for expanding the properties of the buffers. At the same time, this paper gives the definition formulation equations of the new system. We also definite the system-step, give the actions sets on the main ports and the states sets of semaphores, finish the proving of strong bisimilarity proving between the system with buffer semaphore and the original department. Simultaneously, this paper also defines the index calculus, and gives the definitions of each part of index of PI nets, In the process of defining index PI net,it dose its best reserve most of the characteristics of classic Petri nets. Ensure the strong bisimilarity relationship between index PI net and Petri net. Also can ensure the semantic correctness of index PI nets. And it expounds how to add the semantic to the index of PI net. Gives the happened conditions of index PI nets transition, and the change after the occurrence of the impact on subsequent places. In the second half of the paper, it gives a simplified model of PI net. According to the model it shows that the process of exposing a internal channel to the entire system.The bisimilarity theory focuses on the equivalence between acts, it can be also used to statute system behaviors, describe what actions that different systems should have. That only the system we designed have equivalence behavior with the provisions behaviors, we can consider this system is correct. So it standard the process of modeling, this is helpful to of system behavior analysis. Therefore, this paper established the proving bisimilarity of the automata systems. Adding the buffer is proved be simulation with the original system. When it comes to system be added with listing places, it also has the strong bisimilarity relationship. After giving the definition of index PI net, it explains the structure congruence between classic petri-net and the index PI net.In this paper the innovation points mainly includes:(1). Set a buffer between the system and the external environment, and add new actions can reflect expansion. (2). Use the evolution of the state sets proving the strong bisimilarity relation from the improved system to the original system.(3). Define new index PI net, places, transitions, arcs. In these basic elements, it add mappings, so the net can reflect the actions of index PI calculus.This paper aims at using automata to describe the system behavior of index PI calculus, In order to guarantee the correctness of this descriptive modeling, Using the simulation equivalence principle to verify that the new model be bisimilarity with the original pnet. This is a try to the expansion of the theory. The second part of this paper explores how to add new semantic properties to the classic petri nets.