Introduction to concurrency theory. Transition systems and CCS
type: Item
instance of: scholarly article
title: Introduction to concurrency theory. Transition systems and CCS
zbMATH Open document ID: 1333.68001
DOI: 10.1007/978-3-319-21491-7
author: Roberto Gorrieri
author: Cristian Versari
published in: Texts in Theoretical Computer Science. An EATCS Series
publication date: 2015-12-16T00:00:00Z
review text: 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.02…
reviewed by: Pedro Sánchez Terraf
Mathematics Subject Classification ID: 68-01
Mathematics Subject Classification ID: 68Q55
Mathematics Subject Classification ID: 68Q85
zbMATH DE Number: 6521523
zbMATH Keywords: labelled transition systems
zbMATH Keywords: behavioral equivalences
zbMATH Keywords: weak equivalence
zbMATH Keywords: process calculus
zbMATH Keywords: calculus of communicating systems
zbMATH Keywords: basic process algebra
zbMATH Keywords: congruence
zbMATH Keywords: strong prefixing
zbMATH Keywords: step semantics
describes a project that uses: LOTOSphere
describes a project that uses: Concurrency Workbench
describes a project that uses: LOTOS
MaRDI profile type: Publication
full work available at URL: https://doi.org/10.1007/978-3-319-21491-7
OpenAlex ID: W2483867491
description: scientific article; zbMATH DE number 6521523