Browse Books

Reviewer: Idalia Flores

Reactive systems are systems whose behavior is not described algorithmically (by a relation between inputs and outputs), but rather by the way they continuously interact with the environment. The authors present and use some process calculi and verification tools to introduce model-based analysis of reactive systems. The book makes an excellent case for the usefulness of formal methods and models outside academic circles. The first part of the book covers the calculus of communicating systems (CCS), labeled transition systems, and Hennessy-Milner logic. The second part presents timed extensions for real-time systems: timed automata, timed CCS, timed labeled transition systems, and a real-time version of the Hennessy-Milner logic. The first part contains six chapters. Chapters 2 and 3 present CCS and behavioral equivalences. Chapter 4 makes a detour into order theory, presenting some notions and results, such as Tarski's fixed-point theorem, that allow the presentation of bisimulation as a fixed point. Chapters 5 and 6 introduce Hennessy-Milner logic and recursive definitions, ending with an overview of results related to model checking. In the final chapter of this part, the authors use the theory presented so far to model and analyze mutual exclusion algorithms. The second part has a similar structure, starting with the presentation of timed CCS. Chapters 10 and 11 introduce timed automata and timed behavioral equivalences. Chapter 12 presents Hennessy-Milner logic with time. This part ends with Fischer's algorithm for deadlock-free mutual exclusion under timing constraints. The book has arisen from various courses taught over six years in Iceland and Denmark, and is designed to give a broad introduction to reactive systems, with exercises throughout. The presentation is clear and intuitive enough to benefit any student interested in concurrency theory and process algebra. Several examples, many figures, and a rich bibliography are provided to assist the reader in understanding. This is an admirable piece of work, particularly for its pedagogical approach. I recommend it as an excellent textbook to those who teach concurrency theory and software tools for the model-based analysis of computing systems. Online Computing Reviews Service