| CCS (A Calculus of Communicating System), presented by R.Milner in the year 1980, is anabstract computation model for describing behaviours of concurrent (or interactive) systems. Themost famous modern interactive computation models, such as value-passing calculi, name-passingcalculi, and process-passing (or higher order) calculi, are all rooted from CCS. Differing fromtraditional computation models such asλ-calculi and Turing machines, CCS takes communication(or synchronization) as the primitive notion, and moreover CCS uses the composition operator andthe localization operator as the basic syntactic constructors for expressing system interactions. Thecomposition operator enables interactions, while the localization operator disables interactions.This thesis is written at the time exactly after three decades since CCS came into being.During the past three decades, studies on the theory and practice of process calculi have madeconsiderable progression. In spite of this fact, there are still several fundamental problems whichare lack of in-depth explorations. Some of them are even rarely mentioned, others are vaguelyunderstood.We will try to elaborate some new aspects of the theory of CCS, under the deep understandingof the results which was already known. Our contributions cover the following three areas:1. Observation Theory of Processes. One of the fundamental questions in theory of processesis when two processes are considered equal, and when one process is considered approxi-mate to the other. The observation theory tries to answer this question. In the traditionalway, a labelled transition system (LTS) is created at first for a single interactive model, thenbehavioural equivalences and preorders are defined via LTS. A disadvantage of this wayis that the definitions of equivalences and preorders depend on special models. If modelsare changed, some equivalences and preorders could make no sense and others need to bemodified to fit into the new models.The way taken in this thesis is completely different. At first, several basic model-independentproperties of observational equivalences or preorders are abstracted, such as extensionality,equipollence (or preservation) of interactive capabilities. After that, equivalences and pre- orders are defined via these properties, which ensures model-independence. For concretemodels, we can continue to find out the corresponding operational characterizations. Specif-ically, depending on whether environments change dynamically or not, a series of model-independent equivalences and preorders are formalized. These formalizations are intensivelystudied in the framework of CCS. Operational characterizations of these equivalences andpreorders are investigated, and the relationships between them are revealed. Several newpreorders for CCS are proposed along the way. Behavioural properties are discussed in amodel independent manner as far as possible.2. Expressiveness of CCS. The most effective way of comparing the expressiveness of onemodel with another is encoding. However, it is hard to answer whether an encoding is good.In literature,'full abstraction'usually serves as the criterion. Because of not re?ecting theoperation correspondence, full abstraction can only act as a necessary condition instead of thecriterion. Other criterions such as homomorphism are unnecessary since they are algebraic,not observational. The notion of subbisimilarity recently proposed by Fu gives some insightinto criteria of encodings.We will study relative expressiveness of different sub-languages of CCS. We will focuson the existence of encodings. The criteria taken in this thesis are direct from the modelindependent observational equivalences, which can be regarded as simplified versions ofcriteria of Fu. Since a series of equivalences are defined, we also have a series of criteria. Theresults can vary when criterion changed. In addition, we also study the Turing completenessand its relation to the mobility of local names3. Bisimilarity and Similarity Checking Problems. Algorithms and decidability issues forequivalence checking is of great significance. However, for the lack of a proper hierarchy ofCCS, few results of this kind has been obtained related to nontrivial sub-languages of CCS.This thesis studies the decidability issues of CCS on bisimilarity and similarity checkingproblems according to different name scoping rules. By exhibiting a reduction from haltingproblem of Minsky Machine via the technique of'defender's forcing', the strong bisimilarityis shownΠ01-complete for calculi with only static local channels. The strong bisimilaritywith a given finite state process, however, is decidable by an encoding to Labeled Petri Net.Further, following the idea of bisimulation base and the technique of expansion tree, andbased on well-structured transition system, the strong similarity between a finite state processand the process class without name passing is shown decidable. Strong bisimilarity, however,is shownΠ01-complete. These results are maintained no matter recursion or replication isused to specify infinite behaviors. Our study of the decidability issues also contributes to theunderstanding how mobilities of local names will affect the expressiveness. |
