Distinctives of the Game Semantics Approach

This algorithmic representation of program meanings, which is compositional, provides a foundation for model-checking a wide range of behavioural properties of Algol-like programming languages. The promise of this approach is to transfer the methods of Model Checking (see e.g. [5]) based on automata-theoretic representations, which has been so successful in the analysis of hardware designs and communications and security protocols, to the much more structured setting of programming languages, in which data types and control flow are important.

A further benefit of the algorithmic approach is that by embodying game semantics in tools, and making it concrete and algorithmic, it should become more accessible and meaningful to practitioners. We see Game Semantics as having the potential to fill the role of a ``Popular Formal Semantics'' called for in an eloquent paper by Schmidt [18], which can help to bridge the gap between the semantics and programming language communities. Game Semantics has been successful in its own terms as a semantic theory; we aim to make it useful to and usable by a wider community.

In relation to the extensive current activity in model checking and computer assisted verification, our approach is distinctive, being founded on a highly-structured compositional semantic model. This means that we can directly apply our methods to program phrases (i.e. terms-in-context with free variables) in a high-level language with procedures, local variables and data types; moreover, the soundness of our methods is guaranteed by the properties of the semantic models on which they are based. By contrast, most current model checking applies to relatively ``flat'' unstructured situations, in which the system being analyzed is presented as a transition system or automaton. It seems fair to say that Software Model Checking is still in a comparatively primitive state, with tool development in several cases running well ahead of rigorous consideration of soundness of the methods being developed. Our aim is to build on the tools and methods which have been developed in the Verification community, while exploring the advantages offered by our semantics-based approach.

With colleagues at the Computing Laboratory, University of Oxford, work is underway to investigate applications of Algorithmic Game Semantics to Software Model Checking. In addition to model-checking observational equivalence which is of basic importance, the same algorithmic representations of program meanings which are derived in this work can be put to use in verifying a wide range of program properties of IA and cognate programming languages, and in practice this is where the interesting applications are most likely to lie.

Acknowledgements.  I gratefully acknowledge the work and influence of Samson Abramsky, Dan Ghica, Guy McCusker and Andrzej Murawski and Dan Ghica; they have all contributed much to the work reported here.