zbMATH — the first resource for mathematics

Communication and concurrency. (English) Zbl 0683.68008
Prentice Hall International Series in Computer Science. New York etc.: Prentice Hall. XI, 260 p. (1989).
This book is an exposition of a theory of communication. Although the theory presented in the book is rooted in computer science, it may well be accepted as a general theory of systems whose components communicate one with another. The theoretical character and significance of the book may be reflected in saying that it is mathematics of communication. The book is a continuation and extension of an earlier book by the same author [A calculus of communicating systems, Lect. Notes Comput. Sci. 92 (1980; Zbl 0452.68027)]. It is also similar to another book published earlier in the same series as the present one [C. A. R. Hoare, Communicating sequential processes, Prectice-Hall Int. Ser. Comput. Sci. (1985; Zbl 0637.68007)]. It begins, however, with a slightly different notation to describe communicating processes, and develops significantly deeper theoretical treatment of phenomena taking place when the processes proceed.
The author proposes a simple language (notation) in which processes can be defined and combined to from other processes. The language semantics is explained in both, informal and formal ways. The informal explanations are given as examples and comments accompanying the formal definitions. The central idea of the language is the concept of interaction between processes. Systems built as combinations of interacting processes can be manipulated mathematically to discover their equivalences, bisimulations (certain invariants holds between pairs of processes), and observational equivalencies (where differences between what happens internally within the systems do not matter).
The equivalencies and bisimulations between combinations of processes are a basis of what can be called the communication algebra or calculus. Equipped with such a mathematical theory of communication one can specify, design, and verify systems that may be proven to work in an appropriate or desired way. The author uses the theory also to derive a procedural concurrent programming language in which semantics of multiple parallel activations of the same procedures is defined clearly and precisely.
Finally, the author explores the relationship between the present theory and logical specification of communication systems, and the problem of building and verifying determinate communication systems. The book is not too easy, especially as the author does not generally provide solutions to many exercises the reader is supposed to tackle. He only promises them to become available in the future. Nevertheless, the book seems to be the most comprehensive theoretical treatment of communication systems, available so far.
Reviewer: J.Olszewski

68-02 Research exposition (monographs, survey articles) pertaining to computer science
68Q65 Abstract data types; algebraic specification
68N25 Theory of operating systems
68N01 General topics in the theory of software
68Q45 Formal languages and automata
68Q60 Specification and verification (program logics, model checking, etc.)