Introduction to concurrency theory. Transition systems and CCS (Q897107)

This text provides a detailed introduction to the subject of concurrency, where the main focus is put on the Calculus of Communicating Systems (CCS) [\textit{R. Milner}, A calculus of communicating systems. Berlin-Heidelberg-New York: Springer-Verlag (1980; Zbl 0452.68027)] and derivatives, as well as on a careful study of their semantics. The book is organized in six chapters, each with its own abstract. It also contains a useful `glossary', and very detailed bibliography and index. The first chapter consists of a concise introduction to the subject matter of the text, instructions for teaching use and a quick but exhaustive review of notation, and logical and mathematical preliminaries. The second chapter introduces labelled transition systems (LTSs) and the vast majority of process equivalences that will be used in the book, ranging from trace equivalence to isomorphism, going through (bi)similarity, considering completed and weak versions. Here and in the rest of the book, there are a lot of examples and exercises, most of them interrelated (the former often provide solutions to the latter), treated with a very useful level of detail, most of the time with full proofs. Chapter 3 introduces CCS, in a first intuitive section with examples (illustrating semi-counters, competition, interfaces), and then formally. Several subcalculi of CCS are studied separately and later compared, in terms of syntactical and semantical expressiveness. Here, examples also abound, including: buffers, producer-consumers, and counters in several implementations. More than 60 diagrams (most of them in this and the previous chapter) depict LTSs and other concepts, making the book very readable. Next, decidability issues are explored, with a proof of Turing-completeness of finitary CCS and undecidability of weak bisimilarity by reducing 3-register counter machines [\textit{M. L. Minsky}, Computation: finite and infinite machines. Englewood Cliffs, NJ: Prentice-Hall, Inc. (1967; Zbl 0195.02402)] to CSS. Finally, value-passing CCS is treated briefly. Chapter 4 provides a detailed analysis of the identities satisfied by the various process operators up to some equivalence (bisimilarity, etc.), developing into the concept of congruence and axiomatizing these equivalences. As in other parts of the book, the treatment is exhaustive. In Chapter 5, it is studied how new operators can be interpreted in CCS. In the case of sequential composition, a notion of successfully terminating state is introduced in the calculus and the LTS semantics. A hierarchy of calculi is obtained by adding CCS operators to composition, to obtain finite BPA (``basic process algebra''), BPA* (finite BPA with iteration = regular expressions), plain BPA, PA (BPA plus parallel operator without communication), and finally PAER (= PA + restriction). The final chapter starts with a discussion about the inadequacy of CCS to solve the classical dining philosophers problem that motivates the introduction of strong prefixing as a way to implement atomic actions. The calculus thus obtained, multi-CCS [\textit{R. Gorrieri} et al., Theor. Comput. Sci. 72, No. 2--3, 203--223 (1990; Zbl 0698.68029)] carries a different, step semantics, where LTSs are labelled with multisets of actions. The comparison between this and the traditional interleaving semantics (adopted up to this point) is a good point to present the structural congruence. A handful of examples (``case studies''), more details of expressivity (implementing the CSP \(\|_A\) operator), and conclusions discussing some literature, round this chapter off. I would like to quote a fragment of the foreword of the book (by Pierpaolo Degano), as it faithfully summarizes some of its aspects: ``This monograph is therefore an excellent textbook for introducing undergraduate and graduate students, as well as people developing or using concurrent systems, to the theories of concurrency. Some aspects of concurrent systems are not considered here, those typical to more advanced models, like mobility of agents. After a course based on this book, however, a student will have all the knowledge and the techniques to face this intriguing and challenging topic, and many others.''