A Simple Game Semantics Model of Concurrency
Andrea Asperti, Michele Finelli, Giuditta Franco, Davide Marchignoli · 1999
In this paper we propose a conservative extension of the game model of Abramsky, Jagadeesan and Malacaria (AJM games, for short), with the aim to model CCS-like process algebras. The main novelty with respect to the existing game categories consists in relaxing the constraint that players should alternate: the condition we ask is that the players should alternate only in a round of the game, that is, every sequence of an odd and an even move must be played by different players, but we are free to choose if the first should be the Player or the Opponent (the Player / Opponent terminology is standard in game semantics to denote the two players of the game). Each move is associated with two new attributes: its value and its name. The value intuitively captures what it is carried by a channel, while the name is the semantic analogue of the channel: players alternate only with respect to the names of the moves (i.e. you are not allowed to play moves with different names within the same round). We apply this model to the study of a simple CCS-like process algebra. The main result is that we capture strong bisimulation by the existence of a simple mimic strategy between the games associated with terms.