Non-angelic concurrent game semantics
File(s)paper.pdf (397.24 KB)
Accepted version
Author(s)
Castellan, S
Clairambault, P
Hayman, J
Winskel, G
Type
Conference Paper
Abstract
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.
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.
Date Issued
2018-04-14
Date Acceptance
2017-12-22
Citation
Foundations of Software Science and Computation Structures, 2018, 10803, pp.3-19
ISBN
9783319893655
Publisher
Springer
Start Page
3
End Page
19
Journal / Book Title
Foundations of Software Science and Computation Structures
Volume
10803
Copyright Statement
© 2018 The Authors. Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made. The images or other third party material in this book are included in the book's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the book's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
Sponsor
Engineering & Physical Science Research Council (E
Engineering & Physical Science Research Council (E
Engineering & Physical Science Research Council (EPSRC)
Engineering & Physical Science Research Council (EPSRC)
Engineering & Physical Science Research Council (E
Grant Number
ERI 025567 (EP/K034413/1)
PO 20015393
EP/K011715/1
EP/N027833/1
PO 20015391
Source
FoSSaCS 2018 21st International Conference on Foundations of Software Science and Computation Structures (FoSSaCS)
Publication Status
Published
Start Date
2018-04-14
Finish Date
2018-04-20
Coverage Spatial
Thessaloniki, Greece
Date Publish Online
2018-04-14