Model Independent Theory Of Mobile Calculi

Concurrent computation is inherently different to sequential compu-tation. In the literature, researchers have proposed many concurrent mod-els in an effort to capture concurrent computation, trying to be as suc-cessful as classical computation models in capturing sequential computa-tion. However, these concurrent models lack some fundamental commonground, like basic operators, operational semantics and equivalence rela-tions. Consequently, it has many negative effects on the research of con-current computation, especially on program equality, expressiveness andTuring completeness, the most fundamental parts of concurrency theory.Process calculi are mathematical models for describing and analysingproperties of concurrent computation with some characteristics in com-mon. These common points include the facts that they are based uponcommunication, that they are using interleaving semantics, etc. The neg-ative effects mentioned above affect process calculi even more apparently.We have a plethoral of similar but different calculi, many incompatibleequivalence relations, and chaotic results on expressiveness.The theory of interaction of Fu has been proposed to give processcalculi a unified framework. It features interaction as the most basic prim-itive, upon which other concepts are build. The main contributions of thisthesis are investigations of model independent thoery of mobile calculiunder this framework. As a paradigm of the theory of interaction, we re-visit theπ-calculus of name-passing calculi, and compare the well-knownequivalence relations and proof systems on it. We also introduce testingequivalence into the Calculus of Fair Ambients. The contributions of the thesis can be summarized as follows:? Investigationsoftheobservationaltheoryareconductedonπ-calculus.We revisit theπ-calculus in the theory of interaction. Equalities onπ-calculus are investigated. These equalities include testing equiva-lence. Ourπ-calculus has disjoint sets of names and name variables.Its operational semantics and equivalence relation are redefined, ad-hering to the principles of the theory of interaction. The advantageof the new formulation is that it enjoys a simpler theory and is closerto computing practice. In this thesis, it is showed that many equiv-alence relations on the originalπ-calculus (barbed bisimilarity, la-belled bisimilarity, open bisimilarity, quasi-open bisimilarity) coin-cide with the observational bisimilarity, which is defined upon theprinciples of the theory of interaction. We have a more consistentπ-calculus with simplified theory. Testing equivalence is also intro-duced to theπ-calculus in a slightly different form.? Proof systems of the observational equality and testing equivalenceare established.Axiomatization is a crucial part of the research on process calculi.Because axioms provide us with algebraic rules about equivalencerelations, process calculi are also known as process algebra. In thisthesis we are concerning ourselves about proof systems rather thanaxiom systems. We are not axiomatizing particular equivalence re-lations, instead we construct systems which can prove whether twoprocesses are equivalent. In order to faciliate axiomatisation, we in-troduce unguarded choice. It breaks the congruence of observationalequality. We observe that P equals to Q if and only ifτ.P andτ.Qare provably equal in this system. This gives us a general method todecide whether two processes are observationally equal. A similartreatment is given to testing equivalence, for which we also obtain aproof system. We also investigate finite controlπ-processes. We give a proof system for box equivalence on finite controlπ-processes.? Testing equivalence is defined and investigated for the Calculus ofFair Ambient.The Calculus of Fair Ambient (FA for short) adds co-names to theCalculus of Mobile Ambient in order to strengthen the control ofambient movements. A variant of may testing equivalence, contex-tual equivalence, has been proposed for the Calculus Mobile Am-bient. But it is very weak. The testing equivalence defined in thisthesis exploits the functions of conames, making full use of inter-action. It is showed that the observers in some special form havethe full discriminating power that all observers have. It is a con-gruence on finite processes. On hereditarily terminating processesit strictly contains bisimilarity. It is also proved in this thesis thattwo definitions of successful states, one from a structural viewpointand another from an interactive viewpoint, result in the same testingequivalence relation. This justifies the theory of interaction to someextent. This thesis also investigates the encoding fromπ-calculus toFA, showing that it is also fully abstract with respect to the testingequivalence. This adds weights to the viewpoint thatπ-calculus is asubcalculus of FA.The results in this thesis give us a deeper insight into both the theoryof interaction and name-passing calculi. ourπ-calculus can be consid-ered as a paradigm of redefining process calculi in the theory of interac-tion. The coincidence theory in this thesis tells that equivalence relationscan be unified to a single, objective and model independent relation. Boxequivalence also shows that testing equivalence, which is originally de-fined in a different style, can be integrated into the theory of interactionsmoothly. All theses results are of significance in reinforcing the view thatprocess calculi and concurrent computation should be investigated in asingle framework.