Full abstraction for fair testing in CCS

TL;DR

This paper establishes that a new semantics for CCS, based on the concept of playgrounds, is fully abstract for fair testing equivalence, linking game semantics with process equivalence.

Contribution

It introduces the notion of playgrounds to prove full abstraction of a semantics for CCS in the context of fair testing, connecting algebraic and game semantics.

Findings

Semantics for CCS can be viewed as presheaf and game semantics.

A new algebraic notion called playground is introduced.

The semantics is proven fully abstract for fair testing equivalence.

Abstract

In previous work with Pous, we defined a semantics for CCS which may both be viewed as an innocent presheaf semantics and as a concurrent game semantics. It is here proved that a behavioural equivalence induced by this semantics on CCS processes is fully abstract for fair testing equivalence. The proof relies on a new algebraic notion called playground, which represents the 'rule of the game'. From any playground, two languages, equipped with labelled transition systems, are derived, as well as a strong, functional bisimulation between them.