MobilityReadingGroup

Non Angelic Concurrent Game Semantics

Simon CASTELLAN, Pierre CLAIRAMBAULT, Jonathan HAYMAN, Glynn WINSKEL

The hiding operation, crucial in the compositional aspect of game semantics, removes computation paths not leading to observable results. Accordingly, games models are usually biased towards angelic non-determinism: diverging branches are forgotten. We present here new categories of games, not suffering from this bias. In our first category, we achieve this by avoiding hiding altogether; instead morphisms are uncovered strategies (with neutral events) up to weak bisimulation. Then, we show that by hiding only certain events dubbed inessential we can consider strategies up to isomorphism, and still get a category – this partial hiding remains sound up to weak bisimulation, so we get a concrete representations of programs (as in standard concurrent games) while avoiding the angelic bias. These techniques are illustrated with an interpretation of affine nondeterministic PCF which is adequate for weak bisimulation; and may, must and fair convergences.

@inproceedings{CCHW2018,
  author = {Simon Castellan and Pierre Clairambault and Jonathan Hayman and Glynn Winskel},
  title = {{Non Angelic Concurrent Game Semantics}},
  booktitle = {21st International Conference on Foundations of Software Science and Computation Structures},
  volume = {10803},
  pages = {3--19},
  publisher = {Springer},
  year = 2018
}

@inproceedings{CCHW2018,
  author = {Simon Castellan and Pierre Clairambault and Jonathan Hayman and Glynn Winskel},
  title = {{Non Angelic Concurrent Game Semantics}},
  booktitle = {21st International Conference on Foundations of Software Science and Computation Structures},
  volume = {10803},
  pages = {3--19},
  publisher = {Springer},
  doi = "10.1007/978-3-319-89366-2_1",
  year = 2018
}