Concurrency has proven to be a tough problem in our computational paradigm. This book includes 34 papers presented at the 17th International Conference on Concurrency Theory. As with most books based on conference proceedings, it covers a broad spectrum, with each chapter thoroughly addressing one topic. Of those, five are invited papers, and 29 were selected by the program committee. The first section is dedicated to the invited contributions, and the second section contains two invited tutorials. The selected work is organized by topic in the next nine sections: “Model Checking,” “Process Calculi,” “Minimization and Equivalence Checking,” “Types,” “Semantics,” “Probability,” “Bisimulation and Simulation,” “Real Time,” and “Formal Languages.” The work contains extensive proofs for most of the ideas presented, and a good knowledge of the field is required in order to understand it.

The first invited contribution, “Modeling Timed Concurrent Systems,” introduces an alternative, and more complete, semantic framework to time concurrent models. The second invited work, “Some Remarks on Definability of Process Graphs,” defines two concepts of the graph structure of processes, density and connectivity, and is a contribution to the geometrical study of processes. “Sanity Checks in Formal Verification,” the third invited contribution, deals with false positives in model-checking techniques, by surveying and comparing existing work on vacuity and coverage.

Invited tutorials include “Welcome to the Jungle: Subjective Guide to Mobile Process Calculi,” one of my favorite chapters in this book. It surveys a few mobile variants of process calculi, and stresses the differences between mobile and “immobile” (that is, traditional) process calculi. The second tutorial, “Probability and Nondeterminism in Operational Models of Concurrency,” surveys the main operational models for probabilistic and nondeterministic systems, by taking probabilistic automata as a starting point, and defining other models as special cases.

One interesting contribution in the “Model Checking” section is “A Livelock Freedom Analysis for Infinite State Asynchronous Reactive Systems,” in which the authors describe a livelock test of concurrent reactive systems through integer programming. Their approach is efficient, but incomplete: it will prove the absence of livelock, or state that it cannot be proven.

“A Capability Calculus for Concurrency and Determinism” is one of the contributions in the “Minimization and Equivalence Checking” section. It describes a capability calculus for checking the partial confluence of communicating concurrent processes.

Last but not least, “Second-Order Simple Grammars,” under “Formal Languages,” presents a decidability result for the equivalence of second-order systems.