A Truly Concurrent Game Model of the Asynchronous π-Calculus

In game semantics, a computation is represented by a play, which is traditionally a sequence of messages exchanged by a program and an environment. Because of the sequentiality of plays, most game models for concurrent programs are a kind of interleaving semantics. Several frameworks for truly concurrent game models have been proposed, but no model has yet been applied to give a semantics of a complex concurrent calculus such as the pi-calculus (with replication). This paper proposes a truly concurrent version of the HO/N game model in which a play is not a sequence but a directed acyclic graph (DAG) with two kinds edges, justification pointers and causal edges. By using this model, we give the first truly concurrent game semantics for the asynchronous pi-calculus. In order to illustrate a possible application, we propose an intersection type system for the asynchronous pi-calculus by means of our game model, and discuss when a process can be completely characterised by the intersection type system.