We survey a recent development of Game Semantics in a new, algorithmic direction, with a view to applications in computer-assisted verification and program analysis. Several features of Game Semantics make it very promising for such applications. Game Semantics provides a very concrete way of building fully abstract models. It has a clear operational content, while admitting compositional methods in the style of denotational semantics. The basic objects studied in Game Semantics are games, and strategies on games. Strategies can be seen as certain kinds of highly-constrained processes, hence they admit the same kind of automata-theoretic representations central to model checking (see e.g. [21]) and allied methods in computer-assisted verification. Moreover games and strategies naturally form themselves into rich mathematical structures which yield very accurate models of advanced high-level programming languages, as the various full abstraction results show.
The important first steps in this direction have been taken by Ghica and McCusker [7]; they consider Idealized Algol (IA) [17] (a compact language which elegantly combines state-based procedural and higher-order functional programming) and show that the 2nd-order finitary (i.e. recursion-free) fragment of the fully abstract game semantics of IA can be represented in a remarkably simple form by regular expressions. Precisely they prove that the complete plays of the game semantics of every term of the fragment form a regular language. Since complete plays characterize observational equivalence [4], their result yields a procedure for deciding observational equivalence for the fragment. See [1] for an excellent tutorial introduction.
Further results about the decidability of observational equivalence for other fragments of IA have been obtained recently. By modelling state explicitly, the denotation of a 3rd-order finitary IA term can be shown to be compactly innocent i.e. generated by a finite view function in the sense of [11]. Any such function defines a deterministic pushdown automaton (DPDA) that recognizes exactly the complete plays of the game semantics of the term in question. Thus observational equivalence for the 3rd-order fragment is reduced to the decision problem
DPDA EQUIVALENCE: Given two DPDAs, do they recognize the same language?First posed in 1966 [8], DPDA EQUIVALENCE was only recently proved to be decidable by Sénizergues [19] who was awarded the 2002 EATCS/ACM Gödel Prize for his accomplishment (see also [20]). Hence observational equivalence for 3rd-order finitary IA is decidable [16].
Can the algorithmic representation be extended to 4th and higher orders? It turns out that 3rd order is the limit, and the best that we can do. By demonstrating that there are 4th-order terms whose complete plays correspond to runs of Turing-complete machine models, Murawski [15] has shown that observational equivalence is undecidable for the 4th-order fragment. Observational equivalence is also undecidable for the 2nd-order fragment augmented by a fixpoint operator (thus admiting recursively defined first-order functions) [16].