On The Bisimulation Theory And Axiomatization Of Higher-order Process Calculi

Higher-order process calculi,for its abstraction capability and theoretical significance, have constantly been receiving much attention in the field of process calculi,and stand as a mathematical tool for describing and analyzing mobile systems with dynamically changing inter-connection structures.In this thesis we contribute to the higher-order paradigm in several aspects.●Higher-orderπ-calculus with mismatch:the bisimulation theory.Linear fragment of higher-orderπ-calculus with mismatch:the axiomatization.The problem of the axiomatization of higher-order process calculi,such as higherorderπ-calculus,is always a non-trivial one.However,it is important,both in theory and practice,to be able to decide whether two higher-order processes are equivalent with respect to some bisimulation,which needs an algorithm that can effectively analyze and give an answer efficiently.We further the available work by considering the higher-orderπ-calculus with mismatch,which is a useful operator in bisimulation theory and especially the axiomatization,from algorithmic point of view.We first formulate the bisimulation theory,where the bisimulation we define is called open weak higher-order bisimulation,which is a non-delayed and open-styled bisimulation, in presence of the mismatch operator,and then follow the linear approach when designing the axiom system,that is restrain to the linear fragment of the calculus.In terms of the characterization of the open weak higher-order bisimulation,including properties exclusive in linear calculi such as the relationship between the equivalence of prefixed processes and the equivalence of their continuations,we eventually prove the completeness theorem of our axiom system.Our work on bisimulation theory and axiomatization not only extends previous one by influxing a useful operator,but pushes forward more ahead on the way to more advanced study on higher-order axiomatization as well.It also gives insight into the study of other higher-order languages,such as Ambient calculi.●Encoding first-orderπ-calculus with higher-order CCS.Encoding between different calculi is an effective way to compare the expressive power of them and can shed light on the essence of where the difference lies.Thomsen and Sangiorgi have worked on the higher-order calculi(higher-order CCS and higherorderπ-calculus,respectively)and the encoding to and from first-orderπ-calculus. But the work is not complete,in that the encoding of first-orderπ-calculus with higher-order CCS lacks a fully abstract result.In this paper,we try to settle this part.We follow the encoding strategy,first by Thomsen,of translating first-orderπ-calculus into Plain CHOCS.We show that the encoding strategy is fully abstract with respect to ground bisimilarity(in first-orderπ-calculus)and wired bisimilarity (in Plain CHOCS),which is a bisimulation we define on wired processes that only send and receive wires,which is the core in the encoding strategy.Moreover from the fact that wired bisimilarity implies the well-known context bisimilarity,we secure the soundness of the encoding,with respect to ground bisimilarity and context bisimilarity. We use index technique to get around all the technical details to reach these main results,that is the index technique is applied to the original encoding strategy to take care of the extra internal actions generated during the encoding,and then the results in indexed version of the encoding is bridged to the original(non-indexed) encoding.We also make some discussions on how to obtain full abstraction on other reasonable bisimulations in either calculus.Our work on the encoding between process calculi cracks down the long unsettled problem on expressing first-orderπ-calculus in higher-order CCS,thus complementing the encoding between the two kinds of calculi.The contribution mainly lies in solidifying the bridge between first-order calculi and higher-order calculi.Furthermore,it can entail another encoding ofλ-calculus using higher-order calculi.●Logical characterization of local bisimulation in linear higher-orderπ-calculus.Besides work on bisimulations in higher-order process calculi in an algebraic way, logic is also used to study bisimulations.Logical characterization of strong and weak context bisimulation in Plain CHOCS has been reported.In this thesis,we make some new work on linear process calculi in a logical way.We endeavor to find a logical characterization of local bisimulation in linear higher-orderπ-calculus.We prepare for the characterization in two steps:first we simplify local bisimilarity with some variants;second we approximate the local bisimilarity with a descending chain of bisimulations.To achieve the logical characterization,we have to exercise a reformulation on the calculus and obtain an equivalent one(in the sense of bisimulation) easier for the characterization.Our logic has full negation and is simpler than available ones,in that higher-order modality is downscaled to resembling first-order ones, and constructive implication operator is merely used to cope with first-order bound output.We prove the characterization theorem relating logical equivalence to local bisimilarity.Our work on logical characterization mainly contributes to the study of higherorder process calculi by offering another viewpoint,the logical viewpoint,thus complementing the algebraic approach.Moreover,converting a bisimulation equivalence checking to a logical equivalence checking entails immediately the feasibility of logical methodology,which is equipped with both various model checking algorithms and practical tools.Our work in this thesis not only investigates several aspects of higher-order paradigm, but convey some meaningful information as well.One point is that linearity plays a crucial role in securing a sound and complete axiom system in higher-order calculi.This feature successfully downscales the expressive power of communicating processes.Another point is that complementary to the representability of higher-order calculi by first-orderπ-calculus,we show that the converse also holds with respect to reasonable bisimilarities. This adds to the faithfulness that higher-order paradigm is relatively stand-alone,which renders it more appealing with its extra abstracting capability.The logical characterization offers some insight into the linearity by exhibitting that a simpler yet complete logical language solidifies the bisimulation equivalence,which expands the application area of higher-order process calculi.