From CSP to Game Semantics

Abstract

In this short essay, we describe in informal terms how game semantics can be seen to arise as a perturbation of process calculi such as CSP, by making an explicit distinction between the rôles of the System and the Environment. Drawing out the consequences of this distinction uncovers a wealth of mathematical structure, with Game intuitions entering in a natural and compelling fashion. This leads ultimately to the elaboration of mathematically well-structured and behaviourally expressive semantic universes for computation. These provide a basis for fully abstract models of a wide range of programming languages, and lead on to algorithmic methods, with applications to compositional model-checking and program analysis.