We introduce the concurrent game semantics of Probabilistic PCF (PPCF). The model consists of concurrent strategies based on event structures with symmetry, extending with probability a model of Castellan, Clairambault and Winskel.

We "collapse" this model to the weighted relational model of PPCF (Pagani et al), by forgetting the execution history of programs; we retain only the states reached by terminated executions. Usually such operations on strategies are only lax-functorial, but we will see that terms of PPCF satisfy a condition called 'visibility', which ensures that no deadlock arise in their composition, and hence that the collapse to weighted relations is functorial.

Because probabilistic relations are fully abstract for PPCF, we obtain via the collapse that concurrent games are also (intensionally) fully abstract.

(Joint work with Simon Castellan, Pierre Clairambault & Glynn Winskel)