On The Bisimualtion Theory, Expressiveness And Proof System Of Some Name-passing Calculi

Mobile systems are everywhere. The name-passing calculus, often called π-calculus, pro-posed by Milner, Parrow and Walker, is a classical concurrent mobile model for mobile systems.The π-caluclus is not only a model framework of mobile systems, but an efective mathematicaltool for expressing, analyzing and validating concurrent systems. To gain deeper insights into thetheoretical properties and application values of the π-calculus, variants of the π-calculus have beenan important subject of research. Many variants of the π-calculus have been proposed according todiferent criteria, such as operator independence, probabilistic mechanism, synchronous and asyn-chronous mechanisms, tuple transmitted and specifed application scenes, and the results cover thefollowing areas, behavior equivalence, expressiveness, proof system, programming language, andsystem analysis and verifcation etc. However, most variants lack of a systematic study.This dissertation focuses on three variants of the π-calculus, whichvaries from the usability ofreceived names, the number of transmitted names and sensitivity to spatial information. It studiestheir theoretical problems, e.g. the observation theory, the expressiveness and the proof system.The contributions of the dissertation is as follows:1. Variation on name usability. These variants are studied systematically in the frameworkof the model independent theory of interaction. External bisimulations coinciding with theabsolute equality are defned for two variants, and by the coincidences two complete equa-tional proof systems are proposed for the absolute equality on fnite terms. On the basis of thesubbisimilarity criteria, separation results on the expressiveness between the π-calculus andthese variants are presented, and the relation between the absolute equality and the self inter-pretation is revealed. Their interactive completeness are proved by encoding the interactionmodel of computable function.2. Variationontupletransmitted. Bytransformingtheequalityproofsforopentermstoequal-ity proofsforprocesses, a complete equational proofsystemis presentedfortheweakbisimu-lationonthefnitetermsofthek-adicπ-calculus. Itmakesupthestudyontheproofsystemofthepolyadicπ-calculus, andmakesgoodpreparationforthedecisionmethodsofthebehaviorequivalences of the upcoming variants on spatial-sensitive semantics. 3. Variation on spatial-sensitive semantics. Using k-adic π-calculus as a testbed, two variantsof k-adic π-calculus, enriched with spatial-sensitive semantics (the local cause semantics andthe locality semantics) are defned. With respect to the operational correspondence, two fullyabstract encoding are presented from these variants of the k-adic π-calculus to the k+1-adic π-calculus, so that the spatial-sensitive semantics bisimulations are reduced to the weakbisimulation. These two full abstraction results give rise to an interpretation of the spatial-sensitive semantics in the interleaving framework. Two equational proof systems and a newdecision method are proposed for the spatial-sensitive semantics bisimulation on the fniteterms.