An intensionally fully-abstract sheaf model for $\pi$ (expanded version)

TL;DR

This paper introduces a novel sheaf-based model for the $$-calculus that is fully abstract with respect to fair testing equivalence, capturing process behaviors compositionally through sheaves on simple sites.

Contribution

It develops a new sheaf model for the $$-calculus that is fully abstract for fair testing, extending previous work on CCS with a combinatorial site construction.

Findings

The model is intensionally fully abstract for fair testing equivalence.

Processes are interpreted as sheaves that preserve and reflect testing equivalence.

The construction relies on a combinatorial presentation of traces using string diagrams.

Abstract

Following previous work on CCS, we propose a compositional model for the $\pi$-calculus in which processes are interpreted as sheaves on certain simple sites. Such sheaves are a concurrent form of innocent strategies, in the sense of Hyland-Ong/Nickau game semantics. We define an analogue of fair testing equivalence in the model and show that our interpretation is intensionally fully abstract for it. That is, the interpretation preserves and reflects fair testing equivalence; and furthermore, any innocent strategy is fair testing equivalent to the interpretation of some process. The central part of our work is the construction of our sites, relying on a combinatorial presentation of $\pi$-calculus traces in the spirit of string diagrams.