Full abstraction for fair testing in CCS (expanded version)

TL;DR

This paper introduces a new semantics for CCS using playgrounds, establishing full abstraction for fair testing equivalence through algebraic structures and bisimulation, bridging game semantics and process calculus.

Contribution

It presents a novel algebraic framework called playgrounds for modeling CCS semantics and proves full abstraction of fair testing equivalence within this setting.

Findings

Defined a new semantics for CCS as presheaf and game semantics.

Introduced the concept of playgrounds as an algebraic rule of the game.

Proved full abstraction of fair testing equivalence using this framework.

Abstract

In previous work with Pous, we defined a semantics for CCS which may both be viewed as an innocent form of presheaf semantics and as a concurrent form of game semantics. We define in this setting an analogue of fair testing equivalence, which we prove fully abstract w.r.t. standard fair testing equivalence. The proof relies on a new algebraic notion called playground, which represents the `rule of the game'. From any playground, we derive two languages equipped with labelled transition systems, as well as a strong, functional bisimulation between them.