Clovis Eberhart

Tom Hirschowitz

Thomas Seiller

AN INTENSIONALLY FULLY-ABSTRACT SHEAF MODEL FOR π (EXPANDED VERSION)

Keywords: Programming languages, categorical semantics, presheaf semantics, game semantics, concurrency, process algebra

Following previous work on CCS, we propose a compositional model for the π-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 π-calculus traces in the spirit of string diagrams.

Causal models and beyond. Operational semantics of programming languages standardly model the execution of programs as paths in a certain labelled transition system (lts). Under this interpretation, different possible interleavings of parallel actions yield different paths. Verification on ltss thus incurs a well-known state explosion problem. Similarly, causality between various actions, visible in the syntax, is lost in the lts, thus making, e.g., error diagnostics difficult [START_REF] Gösler | Causality analysis in contract violation[END_REF].

Causal models, originally designed for Petri nets [START_REF] Nielsen | Event structures and domains, part 1[END_REF] and Milner's CCS [START_REF] Winskel | Event structure semantics for CCS and related languages[END_REF], intend to remedy both problems, but have yet to be applied to full-scale programming languages. They have recently been extended in two different directions: (1) by Crafa et al. [START_REF] Crafa | Event structure semantics of parallel extrusion in the pi-calculus[END_REF] to Milner's π-calculus, and (2) by Melliès [START_REF] Melliès | Asynchronous games 4: A fully complete model of propositional linear logic[END_REF] to Girard's linear logic. The former extension accounts for the subtle interaction of channel creation with synchronisation in π, a significant technical achievement, 30 years after the first causal semantics for CCS. The latter is the first causal model for functional languages (inspired by Hyland-Ong's and Nickau's games models for PCF [START_REF] Nickau | Hereditarily sequential functionals[END_REF][START_REF] Hyland | On full abstraction for PCF: I, II, and III[END_REF]). An important challenge is now the search for a causal model of fullfledged languages with both concurrent and functional features. Winskel and collaborators are currently working in this direction, using extensions of Melliès's approach [START_REF] Rideau | Concurrent strategies[END_REF][START_REF] Winskel | Strategies as profunctors[END_REF][START_REF] Castellan | The parallel intensionally fully abstract games model of pcf[END_REF].

In previous work [START_REF] Hirschowitz | Innocent strategies as presheaves and interactive equivalences for CCS[END_REF][START_REF] Hirschowitz | Full abstraction for fair testing in CCS[END_REF][START_REF] Hirschowitz | Full abstraction for fair testing in CCS (expanded version)[END_REF], we have proposed a causal model for CCS based on a different approach. We here push this approach further by applying it to the π-calculus.

1.2. Traces and naive concurrent strategies. In standard causal models, execution traces essentially consist of partially ordered sets of atomic 'events'. Our approach relies on a new notion of trace, which we now briefly sketch. There is first a (straightforward) notion of position, which is essentially a finite hypergraph whose nodes are thought of as agents, and whose hyperedges between nodes x 1 , . . . , x n are thought of as communication channels shared by x 1 , . . . , x n . There is then a notion of atomic action from one position to another. The collection of atomic actions is thought of as a 'rule of the game'. Examples of atomic actions are: an agent creates a new, private communication channel; an agent forks into two new agents connected to the same channels; an agent sends some channel a over some channel b to some other agent. We finally have a notion of trace which allows several atomic actions to occur, in a way that only retains some minimal causality information between them. We here mean, e.g., information such as: 'such agent outputs on such channel only after having created such other channel'.

The main purpose of our notion of trace is to interpret π-calculus processes as some kind of strategies over them. Most naively, a strategy on some position X is a prefix-closed set of 'accepted' traces from X. But what should prefix mean in our setting? Well, we may view traces with initial position X and final position Y as morphisms Y X. Sequential composition of traces, denoted by •, yields an analogue of prefix ordering, defined by t ≤ t•w. Strategies as prefix-closed sets of traces however fail to suit our needs on three counts. First, such naive strategies may not be stable under isomorphism of traces; second, they are bound to model coarse behavioural equivalences, at least as coarse as may testing equivalence (a.k.a. trace equivalence); and third, they permit undesirable interaction between players. Let us examine these issues in more detail.

The first, easy one is that there is an obvious notion of isomorphism between traces, under which strategies should be closed. The second problem is more serious: until now, these too naive strategies are not concurrent enough to adequately model CCS or the πcalculus.

Example 1.1 (Milner's coffee machines). Consider the CCS processes P = (a.b + a.c) and Q = a.(b + c). The process P has two ways of inputting on a and then, depending on the chosen way, inputs on either b or c. The process Q inputs on a and then has both possibilities of inputting on b or c. They hence exhibit significantly different interactive behaviour. Both processes, however, accept exactly the same traces (in the standard sense), namely {ǫ, a, ab, ac}, where ǫ denotes the empty trace. Thus, taking strategies to be prefix-closed sets of traces would prevent us from directly modelling any reasonably fine behavioural equivalence on processes. Inspired by presheaf models [START_REF] Joyal | Bisimulation and open maps[END_REF], we remedy both problems at once by passing from prefix-closed sets of traces to presheaves (of finite sets) on traces. Indeed, in the simple case where traces on X form a mere poset T(X) by prefix ordering, a prefix-closed set of traces is nothing but a contravariant functor from T(X) to the ordinal 2, viewed as a category. The latter has two objects 0 and 1 and just one non-trivial morphism 0 → 1. The idea is that a functor S∶ T(X) op → 2 maps any trace to 1 when it is accepted, and to 0 otherwise. Furthermore, if t ≤ t ′ , i.e., t is a prefix of t ′ , then we have a morphism t → t ′ which should be mapped by S to some morphism S(t ′ ) → S(t). If t ′ is accepted then S(t ′ ) = 1, so this has to be a morphism 1 → S(t). Because there are no morphisms 1 → 0, this entails S(t) = 1, hence prefix-closedness of the corresponding strategy. Now in the case where traces form a proper category T(X), whose morphisms encompass both prefix ordering and isomorphism between traces, considering functors T(X) op → 2 retains prefix-closedness and solves our first problem: for any t ≅ t ′ , functoriality imposes S(t) ≅ S(t ′ ). Our second problem is then solved by replacing such functors with presheaves, i.e., functors T(X) op → Set.

Example 1.2. In Example 1.1, the two ways that P has to accept inputting on a may be reflected by mapping the trace a to some two-element set. More precisely, P may be modelled by the presheaf S defined on the left and pictured on the right:

• S(ǫ) = {⋆},

• S(a) = {x, x ′ },

• S(ab) = {y},

• S(ac) = {y ′ },

• S empty otherwise,

• S(ǫ ↪ a) = {x ↦ ⋆, x ′ ↦ ⋆}, • S(a ↪ ab) = {y ↦ x}, • S(a ↪ ac) = {y ′ ↦ x ′ }, ⋆ x x ′ y y ′ . a a b c
Presheaves thus may 'accept a trace in several ways': the trace a is here accepted in two ways, x and x ′ . The process Q is of course modelled by equating x and x ′ .

As it turns out, we actually only need finitely many ways of accepting each trace. Thus, we arrive at a first sensible notion of strategy given by presheaves of finite sets, i.e., functors T(X) op → set, where set denotes the category with as objects all finite subsets of N, with all maps between them. We call them (naive) strategies in the sequel. (Please note that set is equivalent to the category of all finite sets.) Notation 1.3. For any C, let C denote the category of presheaves of finite sets over C. 1.3. Innocence as a sheaf condition. The third problem evoked above is that functors T(X) op → set allow some undesirable behaviours. Intuitively, in π just as in CCS, agents should not have any control over the routing of messages.

Example 1.4. Consider a position X with three agents x, y, and z sharing a communication channel a, and a strategy S accepting (1) the trace where x outputs on a, (2) the trace where y inputs on a, and (3) the trace where z inputs on a. Then, both synchronisations should be accepted by S. However, one easily constructs a naive strategy in which one is refused (see Example 6.2).

In order to rectify this deficiency, we enrich strategies with 'local' information. The idea is that a strategy should not only accept or refuse traces on the whole position X, but also traces on all possible subpositions of X. Moreover, this local information should fit together coherently.

Example 1.5. Consider the position X of Example 1.4. Any strategy on X should now in particular include independent strategies for each of the three agents x, y, and z. Coherence means that in order for a trace to be accepted, it should be enough for it to be 'locally accepted', i.e., at every stage in the trace, each agent should approve what they see of the next action. E.g., if the next action is a synchronisation x y with x outputting and y inputting on some channel a, then all that is required for the synchronisation to be accepted is that x accepts to output and y accepts to input. Consequently, if some other agent z also accepts to input on a at this stage, then the synchronisation x z is also accepted.

We call this putative coherence condition innocence by analogy with Hyland and Ong's notion [START_REF] Hyland | On full abstraction for PCF: I, II, and III[END_REF]. In order to formalise it, we first extend our category of traces T(X) on X with new objects representing traces on subpositions of X. We also add new morphisms, which are about 'locality'. Indeed, standardly, plays form a poset for the prefix ordering, but here we want to enrich this, e.g., by embedding traces on subpositions of X into traces on X.

Example 1.6. Consider a position X with two agents x 1 and x 2 . There is a trace t on X in which both agents fork. Consider now the subposition Y of X consisting solely of x 1 and the trace t ′ on Y in which x 1 merely forks. There is a morphism t ′ → t in our new category. This extended category, T X , yields an intermediate notion of strategy, given by functors T op X → set. Among the new objects, we have in particular traces on just one agent of X obtained by sequentially composing atomic actions whose final position again consists of one agent. We call this particular kind of trace a view. Views are the most 'local' kind of objects in T X . They form a full subcategory V X of T X .

Example 1.7. If X merely consists of an agent x linked to n communication channels, consider the atomic action given by x forking into two new agents, say x 1 and x 2 . This action, viewed as an object of T X has three subobjects which are views: (1) the 'identity' view, in which nothing happens, (2) π l n , which represents the left-hand branch (to x 1 ), (3) and π r n , which represents the right-hand branch (to x 2 ). The inclusion V X ↪ T X induces a simple Grothendieck topology [START_REF] Mac | Sheaves in Geometry and Logic: A First Introduction to Topos Theory[END_REF] on T X , which amounts to decreeing that any trace is covered by its views. We finally call any S∶ T op X → set innocent precisely when it is a sheaf for this Grothendieck topology. In particular, giving an innocent presheaf on T X is equivalent (up to isomorphism) to separately giving an innocent presheaf for each agent of X, which rules out the undesirable behaviour described in Example 1. [START_REF] Adámek | Locally Presentable and Accessible Categories[END_REF].

Sheaves on T X form a category S X , which is small thanks to our use of set instead of Set. They furthermore map back to naive strategies, i.e., presheaves on T(X), by forgetting the local information. Finally, because the considered topology is particularly simple, sheaves are equivalent to presheaves on views, i.e., S X ≃ V X (recalling Notation 1.3). In summary, we have three categories of strategies: naive strategies are presheaves on the 'global' category of traces T(X), innocent strategies S X are sheaves on the extended category of traces T X , and so-called behaviours B X are presheaves on the category of views V X . The last two are equivalent, and we furthermore have an adjunction T(X) S X .

We use both sides of the equivalence: behaviours directly lead to our compositional interpretation ⟦-⟧∶ Pi → S of π-calculus processes, and innocent strategies are used below as the basis for our semantic definition of fair testing equivalence. 1.4. Main result. What should we do in order to demonstrate adequacy of our model? By definition, causal models expose some intensional information. Hence, equality is generally much finer than any reasonable behavioural equivalence, so we should not base our main result on it. On the other hand, causal models are supposed to be 'compositional', i.e., to come equipped with an interpretation of syntactic operations in the model. A natural thing to do is thus to choose some behavioural equivalence defined from syntactic operations, use compositionality to transpose it to the model, and prove that the two coincide. More precisely, the considered equivalence induces by quotienting two 'extensional collapses', one syntactic and the other semantic, and we want to prove that the translation induces a bijection between both extensional collapses. Following [START_REF] Abramsky | Full abstraction for PCF[END_REF], we call this intensional full abstraction for the considered equivalence. In fact, all behavioural equivalences end up relying on some notion of observation, which we will also need to transpose to the model.

We here focus on so-called testing equivalences [START_REF] De | Testing equivalences for processes[END_REF][START_REF] Natarajan | Divergence and fair testing[END_REF][START_REF] Brinksma | Fair testing[END_REF][START_REF] Rensink | Fair testing[END_REF], which are defined in two stages. First, one chooses a 'mode of interaction'. That is, one defines what the relevant tests are for a given process and specifies how the two should interact. Typically, tests for P are other processes T with the same free communication channels as P , and interaction is just parallel composition P T . This part will be easy to transpose to the model by compositionality. The second stage amounts to choosing when P T is successful. E.g., in may testing equivalence P T is successful just when there exists a transition (P T ) ♡ ⇒ P ′ (that is, a ♡ transition, possibly surrounded by silent transitions), where ♡ is some 'tick' action fixed in advance. In must testing equivalence, success is when all maximal (possibly infinite) transition sequences contain at least one ♡ transition. In fair testing equivalence, one requires that all silent sequences (P T ) ⇒ P ′ extend to some sequence P ′ ⇒ P ′′ ♡ → P ′′′ ending with a ♡ transition. These ideas transpose to the model by observing whether a given trace contains a ♡ action. In this paper, we focus on fair testing equivalence, i.e., we prove (Theorem 6.25) that our model is intensionally fully-abstract for fair testing equivalence. We finally show (Section 7.4) that the result generalises to a wide range of testing equivalences, obtained by varying the notion of success.

In order to fix intuitions, let us quickly motivate must and fair testing, using barbed congruence [START_REF] Sangiorgi | The π-calculus -a theory of mobile processes[END_REF] as a standard starting point. Barbed congruence equates processes P and Q, roughly, when for all contexts C, C[P ] and C[Q] are weakly bisimilar w.r.t. reduction (i.e., only τ -actions are allowed), and furthermore they have the same interaction capabilities at all stages. Barbed congruence is sometimes perceived as too discriminating w.r.t. guarded choice. Consider, e.g., the following CCS processes.

P 1 = • • • • • • • τ τ τ a τ b P 2 = • • • • • • • τ τ τ b τ a
Both processes may disable both actions a and b, the only difference being that P 1 disables a before disabling b. Barbed congruence distinguishes P 1 from P 2 (consider the trivial context C = ◻), which some view as a deficiency. Another possibility would be must testing equivalence [START_REF] De | Testing equivalences for processes[END_REF]. Recall that P must pass a test process R iff all maximal executions of P R perform, at some point, the 'tick' action ♡. Then, P and Q are must testing equivalent iff they must pass the same tests. Must testing equivalence does equate P 1 and P 2 above, but is sometimes perceived as too discriminating w.r.t. divergence. E.g., consider Q 1 = !τ a and Q 2 = a. Perhaps surprisingly, Q 1 and Q 2 are not must testing equivalent. Indeed, Q 2 must pass the test a.♡, but Q 1 does not, due to an infinite, silent reduction sequence.

Fair testing equivalence was originally introduced (for CCS-like calculi) to rectify both the deficiency of barbed congruence w.r.t. choice and that of must testing equivalence w.r.t. divergence. The idea is that two processes are equivalent when they should pass the same tests. A process P should pass the test T iff their parallel composition P T never loses the ability of performing the special 'tick' action ♡, after any ♡-free reduction sequence. Fair testing equivalence thus equates P 1 and P 2 above, as well as Q 1 and Q 2 . Cacciagrano et al. [START_REF] Cacciagrano | Explicit fairness in testing semantics[END_REF] provide an excellent survey of fair testing for π. 1.5. Contributions. Since this paper follows the same approach as previous work on CCS [START_REF] Hirschowitz | Innocent strategies as presheaves and interactive equivalences for CCS[END_REF][START_REF] Hirschowitz | Full abstraction for fair testing in CCS[END_REF][START_REF] Hirschowitz | Full abstraction for fair testing in CCS (expanded version)[END_REF], we should explain in which sense extending the approach to π is more than an easy application.

A first contribution comes from the fact that, in order to even define composition in our category of traces, we need to show that traces form the total category of a fibration [START_REF] Jacobs | Categorical Logic and Type Theory[END_REF] over positions. In previous work, this was done in an ad hoc way. We here introduce a more satisfactory approach based on factorisation systems [START_REF] Mac | Duality for groups[END_REF][START_REF] Freyd | Categories of continuous functors, I[END_REF].

A second significant contribution is prompted by the interplay between synchronisation and private channels in π, which is notoriously subtle to handle. And indeed, our proof method for CCS fails miserably on π. One reason for this, we think, is that our notion of trace for π, though simple and natural, is not 'modular' enough, in the sense that a trace contains strictly more information than the collection of all 'local' information accessible to agents (i.e., of all of its views, in the above sense). Thus, adapting our proof technique from CCS would have required us to define a much more complex but more modular notion of trace. Instead, we here take a somewhat rougher route.

Finally, our proof now applies not only to fair testing equivalence, but also to a whole class of testing equivalences. [START_REF] Busi | A Petri net semantics for π-calculus[END_REF][START_REF] Montanari | Concurrent semantics for the πcalculus[END_REF][START_REF] Engelfriet | A multiset semantics for the pi-calculus with replication[END_REF][START_REF] Luca Cattani | Presheaf models for the π-calculus[END_REF][START_REF] Boreale | A fully abstract semantics for causality in the π-calculus[END_REF][START_REF] Degano | Non-interleaving semantics for mobile processes[END_REF][START_REF] Luca | Models for name-passing processes: Interleaving and causal[END_REF][START_REF] Bruni | Event structure semantics for nominal calculi[END_REF][START_REF] Crafa | Event structure semantics of parallel extrusion in the pi-calculus[END_REF][START_REF] Busi | Distributed semantics for the π-calculus based on Petri nets with inhibitor arcs[END_REF], as well as interleaving models [START_REF] Fiore | A fully-abstract model for the pi-calculus (extended abstract)[END_REF][START_REF] Fiore | Semantics of name and value passing[END_REF][START_REF] Stark | A fully abstract domain model for the π-calculus[END_REF][START_REF] Luca | Models for name-passing processes: Interleaving and causal[END_REF][START_REF] Montanari | Structured coalgebras and minimal HDautomata for the π-calculus[END_REF][START_REF] Hennessy | A fully abstract denotational semantics for the π-calculus[END_REF] and the early approach [START_REF] Jategaonkar | Causality and true concurrency: A data-flow analysis of the pi-calculus (extended abstract)[END_REF] based on Girard's Geometry of Interaction. All of these models are based on some lts for π. Instead, ours is rather based on reduction rules. The subtleties usually showing up in ltss, related to mixing synchronisation and private channels, do resurface in our proof of intensional full abstraction, but not in the definition of our model. Indeed, it merely goes by describing the 'rule of the game' in π, and applying the general framework of playgrounds [START_REF] Hirschowitz | Full abstraction for fair testing in CCS (expanded version)[END_REF].

Another general framework relating operational and denotational descriptions of programs is Kleene coalgebra [START_REF] Bonchi | Deriving syntax and axioms for quantitative regular behaviours[END_REF], which is mainly designed for automata theory. Playgrounds may be viewed as adapting ideas from Kleene coalgebra to the process-algebraic setting.

We should also mention Laird's games model of (a fragment of) π [START_REF] Laird | Game semantics for higher-order concurrency[END_REF], which accounts for trace (a.k.a. may testing) equivalence. Standard game models view strategies as sets of traces (with well-formedness conditions), so, as we have seen, lend themselves better to modelling trace equivalence. In a non-deterministic, yet not concurrent setting, Harmer and McCusker [START_REF] Harmer | Categorical combinatorics for innocent strategies[END_REF] resort to an explicit action for divergence, which allows them to recover a finer behavioural equivalence. We feel that the presheaf-based approach is more general.

Furthermore, recent work by Tsukada and Ong [START_REF] Tsukada | Nondeterminism in game semantics via sheaves[END_REF] adapts and extends some ideas of [START_REF] Hirschowitz | Innocent strategies as presheaves and interactive equivalences for CCS[END_REF][START_REF] Hirschowitz | Full abstraction for fair testing in CCS[END_REF] to nondeterministic, simply-typed λ-calculus. In particular, they show that innocent strategies as sheaves are compatible with the hiding operation of standard game semantics. Eberhart and Hirschowitz further establish [START_REF] Eberhart | Justified sequences in string diagrams: a comparison between two approaches to concurrent game semantics[END_REF] a formal link between Tsukada and Ong's notion of innocence and ours: they construct a model of nondeterministic, simplytyped λ-calculus in our style, and then a morphism of Grothendieck sites, which entails that both models are equivalent.

Let us moreover mention less closely related work: Girard's ludics [START_REF] Girard | Locus solum: From the rules of logic to the logic of rules[END_REF], Melliès's reworking of game semantics [START_REF] Melliès | Asynchronous games 2: the true concurrency of innocence[END_REF][START_REF] Melliès | Asynchronous games 4: A fully complete model of propositional linear logic[END_REF], the part of it rediscovered by Levy [START_REF] Blain | Morphisms between plays[END_REF] with a different presentation, Melliès's game semantics in string diagrams [START_REF] Melliès | Game semantics in string diagrams[END_REF], Harmer et al.'s categorical combinatorics of innocence [START_REF] Harmer | Categorical combinatorics for innocent strategies[END_REF], McCusker et al.'s graphical foundation for schedules [START_REF] Mccusker | A graphical foundation for schedules[END_REF], and Winskel's strategies as profunctors [START_REF] Winskel | Strategies as profunctors[END_REF]. Finally, Hildebrandt's work [START_REF] Thomas | Towards categorical models for fairness: fully abstract presheaf semantics of SCCS with finite delay[END_REF] also uses sheaves, though as a tool to correctly handle infinite behaviour, as opposed to their use here to force reactions of agents to depend only on their views. 1.7. Plan. In previous work [START_REF] Hirschowitz | Full abstraction for fair testing in CCS (expanded version)[END_REF], we have defined an algebraic notion called playground, which provides a sufficient framework for sheaf-based innocence to make sense. Namely, it organises positions, atomic actions, and traces into a pseudo double category [START_REF] Ehresmann | Catégories structurées[END_REF][START_REF] Ehresmann | Catégories et structures[END_REF][START_REF] Grandis | Limits in double categories[END_REF][START_REF] Grandis | Adjoints for double categories[END_REF][START_REF] Leinster | Higher Operads, Higher Categories[END_REF]30] with additional structure. Any playground D automatically gives rise, among other things, to

• categories of innocent strategies S X on each position X, organised into a pseudo double functor from D op to small categories; • a simple, yet complete syntax for innocent strategies, together with an lts S D for them over an alphabet built from atomic actions. After introducing some notation, the considered variant of π-calculus, fair testing equivalence (Section 2), and recalling the notion of playground, we construct a playground D for the π-calculus in Sections 3 to 5. This is a lot of work, and not all aspects of playgrounds are used in defining the model and proving the main result. The reason we devote so much energy to it is that playgrounds provide a really helpful setting, in fact a calculus, for reasoning about positions, traces, views and the various notions of strategies. The underlying pseudo double category is constructed in Section 3. The main playground axiom, asserting that a certain functor is a Grothendieck fibration, is established in Section 4. Finally, the remaining axioms are proved in Section 5.

We then continue in Section 6 by applying results from [START_REF] Hirschowitz | Full abstraction for fair testing in CCS (expanded version)[END_REF] to define our sheaf model and semantic fair testing equivalence, as well as our translation ⟦-⟧ of π. We then state the main result (Theorem 6.25). In Section 7, after introducing the basic notion of definite residual, we reduce our main theorem to an analogous statement about an lts S for strategies (derived from S D ). The advantage of the latter statement is that it lies entirely in the realm of ltss. We then define a further, more syntactic lts M which we prove equivalent to S, thus further reducing the main result to an analogous statement about M. We finally prove the latter, which entails the main result.

Notation and preliminaries

We start in this section with a few reminders. In Section 2.1, after fixing some basic notation, we recall ltss. We use a slightly more general, graph-based notion than the standard, relation-based one. In Section 2.2, we introduce the considered π-calculus, which is mostly standard except that (1) we use a presentation in the style of Berry and Boudol's chemical abstract machine [START_REF] Berry | The chemical abstract machine[END_REF], and (2) we consider infinite terms, thus sparing us the need for recursion or replication constructs. We then go on and recall fair testing equivalence for π in Section 2.3. In fact, because we will also need to define fair testing for other ltss, we introduce a general framework in which it makes sense, called graphs with testing. We further provide sufficient conditions for a relation between the vertices of two graphs with testing to preserve and reflect fair testing equivalence (Lemma 2.22 and Corollary 2.25). Finally, in Section 2.4, we recall and briefly explain the definition of playgrounds.

2.1. Basic notation and labelled transition systems. First of all, we adopt the notation of [39, Section 2], with the slight modification that set now denotes the category with finite subsets of N as objects, and all maps as morphisms. (This category is equivalent to what we used in [START_REF] Hirschowitz | Full abstraction for fair testing in CCS (expanded version)[END_REF], but slightly easier to work with for our purposes.) For all n ∈ N, we often abuse notation and let n denote the finite set {1, . . . , n}. We denote by Ĉ the category of presheaves on C, and by C the category of presheaves of finite sets, i.e., of contravariant functors to set. For any category C, let C f denote the full subcategory of finitely presentable objects [START_REF] Adámek | Locally Presentable and Accessible Categories[END_REF], or finite objects for short. In the only case where we'll use this, C will be a presheaf category [C op , set] and furthermore due to the special form of C, finite presentability of F ∈ Ĉ will be equivalent to the category of elements of F being finite, and further equivalent to the set of elements of F being finite, i.e., ∑ c∈ob(C) F (c) is finite.

To recall some bare minimum: we often confuse objects C of a category C with the corresponding representable presheaves y C ∈ Ĉ. Gph denotes the category of reflexive graphs, and all our graphs are reflexive so we often omit mentioning it. We think of morphisms p∶ G → A in Gph as ltss over the alphabet A, except that for reasons specific to playgrounds our convention is that a transition from x to y is represented as an edge x ← y. Using graphs as alphabets generalises the standard approach based on sets of labels: indeed, in order to model any set of labels, take for A the graph with one vertex and one endo-edge for each label. The extra generality is useful, e.g., to add some typing information on labels. Finally, using graphs as alphabets provides us with standard tools for transporting ltss across morphisms (by pullback, resp. post-composition).

For any graph G, G ⋆ denotes the graph with the same vertices and all paths between them; on the other hand, fc(G) denotes the free category on G, i.e., the category with the same vertices and identity-free paths between them. Both (-) ⋆ and fc extend to functors, i.e., act on morphisms. We often silently coerce fc(G) into a reflexive graph, and denote by the obvious morphism G ⋆ → fc(G).

For any graph p∶ G → A over A, x, y ∈ ob(G), and edge a∶ p(y) → p(x) in A, we denote by x a ← y the existence of an edge e∶ y → x in G such that p(e) = a. When a = id , we just write x ← y. We denote strong bisimilarity over A by ∼ A .

For any graph p∶ G → A over A, x, y ∈ ob(G), and path ρ∶ p(y) → p(x) in A ⋆ , we denote by x ρ ⇐ y the existence of a path r∶ y → x in G ⋆ such that p ⋆ (r) = ρ. When ρ is the empty path we just write x ⇐ y. We denote weak bisimilarity over A by ≈ A .

2.2.

A π-calculus. We now present our variant of π, which features a chemical abstract machine presentation and infinite terms. Also, we keep track of the channels known to the considered process, i.e., we work with a 'natural deduction' presentation of terms.

Processes are infinite terms coinductively generated by the grammar

γ ⊢ g P 1 . . . γ ⊢ g P n γ ⊢ i∈n P i γ ⊢ P γ ⊢ Q γ ⊢ P Q γ, a ⊢ P γ ⊢ g νa.P γ ⊢ P γ ⊢ g ♡.P γ ⊢ P γ ⊢ g τ.P a ∈ γ γ, b ⊢ P γ ⊢ g a(b).P a, b ∈ γ γ ⊢ P γ ⊢ g ā⟨b⟩.P
, where

• we have two judgements, ⊢ for processes and ⊢ g for guarded processes;

• γ ranges over finite sets of natural numbers, and • γ, a is defined iff a ∉ γ and then denotes γ ⊎ {a}.

Notation 2.1. Let Pi be the set of all such (non-guarded) processes. Let Pi γ denote the set of processes γ ⊢ P .

As usual, a is bound in νa.P and b is bound in a(b).P . In the following, processes are considered equivalent up to renaming of bound channels. Capture-avoiding substitution extends the assignment γ ↦ Pi γ to a functor set → Set mapping σ∶ γ → γ ′ to P ↦ P [σ].

Let us now describe the dynamics of our π-calculus. They are slightly unusual, in that they are presented in the style of the chemical abstract machine. In particular, there are silent transitions for 'heating' both parallel composition and name creation. A further slight peculiarity, which we adopt for its convenience in the chemical abstract machine presentation, is that name creation is a guard. E.g., we have some processes of the form (νa.P )+b(x).Q. This is hardly significant. E.g., the previous process is strongly bisimilar to (τ.νa.P ) + b(x).Q in more standard settings, and our results are about equivalences coarser than weak bisimilarity anyway. Notation 2.2. For any γ ⊢ g P , γ ⊢ Q of the form ∑ i∈n Q i , and injection h∶ n ↪ n + 1, we denote by P + h Q the sum ∑ j∈n+1 P j , where P h(i) = Q i for all i ∈ n and P k = P , for k the unique element of (n + 1) ∖ Im(h). Definition 2.3. Let -⊙ denote the finite multiset monad on sets.

Definition 2.4. A configuration is an element of Conf = ∑ γ∈P f (N) Pi ⊙
γ . Notation 2.5. Configurations (γ, S) will be denoted by ⟨γ∥S⟩, and we will use list syntax [P 1 , . . . , P n ] for multisets, sometimes dropping brackets, e.g., as in ⟨γ∥P 1 , . . . , P n ⟩. We sometimes resort to a hopefully clear 'multiset comprehension' notation [P ϕ(P )]. We use ∪ for multiset union and

x ∶∶ M = [x] ∪ M .
Just as Pi , Conf extends to a functor set → Set by capture-avoiding substitution.

Let us now extend Conf to an lts over the alphabet {♡, τ }. This means that we need to construct a graph morphism Conf → Σ, where Σ denotes

• ♡ τ ,
τ being the chosen identity edge. This is done in Figure 1, omitting identity edges. There, we let R and R ′ range over processes of the form ∑ i∈n P i . The last rule makes sense because each transition as in the premise implicitly comes with an inclusion h∶ γ 1 ↪ γ 2 , and the second occurrence of S is implicitly S Let us now define fair testing equivalence for π, together with our general framework of graphs with testing. Graphs with testing are essentially De Nicola and Hennessy's original framework [START_REF] De | Testing equivalences for processes[END_REF], adapted to our graph-based presentation of ltss. We derive a few results about general graphs with testing, notably sufficient conditions for a relation between two graphs with testing to preserve and reflect fair testing equivalence.

[h]. ⟨γ∥P Q⟩ τ ← ⟨γ∥P, Q⟩ ⟨γ∥τ.P + h R⟩ τ ← ⟨γ∥P ⟩ ⟨γ∥♡.P + h R⟩ ♡ ← ⟨γ∥P ⟩ ⟨γ∥νa.P + h R⟩ τ ← ⟨γ, a∥P ⟩ ⟨γ∥a(b).P + h R, ā⟨c⟩.Q + h ′ R ′ ⟩ τ ← ⟨γ∥P [b ↦ c], Q⟩ ⟨γ 1 ∥S 1 ⟩ α ← ⟨γ 2 ∥S 2 ⟩ ⟨γ 1 ∥S ∪ S 1 ⟩ α ← ⟨γ 2 ∥S ∪ S 2 ⟩ (α ∈ {τ, ♡})
Remark 2.6. In [START_REF] Hirschowitz | Full abstraction for fair testing in CCS (expanded version)[END_REF], an abstract framework was defined for studying fair testing equivalence and its relationship with weak bisimilarity. We won't use this here, and instead work in a simpler setting.

We first cover π-calculus, and then generalise. The starting point is that we need to be able to test processes against other processes, and more generally configurations against configurations. Because configurations carry their sets of free channels, it makes sense to consider a partial parallel composition operation: Definition 2.7. For any ⟨γ∥S⟩, ⟨γ ′ ∥S ′ ⟩ ∈ Conf, let ⟨γ∥S⟩@⟨γ ′ ∥S ′ ⟩ denote ⟨γ∥S ∪ S ′ ⟩ if γ = γ ′ and be undefined otherwise. Let furthermore ǫ γ = ⟨γ∥⟩.

Lemma 2.8. The domain of @, i.e., the set of pairs (C, C ′ ) such that C@C ′ , is an equivalence relation.

Let us denote by ¨Conf this equivalence relation.

Here is the standard definition of fair testing equivalence: Definition 2.9. Let Conf denote the set of configurations C such that for all C ⇐ C ′ , there exists C ′ ♡ ⇐ C ′′ . Any two configurations C and C ′ are fair testing equivalent iff C ¨Conf C ′ and for all

D ¨Conf C, (C@D) ∈ Conf iff (C ′ @D) ∈ Conf .
Let us now abstract away from this definition. For this, it would make sense to start from a partial, parallel composition map. However, in the model, the corresponding map will involve a pushout of positions which is only determined up to isomorphism. We thus generalise from partial maps to relations, but we need to impose some conditions. What matters is the use we will make of parallel composition for testing. Intuitively, we will check that the parallel composition C@C ′ belongs to some given pole, which is closed under weak bisimilarity over Σ. This choice is perhaps slightly arbitrary, but it encompasses all known testing equivalences. Finally, to gain just a little more generality, we will use the fact that weak bisimilarity over Σ coincides with strong bisimilarity over fc(Σ), and work with the latter (Definition 7.40). For ltss over fc(Σ) obtained by applying fc to ones over Σ, this is equivalent to the previous setting. The extra generality is useful for describing ltss which are not free categories. E.g., in Section 7.1, we introduce the graph with testing C, whose transitions are traces, which compose in a non-free way. We thus start from the following notion, and then define fair testing equivalence. Definition 2.10. A graph with testing is a graph G together with a morphism p∶ G → fc(Σ) and a relation R∶ (ob(G)) 2 ob(G) whose domain is an equivalence relation and which is partially functional up to strong bisimilarity over fc(Σ).

The domain being an equivalence relation more precisely means that the set {(x, y) ∃z.(x, y) R z} forms an equivalence relation over ob (G).

Partial functionality up to strong bisimilarity means that if (x, y) R z and (x, y) R z ′ , then z ∼ fc(Σ) z ′ . Notation 2.11. The relation is called the testing relation, and we denote it by G , i.e., (x, y) R z is denoted by z ∈ (x G y). Furthermore, its domain is denoted by ¨G. We use and ¨when there is no ambiguity. Since is partially functional up to strong bisimilarity, for any (x, y) R z, as long as what we say about z is invariant under strong bisimilarity, then it also holds for any other z ′ such that (x, y) R z ′ . In such cases, we implicitly make some global choice of z and consider as partially functional.

Example 2.12. Figure 1 defines a morphism p Conf ∶ Conf → Σ. Because, @ is a partial map, it induces a partially functional relation ob(Conf) 2 ob(Conf), whose domain is an equivalence relation. Because partially functional implies partially functional up to strong bisimilarity, we have: Proposition 2.13. The morphism fc(p Conf )∶ fc(Conf) → fc(Σ), with @ as testing relation, forms a graph with testing.

We may now mimick the standard definition of fair testing equivalence in the abstract setting: Definition 2.14. For any graph with testing p∶ G → fc(Σ), let G denote the set of objects x such that for all x ← y, there exists y ♡ ← z. Any two objects x and y are fair testing equivalent iff x ¨G y and for all z ¨G x,

(x G z) ∈ G iff (y G z) ∈ G .
Remark 2.15. Because we are working over fc(Σ), if G has the shape fc(G ′ ), then single transitions like x ← y denote arbitrary paths of silent transitions. And analogously x ♡ ← y denotes any path with all edges silent except exactly one. Notation 2.16. We denote fair testing equivalence in G by ∼ G f . Given x, any z such that x ¨z is called a test for x, and x passes the test iff (x G z) ∈ G .

Example 2.17. Definition 2.14 instantiates to Definition 2.9.

In fact, the construction of the graph with testing fc(p Conf ) from p Conf is easily generalised: Lemma 2.18. For any morphism p G ∶ G → Σ and relation R∶ (ob(G)) 2 ob(G) whose domain is an equivalence relation, R equips fc(p G ) with testing structure iff it is partially functional up to weak bisimilarity over Σ.

Proof. R is a strong bisimulation for fc(G) iff it is a weak bisimulation for G. Definition 2.19. A graph with testing is free iff it is of the form fc(p G ).

Our fc(p Conf ) is thus a free graph with testing. Let us conclude this section with a sufficient condition for a relation between the vertices of two graphs with testing to be adequate for fair testing equivalence, and a natural specialisation to free graphs with testing.

Definition 2.20. A relation R∶ ob(G)

ob(H) between the vertex sets of two graphs with testing p G ∶ G → fc(Σ) and

p H ∶ H → fc(Σ) is fair iff • x R y and x ′ R y ′ implies (x ¨G x ′ ) ⇔ (y ¨H y ′ );
• R is total and surjective, i.e., -for all x ∈ G, there exists y ∈ H such that x R y, and for all y ∈ H, there exists x ∈ G such that x R y;

• x R y implies x ∼ fc(Σ) y; • if x R y, x ′ R y ′ ,
G ∶ G → fc(Σ) and p H ∶ H → fc(Σ), x ∈ G and y ∈ H, if x ∼ fc(Σ) y, then (x ∈ G ) ⇔ (y ∈ H ).
Proof. Assume x ∈ G and consider any transition y ← y ′ in H. By bisimilarity, x ← x ′ ∼ fc(Σ) y ′ . By hypothesis, we find x ′ ♡ ← x ′′ , so by bisimilarity, y ′ ♡ ← y ′′ . Thus, y ∈ H , which entails the result by symmetry.

Proof of Lemma 2.22. Consider any such x, y, x ′ , and y ′ . By Lemma 2.21, it suffices to show one direction of the desired equivalence. So let us assume that x ∼ G f x ′ . Then x ¨G x ′ , hence also y ¨H y ′ by fairness of R. By symmetry, it again suffices to check one direction of the desired implication. Consider thus any t ¨H y such that (y t) ∈ H . By surjectivity of R, we find s ∈ G such that s R t. By fairness again, we find u ∈ (x s) and v ∈ (y t) such that u R v, so (x s) ∼ fc(Σ) u ∼ fc(Σ) v ∼ fc(Σ) (y t), and hence by the previous lemma

(x s) ∈ G . Because x ∼ G f x ′ , this entails (x ′ s) ∈ G ,
′ R y ′ , then (x ∼ fc(G) f x ′ ) ⇔ (y ∼ fc(H) f y ′ ).
Proof. Because weak bisimilarity over Σ is the same as strong bisimilarity over fc(Σ), being weakly fair is the same as being fair for the generated graphs with testing.

2.4. Playgrounds. To conclude this preliminary section, let us recall the axioms for playgrounds [START_REF] Hirschowitz | Full abstraction for fair testing in CCS (expanded version)[END_REF]. Some constructions and results are developped from these axioms in op. cit. Some of the main ideas are reviewed and reworked in Sections 6 and 7.

Let us start with a brief recap of pseudo double categories. A pseudo double category D consists of a set ob(D) of objects, shared by a 'horizontal' category D h and a 'vertical' bicategory D v . Since we won't consider strict double categories, we'll often omit the word 'pseudo'. Following Paré [START_REF] Paré | Yoneda theory for double categories[END_REF], D h , being a mere category, has standard notation (normal arrows, ○ for composition, id for identities), while the bicategory D v earns fancier notation ( for arrows, • for composition, id • for identities). D is furthermore equipped with a set of double cells α, which have vertical, resp. horizontal, domain and codomain, denoted by dom v (α), cod v (α), dom h (α), and cod h (α). The horizontal domain and codomain of a double cell are vertical morphisms, while the vertical domain and codomain are horizontal morphisms. E.g., for α in the diagram delow, we have u = dom h (α), u ′ = cod h (α), h = dom v (α), and h ′ = cod v (α). D is furthermore equipped with operations for composing double cells: ○ composes them along a common vertical morphism, • composes along horizontal morphisms. Both vertical compositions (of morphisms and double cells) may only be associative up to coherent isomorphism. The full axiomatisation is given by Garner [30], and we here only mention the interchange law, which says that the two ways of parsing the above diagram coincide:

(β ′ ○ β) • (α ′ ○ α) = (β ′ • α ′ ) ○ (β • α). X X ′ X ′′ Y Y ′ Y ′′ Z Z ′ Z ′′ h u h ′ u ′ k k ′ u ′′ v h ′′ v ′ k ′′ v ′′ α α ′ β β ′
For any (pseudo) double category D, we denote by D H the category with vertical morphisms as objects and double cells as morphisms, and by D V the bicategory with horizontal morphisms as objects and double cells as morphisms. Domain and codomain maps form functors dom v , cod v ∶ D H → D h and pseudofunctors dom h , cod h ∶ D V → D v . We will refer to dom v and cod v simply as dom and cod, reserving subscripts for dom h and cod h .

We then need to recall the notion of fibration (see [START_REF] Jacobs | Categorical Logic and Type Theory[END_REF]). Consider any functor p∶ E → B. A morphism r∶ E ′ → E in E is cartesian when, as in We may now state the definition of playgrounds.

E ′′ E ′ E p(E ′′ ) p(E ′ ) p(E), r p(
Remark 2.28. The following differs slightly from the original definition, mostly in presentation and terminology, but more significantly because the class B of basic moves was mistakenly required to be replete in [START_REF] Hirschowitz | Full abstraction for fair testing in CCS (expanded version)[END_REF].

We provide some intuition right after the definition.

Definition 2.29. In a double category, a cell α is special when its vertical domain and codomain cod(α) and dom(α) are identities. For any u∶ X Y of length 0, there is an isomorphism id

• X → u in D H , as in X X X Y . u ū α u
1 Replete means closed under isomorphism. where v y,M either is a basic action or has length 0, which is unique up to canonical isomorphism, i.e., for any

y ′ ∶ d ′ → X, v ′ ∶ d d ′ , and α ′ ∶ v ′ → M with dom(α ′ ) = y and cod(α ′ ) = y ′ , we have y ′ = y M and there exists a unique isomorphism β∶ v → v ′ making the diagram d Y d y,M X d ′ y v y,M M α y,M α ′ β y M y ′ v ′ commute. (P6) (Left decomposition) Any double cell A X Y B Z h u w 1 w 2 k α decomposes as A X C Y B Z h u 1 u u 2 l w 1 w 2 k α 1 α 2 α 3
with α 3 an isomorphism, in an essentially unique way. (P7) (Right decomposition) Any double cell as in the center below, where b is a basic action and M is an action, decomposes in exactly one of the forms on the left and right:

A X B Y C Z α 1 α 2 A X B Y C Z h w b u M k α A X B Y C Z.
M ← b → M ′ then M ≅ M ′ .
Intuitively, the objects of D are configurations, or positions, in the game. The considered games are multi-party, so it makes sense to consider embeddings of positions: this is intended to be described by the horizontal category D h . The vertical category D v is that of traces, or plays: morphisms u∶ Y X model plays from the initial position X, to the final one, Y . Finally, cells model embeddings of plays, preserving initial and final position. E.g., this could model embedding the part of a play involving a particular agent.

Individuals are intended to model agents in a position, with a role similar to that of representable presheaves among general ones. Typically, the hom-set D h (d, X), with d ∈ I, models the set of agent slots of type d in the position X. For example, in the playground we construct below for π, individuals bear the number of channels that an agent is connected to, so that a morphism [n] → X amounts to an n-ary agent in X, i.e., an agent connected to n channels. Accordingly, the object [n] models a position with just one n-ary agent.

Actions model moves in the game, and atomicity (P3) notably says that any play decomposes into moves. The distinction between basic and full actions has to do with innocence. The two notions are more or less dual: basic actions are as thin as possible, while full ones are as wide as possible. Intuitively, an action is full when it cannot embed into a larger one (unless possibly some agents are added), while it is basic when it cannot embed any smaller one. As we will see, in our playground for π, we have an action for forking, which describes how an agent x may fork into two, say x 1 and x 2 . This action is full, and it has two basic sub-actions, which respectively model the passage from x to x 1 and to x 2 . For another example, we also have an action for inputting on some given channel: it is obviously basic, but in fact also full, because the only way to embed it into a wider action is to add an agent and do a synchronisation. In view of this, it should be natural that basic actions have individuals as their domain and codomain (P2). As alluded to in (P5), views will be defined as composites of basic actions. Axiom (P5) intuitively enforces existence of one sub-action for each agent in the final position of any action. Extending this to general plays will yield an operation analogous to taking the view of a play in standard game semantics. Axiom (P9) requires that these basic sub-actions may not be shared among different full actions.

Both (P6) and (P7) are decomposition axioms. The former says that a decomposition of a play reflects essentially uniquely onto any subplay. The latter essentially says that basic actions are strictly sequential: if any play of the form b • w with b basic embeds into some other play, then the image of w should occur after that of b. This is expressed in a slightly convoluted way by saying that if the latter play decomposes as M • u, then

• either b maps to M , in which case w should map to u,

• or b maps to U , in which case w should also map to u. This should make most of the axioms rather intuitive: the others are technical, which means that they emerged from our attempts to make things work out, but that we are not yet able to explain them satisfactorily.

A pseudo double category of traces

In this section, we introduce our notion of trace, which is based on certain combinatorial objects, close in spirit to string diagrams. We first define these string diagrams, and then use them to define traces. Positions are special, hypergraph-like string diagrams whose vertices represent agents and whose hyperedges represent channels. A perhaps surprising point is that actions are not just a binary relation between positions, because we not only want to say when there is an action from one position to another, but also how this action is performed. This will be implemented by viewing actions from X to Y as cospans Y → M ← X in a certain category Cf , whose objects we call higher-dimensional string diagrams for lack of a better term. The idea is that X and Y respectively are the initial and final positions, and that M describes how one goes from X to Y . By combining such actions (by pushout), we get a bicategory D v of positions and traces. Finally, we recast D v as the vertical bicategory of a pseudo double category D.

3.1. String diagrams. The category Cf will be a category of finite presheaves over a base category, C. Let us motivate the definition of C by recalling that (directed, multi) graphs may be seen as presheaves over the category with two objects ⋆ and [START_REF]Proc. 11th Symposium on Logic in Computer Science[END_REF], and two nonidentity morphisms s, t∶ ⋆ → [START_REF]Proc. 11th Symposium on Logic in Computer Science[END_REF]. Any such presheaf G represents the graph with vertices in G(⋆) and edges in G [START_REF]Proc. 11th Symposium on Logic in Computer Science[END_REF], the source and target of any e ∈ G [START_REF]Proc. 11th Symposium on Logic in Computer Science[END_REF] being respectively G(s)(e) and G(t)(e), or e ⋅ s and e ⋅ t for short. A way to visualise how such presheaves represent graphs is to compute their categories of elements [START_REF] Mac | Sheaves in Geometry and Logic: A First Introduction to Topos Theory[END_REF]. Recall that the category of elements el G for a presheaf G over C has as objects pairs (c, x) with c ∈ C and x ∈ G(c), and as morphisms

(c, x) → (d, y) all morphisms f ∶ c → d in C such that y ⋅ f = x. This category admits a canonical functor π G to C, and G is the colimit of the composite el G π G → C y → Ĉ
with the Yoneda embedding. E.g., the category of elements for y [START_REF]Proc. 11th Symposium on Logic in Computer Science[END_REF] is the poset (⋆, s)

s → ([1], id [1] ) t ← (⋆, t), which could be pictured as
, where dots represent vertices, the triangle represents the edge, and links materialise the graph of G(s) and G(t), the convention being that t connects to the apex of the triangle. We thus recover some graphical intuition.

Let us give the formal definition of C for reference. We advise to skip it on a first reading, as we then attempt to provide some intuition. Definition 3.1. Let G C be the graph with, for all n, m, with a, b ∈ n and c, d ∈ m:

• vertices ⋆, [n], π l n , π r n , π n , ν n , ♡ n , τ n , ι n,a , o n,a,b , and τ n,a,m,c,d ; • edges s 1 , ..., s n ∶ ⋆ → [n], plus, ∀v ∈ {π l n , π r n , ♡ n , τ n , o n,a,b }, edges s, t ∶ [n] → v; • edges [n] t → ν n s ← [n + 1] and [n] t → ι n,a s ← [n + 1]; • edges π l n l → π n r ← π r n and ι n,a ρ → τ n,a,m,c,d ǫ ← o m,c,d .
Let C be the free category on G C , modulo the equations

s ○ s i = t ○ s i l ○ t = r ○ t ρ ○ t ○ s a = ǫ ○ t ○ s c ρ ○ s ○ s n+1 = ǫ ○ s ○ s d .
The first equation should be understood in

C(⋆, v) for all n ∈ N, i ∈ n, and v ∈ ∪ a,b∈n {π l n , π r n , ♡ n , τ n , ι n,a , o n,a,b , ν n }. (This is rather elliptic: if v has the shape ι n,a or ν n , s ○ s i is really ⋆ s i → [n + 1] s → v.)
The second equation should be understood in C([n], π n ) for all n, and the last two in C(⋆, τ n,a,m,c,d ), for all n, m, a ∈ n, and c, d ∈ m.

Our category of string diagrams is the category of finite presheaves Cf . A presheaf X over C is a kind of higher-dimensional graph whose components are typed by objects of C:

• X(⋆) is the set of vertices, or channels;

• X[n] is the set of agents connected to n channels (which are given by X(s i ));

• X(ι n,a ) is the set of input actions by some n-ary agent on its ath channel;

• X(o m,c,d ) is the set of output actions by some m-ary agent on its cth channel of its a,m,c,d ) is the set of synchronisations between some input and some output on a common channel; • X(π n ) is the set of forking actions by some n-ary agent; • and similarly for

dth channel; • X(τ n,
(⋆, s 1 ) (⋆, s 2 ) (⋆, s 3 ) ([3], id
X(π l n ), X(π r n ), X(ν n ), X(♡ n )
, and X(τ n ). To see these intuitions at work, let us compute a few categories of elements. Let us start with an easy one, that of [START_REF] Abramsky | Full abstraction for PCF[END_REF] ∈ C (recalling that we implicitly identify any c ∈ C with y c ). An easy computation shows that it is the poset pictured in the top left part of Figure 2. We think of it as a position with one agent ([3], id [START_REF] Abramsky | Full abstraction for PCF[END_REF] ) connected to three channels, and draw it as in the top right part, where the bullet represents the agent, and circles represent channels. Definition 3.2. Positions are finite presheaves empty except perhaps on ⋆ and [n]s.

Let us organise positions into a category, by designing a notion of morphism. We may equip the objects of C with a dimension: ⋆ has dimension 0, any

[n] has dimension 1, all of τ n , π l n , π r n , ♡ n , ι n,a , o n,c,d , ν n have dimension 2, π n has dimension 3, τ n,i,m,j,k has dimension 4.
Definition 3.3. We accordingly define the dimension of a presheaf X on C to be the lowest n ∈ N such that for any m ∈ C of dimension strictly greater than n, X(m) = ⊘.

A position is thus equivalently a finite presheaf in [C op , set] of dimension at most 1. An interface is one of dimension 0.

Definition 3.4. A map in Ĉ is 1-injective iff it is injective in all strictly positive dimensions.
A morphism of positions is a 1-injective morphism in Ĉ. The intuition for a morphism X → Y between positions is thus that X embeds into Y , possibly identifying some channels. Definition 3.5. Positions and morphisms between them form a category D h .

Returning to our explanation of C through categories of elements, let us consider that of π 2 . It is the poset generated by the left-hand graph in the second row of Figure 2 (omitting base objects for conciseness). We think of it as a binary agent (lt) forking into two agents (ls and rs), and draw it as on the right. The equation lt = rt ensures that π l 2 and π r 2 are performed by the same agent. The graphical convention is that a black triangle stands for the presence of id π 2 , l, and r. Below, we represent just l as a white triangle with only Another category of elements, characteristic of the π-calculus, is the one for synchronisation τ n,a,m,c,d . The case (n, a, m, c, d) = (1, 1, 3, 2, 3) is the poset generated by the graph at the bottom left of Figure 2, which we will draw as on the right. The left-hand ternary agent x outputs its 3rd channel, here β, on its 2nd channel, here α. The right-hand unary agent y receives the sent channel on its unique channel, here α. Both agents have two occurrences, one before and one after the action, respectively marked as x x ′ and y y ′ . Both x and x ′ are ternary here, while y is unary and y ′ , having gained knowledge of β, is binary. There are actually three actions here, in the sense that there are three higher-dimensional elements. The first is the output action ǫ from x to x ′ , graphically represented as the middle point of (intended to evoke the point where β enters channel α). The second is the input action ρ from y to y ′ , graphically represented as the middle point of (where β exits channel α). The third action is the synchronisation itself, which 'glues' the other two together, as represented by the squiggly line.

♡ ♠ [p] π l p [p] [p] π r p [p] [m] o m,c,d [m] [n + 1] ι n,a [n] [p] ♡ p [p] [p] τ p [p] [p + 1] ν p [p]
We leave the computation of other categories of elements as an exercise to the reader. The remaining string diagrams are depicted in the top row of Figure 3, for p = 2 and (n, a, m, c, d) = (1, 1, 3, 2, 3). The first two are views, in the game semantical sense, of the fork action π 2 explained above. The next two, o m,c,d (for 'output') and ι n,a (for 'input'), respectively are views for the sender and receiver in a synchronisation action. The τ p action is a silent, dummy action standard in π-calculus. The ♡ p action is the special 'tick' action used for defining fair testing equivalence. The last one, ν p , is a channel creation action.

3.2.

From string diagrams to actions. In the previous section, we have defined our category of string diagrams as Cf , and provided some intuition on its objects. The next step is to construct a bicategory whose objects are positions, and whose morphisms represent traces. We start in this section by defining in which sense higher-dimensional objects of C represent actions, and continue in the next one by explaining how to compose actions to form traces. Actions are defined in two stages: seeds, first, give their local form, their global form being given by embedding into bigger positions.

To start with, until now, our string diagrams contain no information about the 'flow of time', although we mentioned it informally in the previous section. To add this information, for each string diagram M representing an action, we define its initial and final positions, say X and Y , and view the whole action as a cospan Y s → M t ← X. We have taken care, in drawing our pictures before, of placing initial positions at the bottom, and final positions at the top. So, e.g., the initial and final positions for the example synchronisation of Figure 2 are as follows.

↝

They map into (the representable presheaf over) τ 1,1,3,2,3 , yielding the cospan

Y s → τ 1,1,3,2,3 t ← X.
We leave it to the reader to define, based on the above pictures, the expected cospans for forking and synchronisation

[p] [p] π p [p] [m] c,d a,n+1 [n + 1] τ n,a,m,c,d [m] c a [n]
plus the remaining ones specified in the bottom row of Figure 3. Initial positions are at the bottom, and we use: We now define actions from seeds by embedding the latter into bigger positions. E.g., we allow a fork action to occur in a position with more than one agent. Definition 3.8. The interface I F of a presheaf F ∈ Ĉ is F (⋆)⋅⋆, the F (⋆)-fold coproduct of ⋆ with itself, or in other words the position consisting solely of F 's channels. The interface

of a seed Y s → M t ← X is I X .
Since channels occurring in the initial position remain in the final one, we have for each seed a cone from I X to the seed. For any morphism of positions I X → Z, pushing the cone along I X → Z using the universal property of pushout as in

Y Y ′ M M ′ I X Z X X ′ (3.1) yields a new cospan, say Y ′ → M ′ ← X ′ .
Definition 3.9. Let actions be all such pushouts of seeds.

I [2] [2] + ⋆ π 2 M ′ is . x 1 x 2 x y c a=a ′ b=b ′
The meaning of such an action is that x forks while y is passive.

Example 3.11. Because we push along initial channels, the interface of a seed may not contain all involved channels. E.g., in an input action (not part of any synchronisation), the received channel cannot be part of the initial position.

3.3.

From actions to traces. Having defined actions, we now define their composition to yield our bicategory D v of positions and traces. Consider Cospan( Cf ), the bicategory which has as objects all finite presheaves on C, as morphisms X → Y all cospans X → U ← Y , and obvious 2-cells. Composition is given by pushout, and hence is not strictly associative.

Notation 3.12. By convention, the initial position is the target of the morphism in Cospan( Cf ). We denote morphisms in Cospan( Cf ) with special arrows Y X; composition and identities are denoted with • and id • , which matches the notation of pseudo double categories (Section 2.4). Definition 3.13. A trace is any cospan in Cf which is isomorphic to some finite, possibly empty composite of actions in Cospan( Cf ). Let D v denote the subbicategory of Cospan( Cf ) obtained by restricting to positions, traces, and 1-injective 2-cells. Thus, arrows X → Y in D h denote embeddings of X into Y (up to identification of channels), whereas arrows Y X in D v denote traces with X initial and Y final. Intuitively, composition in D v glues string diagrams on top of each other, which yields a truly concurrent notion of trace: the only information retained in a trace about the order of occurrence of actions is their causal dependencies.

Example 3.14. Composing the action of Example 3.10 with a forking action by y yields the first string diagram of Figure 4, which shows that the ordering between remote actions is irrelevant. To illustrate how composition retains causal dependencies between actions, consider the second string diagram. It is unfolded for readability: one should identify both framed nodes, resp. both circled ones. In the initial position, there are channels a, b, and c, and three agents x(a, b), y(b), and z(a, c) (channels known to each agent are in parentheses). In a first action, x sends a on b, and y receives it. In a second action, z sends c on a, and the avatar y ′ of y receives it. The second action is enabled by the first, by which y gains knowledge of a.

Before going on to construct the base double category for our playground, let us observe the following two basic facts about traces. Proof. We proceed by induction on the number of actions involved in any decomposition of U . The base case is trivial. For the induction step, because composition of cospans is by pushout, the result follows from the induction hypothesis, stability of monos under pushout and composition, and the fact that the result holds for actions. The latter in turn follows from the fact that monos are stable under pushout (again!), the pushout lemma, and the fact that the result holds for seeds, which holds by case inspection.

Lemma 3.16. For any trace Y s → U t ← X, s ⋆ is an isomorphism.
Proof. Similar to the previous proof.

The intuition behind the last lemma is that no channel is forgotten during the play.

3.4.

The main double category. At last, we define the base double category D of our playground for the π-calculus. It is a sub-double category of a double category of cospans in Ĉ.

Consider the double category D 0 with • positions as objects,

• horizontal morphisms X → Y given by all natural transformations h∶ X → Y ,

• vertical morphisms X Y given by cospans

X s → U t ← Y in Ĉ,
• and double cells U → V given by commuting diagrams

X ′ Y ′ U V X Y . s U k t U h l s V t V (3.
→ P t ← X and n ∈ N, Y [n]
consists of all elements of P [n] which are not in the image of (the action of) any map in V 0 . Now, consider any double cell as in (3.2). Because s V is monic, U × V Y ′ may be chosen to be just l -1 (Y ′ ) ⊆ U . By Lemma 3.15 and standard cancellation properties of monos, the mediating arrow X ′ → U × V Y ′ is mono. To show that it is epi, we proceed pointwise. Over ⋆, the result follows from s U and s V being isomorphisms (Lemma 3.16). Over

[n], if x ∈ (U × V Y ′ )[n] then x ∈ U [n], and l(x) ∈ V [n]
is not in the image of (the action of) any t ∈ V 0 . But if there existed y such that y ⋅ t = x, then by naturality we would have l(y) ⋅ t = l(x), contradicting the latter. Any natural transformation being both epi and mono is an isomorphism, hence the result. Lemma 3.21. In Set, consider any cube

I B A C I ′ B ′ A ′ C ′ , f
with the marked pushouts and pullback, and with all arrows mono except perhaps f . Then, f is also mono and the front square is also a pullback.

Proof. Any such cube is naturally isomorphic to some cube of the shape

I I + R I + Y I + Y + R I + X I + X + S I + X + Z I + X + Z + S, inj l inj l inj l +k I+h f =I+h+k
the only non-trivial point being that the map I + R → I + X + S has the given shape. But this is because we know that its pullback along I + X → I + X + S is inj l , so the image of R has to lie in S.

Corollary 3.22. Consider any cube

X B A C X ′ B ′ A ′ C ′ , f
in Ĉ in which all arrows except perhaps f are 1-injective, and the marked squares are pushouts, resp. pullbacks. Then f is also 1-injective.

Proof. We proceed pointwise. On any object C of dimension > 0, we obtain a diagram in sets for which the lemma applies.

Codomain is a fibration

In this section, we prove that the double category D of traces constructed in the previous section satisfies the primary axiom for playgrounds, namely that the codomain functor D H → D h is a fibration. We proceed as follows. We first define a (strong) factorisation system on Ĉ (Section 4.1), from which we derive in Section 4.2 an intermediate sub-double category D ↪ D 1 ↪ D 0 . We further show that by the properties of factorisation, the codomain functor D 1 H → D 1 h is a fibration. Finally, we want to show that D H → D h is a fibration by proving that traces are stable under relevant cartesian lifting in D 1 , i.e., cartesian liftings of any trace along any morphism in D h are again in D H . We first check this for seeds, by case analysis, in Section 4.3. In order to generalise to actions M ∶ Y X, the basic idea is to

(1) decompose X as a pushout of X 0 , where the generating seed M 0 takes place, and Z, which is passive; (2) decompose the morphism along which we want to restrict, say h∶ X ′ → X, accordingly, say as h 0 ∶ X ′ 0 → X 0 and h Z ∶ Z ′ → Z; (3) restrict M 0 along h 0 to obtain P ′ 0 ; (4) recompose a trace P ′ from P ′ 0 and Z ′ ; (5) check that P ′ admits a cartesian morphism to M .

Step ( 4) is non-trivial, so we devote Section 4.4 to it. It works as a kind of formal opposite to restriction, as we essentially lift P ′ 0 along h 0 ∶ X ′ 0 → X ′ . We call this an oplifting of P ′ 0 along h 0 , by analogy with lifting in opfibrations. However, opliftings do not enjoy the relevant universal property (opcartesianness, which is dual to cartesianness). Instead, we find that opliftings are in fact cartesian! In Section 4.5, we use opliftings to show that actions are stable under restriction, following the above plan. Finally, we extend the result to arbitrary traces in Section 4.6. 4.1. A factorisation system. Let us start by defining the (strong) factorisation system (V, H) on Ĉ, on which the intermediate sub-double category D 1 will be based. The idea is that all three components of cartesian morphisms in D H are in H, while t-legs of vertical morphisms are in V. The cartesian lifting of any V ∶ Y ′ Y as in (3.2) along any h∶ X → Y is then given by factoring t V ○ h as l ○ t U with t U ∈ V and l ∈ H to obtain

X ′ Y ′ U V X Y, k l h s U s V t U t V (4.1)
where the upper square is a pullback. We recall from Definition 3.19 that V 0 denotes the set of 't'-legs (i.e., lower legs) of seeds. Following Bousfield's [START_REF] Bousfield | Constructions of factorization systems in categories[END_REF] construction of 'cofibrantly generated' factorisation systems, we define H = V 0 to be the class of maps f such that for any t ∈ V 0 and commuting square (u, v)∶ t → f in Ĉ→ , there exists a unique filler h making the following diagram commute:

X X ′ Y Y ′ . u t v f h
In this situation, one says that f is right-orthogonal to t, and t is left-orthogonal to f , which is denoted by t f . We finally define V = H to consist of all maps which are left-orthogonal to any map in H. Of course, we have V 0 ⊆ V. The following is an application of [8, Theorem 4.1]: Proposition 4.1. The pair (V, H) forms a factorisation system.

What does that mean? Here is a modern definition [START_REF] Freyd | Categories of continuous functors, I[END_REF]: Definition 4.2. The classes of maps V and H form a factorisation system iff V = H, V = H, and any arrow factors as h ○ v with h ∈ H and v ∈ V.

In the case where H = V 0 and V = H, Bousfield proves that any map in Ĉ admits a factorisation using a transfinite construction (a so-called small object argument). But here we will only need factorisations of particular morphisms, which we will actually be able to calculate by hand. Bousfield's results include: Lemma 4.3. V is stable under pushout and composition, contains all isomorphisms, and enjoys the right cancellation property, i.e., if v ∈ V and f v ∈ V, then f ∈ V.

H is stable under pullback and composition, contains all isomorphisms, and enjoys the left cancellation property, i.e., if h ∈ H and hf ∈ H, then f ∈ H. Remark 4.4. Stability under pushout is ambiguous here: we mean that for any pushout

X Y Z T , v v ′ if v ∈ V, then v ′ ∈ V.
Stability under pullback is defined dually.

4.2.

A first 'fibred' double category. We now make concrete the idea evoked in the previous section, of using our factorisation system to obtain a codomain fibration. Consider the sub-double category D 1 of D 0 obtained by restricting vertical morphisms to cospans X Proof. Indeed, consider any h∶ X → Y in D h . There cannot be any commuting square

X 0 X U Y u t v h
with t ∈ V 0 , because U is a representable presheaf of dimension > 1 and Y has dimension ≤ 1, so there cannot be any v∶ U → Y .

4.3. Restriction of seeds. We now show that restrictions of seeds (in the sense of D 1 ) are traces.

Lemma 4.9.

Consider any diagram X ′ h → X t → M , where t ∈ V 0 and h ∈ D h (X ′ , X). Its factorisation X ′ t ′ → M ′ h ′ → M with t ′ ∈ V and h ′ ∈ H is such that h ′ is 1-injective
and the obtained restriction is a trace of length at most 2. If X ′ is an individual, i.e., a position of shape [n], then it is isomorphic to some seed. If X ′ is an interface, then the restriction is an equivalence (in D v ).

Proof. We proceed by case analysis. In each case, one has to check that h ′ is 1-injective, that X ′ individual implies t ′ seed, that X ′ interface implies that t ′ is an isomorphism, and that the upper leg of the obtained cospan is as expected: this is routine so we mention it here once and for all.

Let us first treat the case where M = y c , for c not of the shape τ n,i,m,j,k . Then, we have X = [n] for some n. If id c ∈ Im(th), then X ′ ≅ [n] + I for some interface I (since h is 1-injective). Consider the diagram

M + I M [n] + I [n].
[id,tk]

t+id I h=[id,k] t
The map t + id I is in V by Lemma 4.3, so we just have to prove that [id, tk] is in V 0 , which is a simple verification.

If now id c ∉ Im(h), then X ′ is an interface, and the relevant factorisation is

X ′ M X ′ [n], t○h id h t (4.2)
because t ○ h is easily checked to be in V 0 . The case of τ n,i,m,j,k is a bit more complicated. Here, t is actually t 0 = [ρt, ǫt]. First of all, if X ′ is an interface, then we obtain a factorisation analogous to (4.2). Consider now the case where Im(h) contains both agents of [n] i j [m]. Let x denote the n-ary one and y denote the m-ary one (in

X ′ ). If x ⋅ s i = y ⋅ s j , then X ′ = ([n] i j [m]
) + I for some interface I and the required factorisation is easily seen to be

τ n,i,m,j,k + I τ n,i,m,j,k ([n] i j [m]) + I [n] i j [m]. [id,t 0 k] t 0 +id I h=[id,k] t 0
Consider now the case where X ′ still contains both agents but x ⋅ s i ≠ y ⋅ s j . Then X ′ = [n] + [m] + I for some interface I, and the required factorisation is

ι n,i + o m,j,k + I τ n,i,m,j,k [n] + [m] + I [n] i j [m]. [ρ,ǫ,t 0 k] t+t+id I [x,y,k] t 0
The only non-trivial point here is to show that [ρ, ǫ, t 0 k] is in V 0 , which easily reduces to showing that there is no commuting square

[n] i j [m] ι n,i + o m,j,k + I τ n,i,m,j,k τ n,i,m,j,k , u t 0 v [ρ,ǫ,t 0 k]
which is true because there is no such u.

The cases where X ′ only contains one agent of [n] i j [m] are similar to the latter case: if it contains x then the factorisation is through ι n,i , and otherwise it is through o m,j,k . 4.4. Opliftings. We now aim at extending Lemma 4.9 from seeds to actions. Consider an arbitrary action Y → M ← X, obtained by pushing some seed Y 0 → M 0 ← X 0 along I X 0 → Z. Consider now a morphism h∶ X ′ → X in D h , along which we wish to restrict M . As explained at the beginning of Section 4, our strategy is to consider the pullback

X ′ 0 X 0 X ′ X.
Indeed, the part of X really concerned by M is the image of X 0 , so we would like to first restrict M 0 to X ′ 0 using Lemma 4.9, and then extend it to X ′ . The present section is devoted to constructing the second step, the extension of (M 0 ) X ′ 0 to X ′ , which we call an oplifting of (M 0 ) X ′ 0 along X ′ 0 → X ′ . In the general case, we want to compute the oplifting of Y → U ← X along h∶ X → X ′ . Because h is 1-injective, we can complete the solid part of

I X Z X X ′ ⊆ h ⊆ into a pushout. Indeed, we take Z(⋆) = X ′ (⋆), Z[n] = X ′ [n] ∖ Im(h [n]
) for all n, and I X → Z is uniquely determined by h ⋆ . In passing, we have:

Lemma 4.10. This pushout is uniquely determined up to canonical isomorphism by h alone.

Then, we observe that, because U is a trace,

I X → X → U factors through Y → U .
Definition 4.11. Let the oplifting of U ∶ Y X along h∶ X → X ′ be the cospan obtained as in (3.1) by pushing U along I X → Z.

All horizontal maps are 1-injective by construction, and we have:

Lemma 4.12. The obtained cospan Y ′ → U ′ ← X ′ is a trace.
Proof. We start by showing that U ′ is an action if U is. So assume U is obtained by pushing a seed Y 0 → M 0 ← X 0 along some I X 0 → Z 0 . Then, Z 0 → X is surjective on ⋆ because I X 0 → X 0 is and epis are stable under pushout in presheaf categories. Thus,

I X → X factors through Z 0 → X. Let Z ′′ denote the pushout I X Z 0 Z Z ′′ .
By the pushout lemma, Y ′ → U ′ ← X ′ is isomorphic to the cospan obtained by pushing Y → U ← X along Z 0 → Z ′′ . By the pushout lemma again, it is isomorphic to the cospan obtained by pushing Y 0 → M 0 ← X 0 along I X 0 → Z 0 → Z ′′ . Thus, it is indeed an action. We now prove the general case by induction on U . This is trivial if U is isomorphic to an identity. If now U is a composite Z V Y M X, then we compute the oplifting of M along h to obtain a double cell, say

Y Y ′ X X ′ , h ′ M h M ′ α M by pushing M along some morphism I X → Z 1 making I X Z 1 X X ′ h into a pushout.
The crucial insight is then that by computing the following pushout Z 2 and applying its universal property, we obtain a diagram

I X I Y Y Z 1 Z 2 Y ′ (4.3)
whose exterior is a pushout by construction. So by the pushout lemma the right-hand square is again a pushout, which by Lemma 4.10 is the unique pushout along which to push V to compute the oplifting of V along h ′ , say

Z Z ′ Y Y ′ . h ′′ V h ′ V ′ α V
By induction hypothesis, V ′ is again a trace. But by the pushout lemma again, α V is also what we obtain by pushing V along the exterior rectangle of (4.3). A bunch of applications of the pushout lemma finally yields that α M •α V is the oplifting of M •V along h, so M ′ •V ′ is a trace by construction.

Although opliftings have an opcartesian flavour, they are in fact not opcartesian in general, and moreover opcartesian liftings do not exist in general.

Example 4.13. Consider the oplifting of the seed

ι 1,1 along [1] ↪ [1] 1 1 [1], say ι 1,1 1 1 [1], whose final position is [2] 1 1 [1]. To see that it is not opcartesian, consider the diagram [2] 1,2 1,1 [1] [2] [2] 1 1 [1] τ 1,1,1,1,1 ι 1,1 ι 1,1 1 1 [1] [1] 1 1 [1] [1] [1] 1 1 [1].
In this case, opcartesianness would mean finding dashed arrows rendering the diagram commutative. There is indeed a unique arrow [START_REF]Proc. 11th Symposium on Logic in Computer Science[END_REF] fits. Indeed, there is only one arrow of the given type, and it does not make the relevant square

ι 1,11 1 [1] → τ 1,1,1,1,1 making the corresponding square commute, but then no arrow [2] 1 1 [1] → [2] 1,2 1,1
[2] 1 1 [1] [2] 1,2 1,1 [1] ι 1,1 1 1 [1] τ 1,1,1,1,1
commute, because one side (down; right) of the square maps the unary player to ρ ○ t, while the other (right; down) maps it to ρ ○ s. This shows that ι 1,1 1 1 [START_REF]Proc. 11th Symposium on Logic in Computer Science[END_REF] is not an opcartesian lifting of ι 1,1 . But in fact, ι 1,1 1 1 [START_REF]Proc. 11th Symposium on Logic in Computer Science[END_REF] and

τ 1,1,1,1,1 are two liftings of ι 1,1 along [1] ↪ [1] 1 1 [1].
Thus, any opcartesian lifting should have a final position mapping both to [2] 1 1 [START_REF]Proc. 11th Symposium on Logic in Computer Science[END_REF] and [2] 1,2 1,1 [START_REF]Proc. 11th Symposium on Logic in Computer Science[END_REF], hence containing just one, binary player: no trace can meet this requirement.

However, even though they are not opcartesian, opliftings are in fact cartesian. Let us now show this, starting with a few preliminary results.

(n,x)∈Agents(X) [n] [x] (n,x) → X is epi.
Proof. This is trivial except in dimension 0, where it holds by case inspection.

Corollary 4.16. For all arrows as in

X U C U ′ h h ′ t g f in Ĉ such that f is 1-injective, t ∈ V 0 , and f h = gt = f h ′ , we have h = h ′ .
Proof. We construct the diagram

∑ (n,x)∈Agents(X) [n] U X U C U ′ , he h ′ e e h h ′ t f g
and observe that h ′ e = he by 1-injectivity of f , hence h = h ′ because e is epi by Lemma 4.15.

Lemma 4.17. Opliftings of traces are cartesian.

Proof. Consider any oplifting

U f → U ′ of Y → U ← X along, say X → X ′ . By Lemma 4.
→ M t ← X and h ∈ D h (X ′ , X), the factorisation X ′ t ′ → P ′ h ′ → M of th with t ′ ∈ V and h ′ ∈ H is such that h ′ is 1-injective
and the obtained restriction is a trace of length at most 2. If X ′ is an individual then it is either a seed or an equivalence; if X ′ is an interface then it is an equivalence.

Proof. Consider any action Y → M ← X obtained by pushing the following seed-withinterface along I → Z:

I Y 0 M 0 X 0 .
By Lemma 4.17, the morphism M 0 → M is cartesian. Consider the pullback of the bottom square below along h∶ X ′ → X to obtain the top square

I ′ Z ′ X ′ 0 X ′ I Z X 0 X, f
which, because presheaf categories are adhesive [START_REF] Lack | Adhesive categories[END_REF] and I → X 0 is mono, is again a pushout. Furthermore, consider the front face, which is a pullback in D h . By Lemma 4.9, restricting M 0 along X ′ 0 → X 0 yields a trace, say

Y ′ 0 → P ′ 0 ← X ′ 0 with a morphism to Y 0 → M 0 ← X 0 in D H . Since it is a trace, I ′ ↪ X ′ 0 ↪ M ′ 0 factors through Y ′ 0 ↪ M ′ 0 . Pushing Y ′ 0 → P ′ 0 ← X ′ 0 along I ′ → Z ′
, we obtain a trace Y ′ → P ′ ← X ′ (we may choose X ′ as initial position because the top square above is a pushout) with a morphism from Y ′ 0 → P ′ 0 ← X ′ 0 in D H , which is an oplifting, hence cartesian (by Lemma 4.17). Then, by universal property of pushout we obtain a unique morphism f ∶ P ′ → M making the following cube commute:

I ′ Z ′ P ′ 0 P ′ I Z M 0 M .
f By Corollary 3.22, f is 1-injective, which entails that the induced morphism of traces is in D H . We now need to show that P ′ → M is cartesian, which by Lemmas 3.20 and 4.7 amounts to showing that its middle arrow f ∶ P ′ → M is in H. To this end, consider any morphism t∶ Z ′′ → C in V 0 and morphism (u, v)∶ t → f in Ĉ→ . First of all, because M 0 → M is identity in dimensions > 1, the morphism v uniquely factors through M 0 → M . Furthermore, in all cases where f 0 ∶ P ′ 0 → M 0 is identity in dimensions > 1, the Yoneda lemma entails that C → M 0 uniquely factors through P ′ 0 . This yields a diagram

Z ′′ P ′ 0 P ′ C M 0 M l u v k f 0 g f ?
which commutes except perhaps for the upper part marked '?'. But the latter also commutes by Corollary 4.16 with h = u and h ′ = gl. We thus obtain a lifting, which is unique by 1injectivity of f . So what happens when is f 0 non-identity in dimensions > 1? By inspection of the proof of Lemma 4.9, except for the easy case where P ′ 0 ≅ X ′ 0 , this is when M 0 = τ n,i,m,j,k for some n, m, i, j, k, and P ′ 0 has one of the shapes ι n,i + J, o m,j,k + J, or ι n,i + o m,j,k + J, for some interface J. In the first two cases, C ≠ τ n,i,m,j,k because there can be no u∶ [n] i j [m] → P ′ (one agent is missing in P ′ ), so the previous argument applies. In the third case, letting x and y respectively denote the n-and m-ary initial agents in P ′ 0 and a = x ⋅ s i and a ′ = y ⋅ s j the corresponding channels, one easily shows that g(a) ≠ g(a ′ ), so again there can be no u∶ [n] i j [m] → P ′ . Thus, C ≠ τ n,i,m,j,k and the previous argument again applies. 4.6. Restriction of traces. So far, we have shown that seeds and actions admit cartesian liftings in D H . We now show that it is also the case for arbitrary traces. We proceed by induction on the length of the considered trace, which requires a few preliminary results. Corollary 4.20. In any presheaf category, in any commuting cube

I B A C I ′ B ′ A ′ C ′ , f
with the marked pushouts, pullback, and mono, the front square is also a pullback.

Proof. It suffices to show the result in sets, as all involved properties are pointwise in presheaf categories. First, as monos are stable under pullback and pushout, I → B, A → C, and A ′ → C ′ are also monos. Furthermore, pushouts along monos are also pullbacks, so the top and bottom faces are also pullbacks. By the pullback lemma, the rectangle

I I ′ A ′ B B ′ C ′
is a pullback. The previous lemma thus entails the result.

Lemma 4.21. For any commuting diagram as the solid part of

T V ′ U ′ C V U t h f k
with t ∈ V 0 , h ∈ H, and f 1-injective, there is a unique lifting k as shown.

Proof. Because h ∈ H, there is a unique map from k ′ ∶ C → V ′ making both triangles commute. By composing k ′ with V ′ → U ′ , we obtain a lifting k for the desired square. Uniqueness follows from 1-injectivity of f .

Lemma 4.22. The codomain functor cod∶

D H → D h is a subfibration of cod∶ D 1 H → D 1 h .
Proof. First of all, it is sufficient to prove that given any trace Y s → U t ← X and h ∈ D h (X ′ , X), any cartesian lifting in D 1 lies in D, i.e., the obtained vertical morphism is again a trace and the double cell to U lies in D (i.e., all its components are 1-injective). Indeed, mediating morphisms computed in D 1 are automatically in D by cancellation.

We proceed by induction on U . If U is an equivalence, then the result is obviously true. Otherwise, U = M • V for some action M and trace V . Let us call Z the final position of M . By Lemma 4.18, M admits a lifting P ′ along h, with a final position Z ′ , and Z ′ → Z and f M ∶ P ′ → M are 1-injective. By induction hypothesis, V admits a lifting V ′ along Z ′ → Z with a double cell to V in D H . Therefore, considering the composite

P ′ • V ′ , we have a commuting diagram Y ′ Y V ′ V P ′ • V ′ M • V Z ′ Z P ′ M X ′ X, t 0 s 0 t 1 s 1 t 2 s 2 f M t ′ 2 f V s ′ 2 f
where f is obtained by universal property of pushout.

Because pushouts along monos are also pullbacks in presheaf categories, both marked pushouts are also pullbacks. Furthermore, by Lemma 3.20,

Z ′ = P ′ × M Z and Y ′ = (V ′ × V Y ), as shown. Also, by Corollary 4.20, V ′ = (P ′ • V ′ ) × M •V V , as shown. Furthermore, by Proposition 3.18, f is 1-injective.
By Lemmas 4.7 and 3.20, it suffices to show that f is in H, i.e., that it is right-orthogonal to any T t → C in V 0 . Consider any commuting square

T P ′ • V ′ C M • V. t u v f
Since M • V is the coproduct of M and V in dimensions greater than 1 and C is a representable of dimension greater than 1, we have that v factors either through t 2 or s 2 .

If v factors through s 2 , then by universal property of pullback we find a map

u ′ ∶ T → V ′ making T V ′ P ′ • V ′ C V M • V u ′ t u v s 2
commute. Then, by Lemma 4.21, we find a unique lifting as desired.

If v factors as t 2 v ′ , then by Lemma 4.21, it is sufficient to show that there is a map u ′ ∶ T → P ′ making

T P ′ P ′ • V ′ C M M • V u ′ t u v ′ v t ′ 2 t 2 f commute.
To that end, it is sufficient to show that for every [n]

x → T , there is a map

[n] fx → P ′ such that [n] T P ′ P ′ • V ′ x fx u t ′ 2 (4.4)
commutes. Indeed, if that is the case, then the square

∑ (n,x)∈Agents(T ) [n] T P ′ P ′ • V ′ [x] (n,x)∈Agents(T ) [fx] (n,x)∈Agents(T ) u t ′ 2 u ′
also commutes, and since its bottom map is mono and its top map is epi by Lemma 4.15, there is a unique lifting u ′ ∶ T → P ′ making both triangles commute. The square

T P ′ C M t u ′ v ′
also commutes because it commutes when composed with t 2 , which is mono.

So we now need to show that for every [n]

x → T , there is a map [n] fx → P ′ making the square (4.4) commute. Because

P ′ + V ′ [t ′ 2 ,s ′ 2 ] → P ′ • V ′ is epi and [n] is a representable presheaf, [n] ux → P ′ • V ′ factors through either t ′ 2 or s ′ 2 . If it factors through s ′ 2 , say as s ′ 2 x ′ , then we have t 2 (v ′ tx) = vtx = f ux = f s ′ 2 x ′ = s 2 f V x ′ ,
so by universal property of the pullback Z there exists a unique

x ′′ ∶ [n] → Z such that s 0 x ′′ = v ′ tx and t 1 x ′′ = f V x ′ . We thus obtain a commuting diagram [n] Z T C M, x x ′′ t v ′ s 0
which is impossible because v ′ tx, as one of the agents performing action C in M , cannot remain in the final position of M . Thus, ux factors through t ′ 2 and we are done.

A playground for π

In the previous section, we have proved the main playground axiom, asserting that the codomain functor D H → D h of the double category of traces constructed in Section 3 is a fibration. We now prove the remaining axioms. In Section 5.1, we equip D with playground structure and prove that it satisfies all the needed axioms, except both decomposition axioms ((P6) and (P7)) which require a bit more work. In Section 5.2, we establish a correctness criterion detecting when a given cospan in Ĉ is a trace. We then use this criterion in Section 5.3 to prove both remaining axioms.

5.1.

A candidate playground. So we start in this section by defining the needed additional structure on D.

Definition 5.1. We recall from Lemma 4.9 that I, the set of individuals, consists of representable positions [n]. Let B, the full subcategory of basic actions, span all seeds of shape τ n , π r n , π l n , ν n , ♡ n , ι n,i , or o m,j,k . Full actions (notation F) are all actions obtained from seeds of shape τ n , π n , ν n , ♡ n , ι n,i , o m,j,k , or τ n,i,m,j,k . Closed-world actions are all actions obtained from seeds of shape τ n , π n , ν n , ♡ n , or τ n,i,m,j,k . Let W denote the graph with positions as vertices and closed-world actions between them as edges (the initial position being the target). Finally, all decompositions of any trace U into actions have the same length which we denote by U .

Here is a summary of which actions are basic, full and closed-world:

τ n π l n π r n π n ι n,i o m,j,k τ n,i,m,j,k ν n ♡ n Basic ✓ ✓ ✓ ✓ ✓ ✓ ✓ Full ✓ ✓ ✓ ✓ ✓ ✓ ✓ Closed-world ✓ ✓ ✓ ✓ ✓ .
Remark 5.2. The definition matches the explanations following Definition 2.30. Basic actions are as small as possible, which here means they start from one agent and only retain one agent in the final position. Full actions are those that retain all possible agents in the final position. So the only kind of actions which are not basic are π n and τ n,i,m,j,k . They each have one sub-action for each agent in their final positions, namely π r n and π l n for π n , and ι n,i and o m,j,k for τ n,i,m,j,k . All of these sub-actions are basic, but only ι n,i and o m,j,k are full. Finally, a new class of actions appear here, that of closed-world actions. Intuitively, it consists of those actions that do not involve any interaction with the environment. Or, in other words, those that cannot be extended, even by adding new agents. E.g., ι n,i may be completed to τ n,i,m,j,k by adding an agent, hence is not closed-world. But τ n,i,m,j,k is. Closed-world actions will be at the basis of our semantic notion of testing equivalence (Definition 6.24). Lemma 5.3.

• (P1) I, viewed as a subcategory of D h , is discrete. Basic actions have no nontrivial automorphisms in D H . Vertical identities on individuals have no non-trivial endomorphisms. • (P2) (Individuality) Basic actions have individuals as both domain and codomain. • (P3) (Atomicity) For any cell α∶ U → U ′ , if U ′ = 0 then also U = 0. Up to a special isomorphism in D H , all traces of length n > 0 admit decompositions into n actions. For any U ∶ X Y of length 0, there is an isomorphism id

• X → U in D H as in X X X Y . U Ū α U
• (P4) Restrictions of actions (resp. full actions) to individuals either are actions (resp. full actions), or have length 0.

Proof. (P1) and (P2) are direct by Yoneda. (P4) is also easy in view of Lemma 4.22 and its proof. For (P3), any vertical X → U ← Y of length 0, being a trace, is isomorphic to an identity cospan, say Z → Z ← Z. To construct α U , just take the composite id

• X ≅ → id • Z ≅ → U .
Let us now treat the axiom for views, which is really easy. It actually becomes stronger because of Remark 2.28, though this does not affect the rest of the construction: Proof. The result holds for seeds, by case analysis. E.g., v ls,πn = π l n , v rs,πn = π r n , and so on. Now, any action M comes with a cell from its generating seed, say β∶ M 0 → M . If y is in the image of M 0 , then the required cell α y,M is β ○ α y,M 0 . Otherwise, v y,M = id • d admits a cell to M , which suits our needs. Uniqueness follows by (P1).

Remark 5.6. The important result that Axiom (P5) entails [START_REF] Hirschowitz | Full abstraction for fair testing in CCS (expanded version)[END_REF]Proposition 4.24] says that when we replace M with any trace u, we get a double cell α y,u which is only unique up to isomorphism. Below, we still define views up to isomorphism, so our modified Axiom (P5) does not make this any stronger.

We conclude this section with the (straightforward) verification of (P8) and (P9). Proof. By case analysis. E.g., if b = π l n , then M ≅ π n ≅ M ′ . Remark 5.9. While the verification of (P9) is straightforward in our case, this axiom does impose strong constraints on playgrounds. Morally, it demands that the basic subactions of a given full action should be disjoint from those of a different full action. To see why this is restrictive, let, for all j ∈ n, ι n,i,j denote the quotient of ι n,i by the equation s ○ s n+1 = s ○ s j . The equation says that the received channel was already known as channel number j.

Further let [n] {i = j} denote [n] quotiented by s i = s j . We could be tempted to decree that the cospan

[n + 1] {n + 1 = j} s → ι n,i,j t ← [n]
is an action. An example consequence would be that, e.g., the synchronisation on [n] i,l j,k

[m] where [m] sends k on j, when restricted to the receiver, would give ι n,i,l instead of ι n,i .

But then ι n,i and ι n,i,l would be two non-isomorphic full actions sharing a common basic subaction, ι n,i .

We now have proved all playground axioms for D, except right and left decomposition. These require the development of more machinery, which we undertake in the next section.

Correctness criterion.

In order to prove the remaining playground axioms for D, we set up a combinatorial characterisation of traces among cospans. Before delving into technicalities, let us briefly map out our correctness criterion. Given a trace Y ↪ U ↩ X, we start by forgetting the cospan structure and exploring the properties of U alone.

The main idea is to construct a binary relation over the elements of U , modeling causality. So, e.g., if an agent x ∈ U [n] forks into x 1 and x 2 , then we will have causal relations

x 1 x 2 r x,
where r denotes the corresponding element in U (π n ). In order for U to admit a sequential decomposition into actions, the main criterion is that the causality relation should be acyclic. In addition to this, a few sanity checks are necessary. First of all, because actions are merely seeds pushed along 1-injective maps from their interfaces, the neighbourhood of each action x ∈ U (µ) should not be too degenerate. For instance, the corresponding map ⌜x⌝∶ µ → U should be 1-injective. Moreover, for inputs and channel creations, the new channel should really be new. This property, which is a bit tedious to define properly, is called local 1-injectivity.

Furthermore, when we add a new action to some trace, it is played by an agent in the final position. This entails that no two actions in U may be performed by the same agent. We call this target-linearity below. Symmetrically, no two actions may share their 'created' agents, which we call source-linearity. Linearity is then the conjunction of sourceand target-linearity.

These conditions are sufficient, in the sense that if any U ∈ Cf has an acyclic causal relation, and is furthermore locally 1-injective and linear, then it is the middle object of a trace. But in fact, it is then easy to determine the corresponding initial and final positions. We design notions of initial and final morphisms, so that Y s → U t ← X is a trace iff U satisfies the above conditions, t is initial, and s is final.

Let us first define the causal relation. A first step is to restrict attention to the cores of U , in the following sense, which are intuitively the main elements. E.g., for a forking action x ∈ U (π n ), keeping track of x is enough, and handling x ⋅ l and x ⋅ r tends to get in the way.

Technically, an input or output is a core iff it is not part of a synchronisation; and a left or right fork action is a core iff it is not part of a full fork action. Here is a concise definition: Definition 5.10. A core of a presheaf U ∈ Ĉ is an element of dimension > 1 which is not the image of any element of higher dimension.

Our definition of the causal relation will rely on the preliminary notions of sources and targets of a core, and that of channels created by a core. These notions will fix the direction of the causal relation. Definition 5.11. For any U and core µ ∈ U (c),

• the sources of µ are the agents x such that x = µ ⋅ f ⋅ s for some f ;

• the targets of µ are the agents y such that y = µ ⋅ f ⋅ t for some f ;

• a channel a ∈ U (⋆) is created by µ iff µ has the shape ν n or ι n,i , and a = µ ⋅ s ⋅ s n+1 .

Example 5.12. In the representable π n , there is one target, l ○ t (or equivalently r ○ t), and two sources, s 1 = l ○ s and s 2 = r ○ s. Another example is τ n,i,m,j,k , which has two targets, ǫ ○ t and ρ ○ t, and two sources. However, ρ ○ s ○ s n+1 is not created by the input element ρ, because it is not a core.

Definition 5.13. For any U , let its causal graph G U have:

• as vertices, all channels, agents, and cores in U ,

• for all x ∈ U [n] and i ∈ n, an edge x → x ⋅ s i ,

• and, for each core µ, an edge from each of its sources and created channels, and one into each of its targets, as in

source 1 source 2 created core target 1 target 2 .
Please note that edges a → µ from a channel to an input action exist only if the involved action is not part of a synchronisation; for otherwise the synchronisation is a core, not the input.

The obtained graph is actually a binary relation, since there is at most one edge between any two vertices. It is also a colored graph, in the sense that it comes equipped with a morphism to the graph L: ∞ 1 0, mapping cores to ∞, agents to 1, and channels to 0. (In particular, there are no edges from channels to agents or from cores to channels.) For any graph G, equipped with a morphism l∶ G → L, we call vertices of G channels, agents, or cores, according to their label.

As expected, we have:

Proposition 5.14. For any trace U , G U is acyclic (in the directed sense).

Proof. By induction on any decomposition of U .

Let us now consider local 1-injectivity, linearity, initiality and finality. First, let us emphasise that for all seeds Y ↪ M ↩ X, M is a representable presheaf, so, e.g., it makes sense to consider U (M ). Definition 5.15. A presheaf U is locally 1-injective iff for any seed Y ↪ M ↩ X with interface I and core µ ∈ U (M ), if two distinct elements of M are identified by the Yoneda morphism µ∶ M → U , then they are in (the image of) I(⋆). This is equivalent to requiring that all morphisms y c → U , for all c ∈ C, are 1-injective, and that for all core inputs and channel creations x of arity n in U , for all i ∈ n, we have

x ⋅ s ⋅ s n+1 ≠ x ⋅ s ⋅ s i .
Proposition 5.16. Any trace U is locally 1-injective.

Proof. Choose a decomposition of U into actions; µ corresponds to precisely one such action, say M ′ , obtained, by definition, from some seed M as a pushout (3.1). By construction of pushouts in presheaf categories, M ′ is obtained from M by identifying some channels according to I → Z.

Let us observe that, because local 1-injectivity is only about cores, an input which is part of a synchronisation may receive an already known channel, even if its n + 1th channel is not part of its interface -because it is not a core.

After local 1-injectivity, let us consider linearity.

Definition 5.17. Any G ∈ Gph L is source-linear iff for any cores µ, µ ′ , and other vertex (necessarily an agent or a channel) x, µ ← x → µ ′ in G, then µ = µ ′ ; G is target-linear iff for any cores µ, µ ′ and agent x, if µ → x ← µ ′ in G, then µ = µ ′ ; G is linear iff it is both source-linear and target-linear.

Proposition 5.18. For any trace

Y s → U t ← X, G U is linear.
Proof. Straightforward, by induction on any decomposition of U into actions, observing that we glue along agents and channels which are initial on one side and final on the other.

The last of our necessary sanity checks is about initiality and finality. The idea here is that one may read in U alone what both legs of the cospan Y ↪ U ↩ X should be. Definition 5.19. An agent is initial in U when it is not the source of any action, i.e., for no action µ ∈ U , x = µ ⋅ s. A channel is initial when it is not created by any core.

An agent x in U is final iff it is not the target of any action, i.e., for no action µ ∈ U , x = µ ⋅ t. All channels are final. Lemma 5.20. An agent is initial in U iff it has no edge to any core in G U . Lemma 5.21. An agent is final in U iff it has no edge from any core in G U . Now, here is the expected characterisation: Theorem 5.22. A monic cospan Y s U t X of finite presheaves is a trace iff (C1) U is locally 1-injective, (C2) X contains exactly the initial agents and channels in U , (C3) Y contains exactly the final agents and channels in U , (C4) and G U is linear and acyclic.

Of course, we have almost proved the 'only if' direction, and the rest is easy, so only the 'if' direction remains to prove. The rest of this section is devoted to this. So given a cospan satisfying the above conditions, we intend to sequentialise it, i.e., decompose it into actions. We will proceed by induction on the number of cores in U , by picking a core µ which is maximal according to G U , removing it from U and applying the induction hypothesis to the rest. However, it may not be obvious how we should remove µ from U . E.g., the topostheoretic difference U ∖ µ does not yield the expected result, as it removes all sources of µ. Instead, we consider the following operation: for any morphism of presheaves

f ∶ U → V and set W , let U -W = ∑ c∈C Im(U (c)) ∖ W ⊆ ∑ c∈C V (c)
. This is a slight abuse of notation, as f is implicit, but it should be easily inferred from context. Remark 5.23. We observe that U -W is generally just a set, not a presheaf; i.e., its elements are not necessarily stable under the action of morphisms in C. Consider for example U = [1] [START_REF]Proc. 11th Symposium on Logic in Computer Science[END_REF] and let W consist of the first agent and the unique channel. Then U -W does not contain the unique channel of U , so the action of s 1 on the second agent steps outside U -W .

But there is one useful case where U -W is indeed a subpresheaf of U , as we show below in Lemma 5.25. Definition 5.24. For any seed Y ↪ M ↩ X, let the past past(M ) = M -Y of M be the set of its elements not in the image of Y . For any such M , presheaf U , and core µ ∈ U (M ), let past(µ) = Im(past(M )) consist of all images of past(M ).

To explain the statement a bit more, by Yoneda, we see µ as a map M → U , so we have a set-function past(M ) ↪ ob(el(M )) → ob(el(U )) (recalling that el denotes the category of elements). We observe that past(µ) is always a set of agents and actions only, since channels present in X always are in Y too.

Given a core µ ∈ U , the relevant way of removing µ from U will be:

U µ = ⋃{V ↪ U ob(el(V )) ∩ past(µ) = ⊘}.
U µ is thus the largest subpresheaf of U not containing any element of the past of µ. The good property of this operation is:

Lemma 5.25. If µ is a maximal core in G U (i.e.
, there is no path to any further core) and

G U is target-linear, then (U µ)(c) = U (c) ∖ past(µ) for all c. Proof. The direction (U µ)(c) ⊆ U (c) ∖ past(µ) is by definition of . Conversely, it is enough to show that c ↦ U (c) ∖ past(µ) forms a subpresheaf of U , i.e., that for any f ∶ c → c ′ in C, and x ∈ U (c ′ )∖past(µ), x⋅f ∉ past(µ). Assume on the contrary that x ′ = x⋅f ∈ past(µ).
Then, of course f cannot be the identity, and w.l.o.g. we may assume that x ′ is an agent and x is a core. But then, because x ′ ∈ past(µ), there is an edge µ → x ′ in G U , and because

x ′ = x ⋅ f , there is an edge x → x ′ or x ′ → x in G U .
The former case is impossible by target-linearity, and the latter case would imply the existence of a path µ → x in G U , which contradicts the maximality of µ. So x ′ ∈ past(µ) is impossible altogether.

Proof of Theorem 5.22. We proceed by induction on the number of actions in U . If it is zero, then U is a position; by (C2), t is an iso, and by (C3) so is s, hence the cospan is a trace. For the induction step, we first decompose U into

Y s 2 → U ′ t 2 ← Z s 1 → M ′ t 1 ← X,
and then show that M ′ is an action and U ′ satisfies the conditions of the theorem. First, by acyclicity, pick a maximal core µ in G U , i.e., one with no path to any other core. Let

I 0 Y 0 M 0 X 0
be the seed with interface corresponding to µ, so we have the Yoneda morphism µ∶ M 0 → U . Let U ′ = (U µ), and X 1 = X -Agents(X 0 ). X 1 is a subpresheaf of X, since it contains all channels. The square

I 0 X 1 X 0 X
is a pushout, since it just adds the missing agents to X 1 . Define now Z, M ′ , s 1 , and t 1 by the pushouts

Y 0 Z M 0 M ′ U I 0 X 1 X 0 X t 1 s 1
and the induced arrows. We further obtain arrows to U by universal property of pushout. Let us show that the arrow

f ∶ M ′ → U is mono. First, it is obviously mono in dimensions > 1. It is also mono in dimension 1, because M ′ [n] = X[n] + Y 0 [n]
for all n and X → U is mono with image consisting only of initial agents, which are thus dijoint from the image of Y 0 . Finally, for dimension 0, i.e., at ⋆, the pushout defining M ′ is isomorphic to

I 0 (⋆) = X 0 (⋆) X 1 (⋆) = X(⋆) M 0 (⋆) = X 0 (⋆) + I M ′ (⋆) = X(⋆) + I inj l inj l
where I = M 0 (⋆) ∖ X 0 (⋆) is the set of channels created by the action. Consider any a, b ∈

M ′ (⋆) such that a ≠ b. Because X → U is mono, if a, b ∈ X(⋆) then f (a) ≠ f (b). By local 1-injectivity of U , if a, b ∈ I then f (a) ≠ f (b). Finally, if a ∈ X(⋆) and b ∈ I, then we have an edge f (b) → µ in G U , whereas f (a) is initial by (C2), so f (a) ≠ f (b)
. This shows that M ′ → U is mono, which also entails that Z → U is a mono, because s 1 is a pushout of the mono Y 0 → M 0 . By (C1) and Lemma 5.25, U = M ′ ∪ U ′ , i.e., the square

Z U ′ M ′ U
is a pushout, so U is indeed a composite as claimed, with Z ↪ M ′ ↩ X an action by construction. So, it remains to prove that Y ↪ U ′ ↩ Z satisfies the conditions. First, as a subpresheaf of U (whose inclusion preserves cores), U ′ is locally 1-injective and has a linear and acyclic causal graph, so satisfies (C1) and (C4). U ′ furthermore satisfies (C2) by construction of Z and source-linearity of G U , and (C3) because removing past(µ) cannot make any non-final agent final.

Let us conclude this section with a helpful lemma, whose proof relies on Theorem 5.22:

Lemma 5.26. There is at most one cell filling any diagram

Y ′ Y X ′ X k u ′ h u in D.
In order to prove this, let us introduce:

Definition 5.27. For any action x ∈ U , let core(x), the core associated to x, be the unique core µ ∈ U for which there exists f in C such that µ ⋅ f = x. If x is an agent or a channel, then by definition core(x) = x.

Proof of Lemma 5.26. By definition, we have cospans

Y ′ s ′ → u ′ t ′ ← X ′ and Y s → u t ← X.
Suppose we are given l, l ′ ∶ u ′ → u making (k, l, h) and (k, l ′ , h) into cells. By naturality, l and l ′ are determined by their images on channels, agents, and cores. We show by induction on the ordering induced by G u ′ that they have to agree on these. For the base case: they have to agree with h on initial agents and channels by definition of cells. For the induction step, we proceed by case analysis on the kind of element to consider. The image of any source of or channel created by a core µ is uniquely determined by naturality, which leaves the case of a core µ, of which we assume that there is an agent x such that µ → x in G u ′ and l(x) = l ′ (x). The edge µ → x yields a morphism, say t, in C such that µ ⋅ t = x. But then by naturality we have l(µ) ⋅ t = l(x) = l ′ (x) = l ′ (µ) ⋅ t. By linearity of G u we have core(l(µ)) = core(l ′ (µ)). Now let c µ denote the object of C over which µ lies, and let c ′ be the one over which core(l(µ)) lies. By inspection of C, there is exactly one morphism f ∶ c µ → c ′ , and so we have l(µ) = core(l(µ)) ⋅ f = core(l ′ (µ)) ⋅ f = l(µ), as desired.

A playground.

In this section, we finally prove: Theorem 5.28. D forms a playground.

Most axioms have been proved in previous sections, and we are left with both decomposition axioms, which are proved in Lemmas 5.29 and 5.30 below, relying on the correctness criterion of the previous section.

Lemma 5.29. (P7) Any double cell as in the center below, where B is a basic action and M is an action, decomposes in exactly one of the forms on the left and right:

A X C Y D Z α 1 α 2 A X C Y D Z h U B V M k α A X C Y D Z. α 1 α 2
Proof. For any element a over c ∈ C of any presheaf F ∈ Ĉ, let its neighbourhood consist of all elements in the image of a∶ c → F . Let b ∈ B and m ∈ M be the unique cores of B and M , respectively. Let V m be the neighbourhood of m in M • V .

If α(b) ∈ V m , let us show that the whole of U is mapped to V , and we are in the left-hand case. It is clear for channels. If there exists an element x of U of dimension ≥ 1 mapped to y in M -V , i.e., M -Y , then we obtain a path x → x ′ to an agent

x ′ of C, in G B•U . Via α, this yields a path M -Y → Y in G M •V between elements of dimension ≥ 1, a contradiction.
If now α(b) ∉ V m , we show similarly that the whole of B • U is mapped to V , because the contrary would imply the existence of a path M -Y → V -Y in G M •V , which also is a contradiction. Hence, we are in the right-hand case.

Lemma 5.30. (P6) Any double cell

A X Y B Z h U W 1 W 2 k α decomposes as A X C Y B Z h U 1 U U 2 f W 1 W 2 k α 1 α 2 α 3
with α 3 an isomorphism, in an essentially unique way.

Proof. Let α = (h, f, k). We first treat the case where W 2 is an action M , recalling Definition 5.27. We construct U 1 and U 2 , as depicted in Figure 5. First, let

U 1 = U × W W 1 ,
where W = W 2 • W 1 , and let A → U 1 denote the induced arrow. By construction, all of A → U 1 → U are monos and, by Lemma 3.20 and the pullback lemma,

A = U 1 × W 1 X.
Let us show that the projection f 1 ∶ U 1 → W 1 preserves initiality of channels and agents. We proceed by contrapositive: consider any channel or agent morphism between traces, it preserves initiality, so x cannot be initial in U , hence we find x → µ in G U . By source linearity of G W , core(f (µ)) = µ ′ , so the action f (µ) ∈ W has antecedents both in U and W 1 . By universal property of pullback, there exists an action y ∈ U 1 , respectively mapped to µ and f (µ), which by naturality and injectivity of U 1 → U entails that x → y in G U 1 . Therefore, x is not initial in G U 1 , as required.

x ∈ U 1 . If x ′ = f 1 (x) is not initial in W 1 , then we have an edge x ′ → µ ′ for some core µ ′ of W 1 . But, since f is a A X U 1 W 1 C Y U W U 2 M B Z, fm f f 1 f 2 h k
Let now C ↪ U 1 denote the subpresheaf of U 1 consisting of initial channels and agents (a subpresheaf because if x is an initial, n-ary agent, then x ⋅ s i is an initial channel for any i ∈ n, by Theorem 5.22 and Lemma 5.21). Since f 1 preserves initiality, C → U 1 → W 1 factors through Y → W 1 , uniquely since the latter is mono, say as f m (see Figure 5). By Theorem 5. 22,A

→ U 1 ← C is a trace and (h, f 1 , f m ) defines a morphism to X → W 1 ← Y . Let then U 2 ↪ U denote the subpresheaf of U consisting of elements below C in G U , i.e., x ∈ U 2 ⇔ ∃c ∈ C.c → ⋆ G U core(x)
. A first observation is that all initial channels and agents of U are in U 2 , so that B → U factors through U 2 . Indeed, consider any such initial x. By acyclicity of G U , each initial element is reachable from some final element, so x is reachable from some final y. But by source-linearity the corresponding path y → ⋆ x goes through C, so we find a path c → ⋆ x for some c ∈ C, as desired. Now, because U 2 → U and M → W are monos, showing that f maps all elements x of U 2 to M will imply that U 2 → U → W uniquely factors through M → W . Let us do this by case analysis:

• If x is not a channel, then f preserves paths from agents to x, so we find some path

f (c) → ⋆ G W core(f (x)) with c ∈ C hence f (c) ∈ Y , which implies that f (x) ∈ M (f (x) ∈ W 1 -M would contradict initiality of Y in W 1 ). • If x is some channel initial in U , then since f preserves initiality x is mapped to Z hence to M .
• If finally x is some non-initial channel, then x → µ for some core µ ∈ U . Now µ ∈ U 2 , as witnessed by the path c → ⋆ x → µ. But then x = µ ⋅ u for some morphism u of C, so since by the above f (µ) ∈ M , we have that f (x) = f (µ) ⋅ u is in M too, as desired. We thus get a diagram as in Figure 5, which commutes because M → W is mono. By Theorem 5.22, C → U 2 ← B is a trace, and U = U 2 • U 1 , which shows existence of the desired decomposition.

For any decomposition as in Figure 5, we have C = U 2 × M Y by Lemma 3.20, so by Corollary 4.20, we also have U 1 = U × W W 1 . Thus, U 1 is uniquely determined up to canonical isomorphism. But by Theorem 5.22, C → U 1 is so too, as the subobject of initial agents and channels. But then U 2 precisely consists of elements below C. Indeed, by finiteness of G U 2 and (C3) in Theorem 5.22, all of U 2 clearly lies below C. Conversely, for any x ∈ U 1 -U 2 , by finiteness of G U 1 and (C3) in Theorem 5.22, we have a path x → + c to some c ∈ C, so x cannot lie below C by (C4). Our decomposition is thus unique up to canonical isomorphism.

A sheaf model

In the previous sections, we have constructed a double category D and equipped it with playground structure. We now instantiate constructions from [START_REF] Hirschowitz | Full abstraction for fair testing in CCS (expanded version)[END_REF] on D, which lead to the definition of our sheaf model for π. We first recall various notions of strategy in Section 6.1: naive strategies, innocent strategies, and behaviours. Behaviours are further studied in Section 6.2, where we introduce a kind of calculus for them. Using this calculus, we then define our intepretation of π in Section 6.3. Finally, in Section 6.4, we state our semantic definition of fair testing equivalence and our main result. 6.1. Strategies and behaviours. We first recall notions of strategies. As announced in the introduction, we define a category T(X) combining prefix ordering and isomorphism of traces: T(X) has traces u∶ Y X as objects, and as morphisms u → u ′ all pairs (w, α)

with w∶ Y ′ Y and α an isomorphism u • w → u ′ in the hom-category D v (Y ′ , X), as in Y ′ Y X, w u u ′ ≅ α considered up to the smallest equivalence relation identifying (w, α) and (w ′ , α ○ (u • γ)), for any w ′ ∶ Y ′
Y and special γ∶ w ′ → w). Thus, u ′ is an extension of u by w. Definition 6.1. Let the category of (naive) strategies on X be T(X).

Strategies do not yield a satisfactory model for π: Example 6.2. Consider the position X with three agents x, y, z sharing a channel a, and the following traces on it: in u x,y , x sends a on a, and y receives it; in u x,z , x sends a on a, and z receives it; in i z , z inputs on a. One may define a strategy S mapping u x,y and i z to a singleton, and u x,z to ⊘. Because u x,y is accepted, x accepts to send a on a; and because i z is accepted, z accepts to input on a. The problem is that S rejecting u x,z roughly amounts to x refusing to synchronise with z, or conversely.

We want to rule out this kind of strategy from our model, by adapting the idea of innocence. We start by extending T(X) with objects representing traces on subpositions of X. For this, we consider the following category T X . It has as objects pairs (u, h) of a trace u∶ Z Y and a morphism h∶ Y → X in D h . A morphism (u, h) → (u ′ , h ′ ) consists of a trace w∶ T Z and a cell as below left with h ′ r = h. Morphisms are considered up to the smallest equivalence relation identifying (w, α) with (w ′ , α ○ (u • γ)), for any w ′ and γ as below right.

T Z ′ Z Y Y ′ w u u ′ r s α X h h ′ T ′ T Z ′ Z Y Y ′ w w ′ u u ′ r s α γ X h h ′ Example 6.3.
Recalling the right-hand trace of Figure 4 (page 22), say u∶ Y X, y's first action is an input on its unique channel b. This yields a trace

ι 1,1 ∶ [2] [1].
Here is an

examlpe morphism (ι 1,1 , y) → (u, id X ) in T X : [3] Y [2] [1] X. ι 2,2 ι 1,1 u y y ′′
X.

y

We think of it as an occurrence of the trace ι 1,1 in u. Thus, morphisms in T X account both for prefix inclusion and for 'spatial' inclusion, i.e., inclusion of a trace into some other trace on a larger position.

We now define views within T X : Definition 6.4. A view is a trace isomorphic to some (possibly empty) composite of basic actions (Definition 5.1). Let V X denote the full subcategory of T X spanning pairs (u, h) where u is a view.

Intuitively, basic actions follow exactly one agent through an action. An object of V X consists of a view, say v∶ [n ′ ]

[n], plus a morphism h∶ [n] → X in D h , which by Yoneda is just an agent of X. So an object of V X is just an agent of X and a view from it.

Definition 6.5. The inclusion j X ∶ V X ↪ T X induces a Grothendieck topology, for which a sieve ((u i , h i )

(w i ,α i )
→ (u, h)) i∈I of morphisms to some trace u is covering iff it contains all morphisms from views into u. Let the category S X ↪ T X of innocent strategies be the category of sheaves of finite sets for this topology. Let the category B X of behaviours over X be V X .

As announced in the introduction, letting ran j op X denote right Kan extension [START_REF] Mac | Categories for the Working Mathematician[END_REF] along the inclusion j op X ∶ V op X ↪ T op X , we have: Proposition 6.6. The embedding ran j op X induces an equivalence of categories B X ≃ S X .

Proof. See [START_REF] Hirschowitz | Full abstraction for fair testing in CCS (expanded version)[END_REF]Lemma 4.34].

We thus obtain the innocent strategy S B associated to a behaviour B ∈ B X by taking its right Kan extension as in

V op X T op X T(X) op set. B j op X k op X U(S B ) S B
Explicitly, using standard results, we obtain the end

S B (u, h) = (v,x)∈V X B(v, x) T X ((v,x),(u,h)) ,
which is a kind of generalised product. In the boolean setting (functors to 2), this end reduces to the conjunction ⋀ {(v,x)∈V X ∃α∶(v,x)→(u,h)} B(v, x), demanding precisely that all views of u are accepted by B. In the general case, the intuition is that a way of accepting u for S B is a compatible family of ways of accepting the views of u for B. The forgetful functor U to naive strategies is then given by restricting along the opposite of k X ∶ T(X) ↪ T X as above. Some local information may be forgotten by U, which is hence neither injective on objects, nor full, nor faithful. E.g., if two behaviours differ on one agent, but are both empty on the views of another, then both are mapped to the empty naive strategy. Example 6.7. Recalling X and S from Example 6.2, let us show that for any B ∈ B X , the associated strategy U(S B ) ∈ T(X) cannot be S. Indeed, if U(S B ) was S, then because S accepts u x,y and i z , B has to accept the following views: (1) i z , (2) o x , in which x sends a on a (without any matching input), (3) i y , in which y inputs on a, and (4) all identity views on x, y, and z. But then U(S B ) has to accept both u x,y and u x,z , because B accepts all views mapping into them. 6.2. Decomposing behaviours. In this section, we study behaviours a bit more in depth, which yields the calculus announced at the beginning of Section 6. The starting point is that the assignment X ↦ B X may be equipped with useful structure, describing how a behaviour B on some given position restricts to any subposition, and also what remains of it after a given action has been played. Otherwise said, morphisms of D act contravariantly on behaviours:

• horizontal morphisms h∶ X → X ′ induce functors B h ∶ B X ′ → B X , and • vertical morphisms u∶ Y X induce functors B u ∶ B X → B Y .
Furthermore, any cell as below left induces a natural isomorphism as below right:

Y Y ′ X X ′ k u h u ′ α B Y B Y ′ B X B X ′ , B k Bu B h B u ′ ≅ which notably says that B ⋅ u ′ ⋅ k ≅ B ⋅ h ⋅ u for any behaviour B ∈ B X ′ .
This is worked out in detail and in full generality in [START_REF] Hirschowitz | Full abstraction for fair testing in CCS (expanded version)[END_REF], and extended to a pseudo double functor D op → QCat, where QCat denotes Ehresmann's double category of quintets over Cat. But let us explain how both actions look like in the present, concrete case.

The first, horizontal action is really easy: any horizontal morphism k∶ X ′ → X acts on a given behaviour B ∈ B X by returning the behaviour B ⋅ k such that for all

(v, h) ∈ V X ′ , (B ⋅ k)(v, h) = B(v, k ○ h). Proposition 6.8. The functor B X → ∏ n,x∶[n]→X B [n] given at (n, x) by horizontal action of x, i.e., B ↦ B ⋅ x, is an isomorphism. Proof. We have V X ≅ ∑ n,x∶[n]→X V [n] . Notation 6.9. If (B x ) x∶[n]
→X is a family of behaviours indexed by the agents of X, we accordingly denote its unique antecedent by

[B x ] x∶[n]→X .
Vertical action is a bit harder. Let us start by recalling the following result from [START_REF] Hirschowitz | Full abstraction for fair testing in CCS (expanded version)[END_REF], which generalises Lemma 5.5: with v y,P a view.

Proof. By induction on P using Lemma 5.5. See [START_REF] Hirschowitz | Full abstraction for fair testing in CCS (expanded version)[END_REF] for the precise meaning of essential uniqueness in this case. So we may consider residuals of behaviours along arbitrary traces. Conversely, any behaviour is determined by its initial states and residuals. Let us first consider the following special kind of behaviour:

Definition 6.12. A behaviour B on [n] is definite iff B(id • , id [n] ) ≅ 1.
A behaviour B on an arbitrary position X is definite iff for all agents x of X, B ⋅ x is definite. Let D X denote the full subcategory of B X spanning definite behaviours. This means that B has exactly one initial state. This extends to arbitrary behaviours on individuals using the fact that any behaviour on an individual is a coproduct of definite behaviours. Notation 6.15. For any behaviour B = ∑ k∈γ D k on any [n], let B = γ and, for any k ∈ γ, let the restriction B k of B to k be D k . Remark 6.16. In other words, k ∈ γ is just an element of B(id

• [n] , id [n] ) and B σ is deter- mined by B σ (v, id [n] ) = {σ ′ ∈ B(v, id [n] ) σ ′ ⋅ ! v = σ}, where ! v denotes the unique morphism (id • [n] , id [n] ) → (v, id [n] ) in V [n]
. We obtain: Proposition 6.17. For any behaviour

B ∈ B [n] , B ≅ k∈ B ⟨(B k ) ⋅ b⟩ b .
Putting this together with spatial decomposition, we obtain:

Corollary 6.18. For any behaviour B ∈ B X , B ≅ [ k∈ B⋅x ⟨((B ⋅ x) k ) ⋅ b⟩ b∶[n b ] [nx] ] x∶[nx]→X .
The fact that both actions of D yield a pseudo double functor D op → QCat essentially boils down to:

Lemma 6.19. For any B ∈ B X and cell Y ′ Y X ′ X, k u ′ h u α we have D ⋅ h ⋅ u ′ ≅ D ⋅ u ⋅ k.
The result is stated (and proved) in full generality as [39, Proposition 4.31]. 6.3. Interpretation of π. We now define our interpretation of π-calculus configurations. We start with processes and then cover configurations. Because the notation for behaviours introduced in the previous section only covers behaviours on representable positions, while π-calculus syntax is name-based, we bridge the gap by keeping track, along the recursive definition, of a bijection between the set γ of free channels of the considered process and its cardinal γ . So we define a family of maps in

γ∈P f (N) D Piγ ×Bij(γ, γ ) [ γ ]
,

where Bij(A, B) denotes the set of all bijections A -∼ B. For any such γ, P , and h in the domain, we denote the result by ⟦P ⟧ h , or ⟦P ⟧ γ,h when needed. Letting n = γ , it is coinductively defined by

⟦∑ i P i ⟧ h = ⊞ i ⟦P i ⟧ h ⟦P Q⟧ h = ⟨ π l n ↦ ⟦P ⟧ h π r n ↦ ⟦Q⟧ h ⟩ ⟦νb.P ⟧ h = ⟨ ν n ↦ ⟦P ⟧ h ′ ⟩ ⟦♡.P ⟧ h = ⟨ ♡ n ↦ ⟦P ⟧ h ⟩ ⟦τ.P ⟧ h = ⟨ τ n ↦ ⟦P ⟧ h ⟩ ⟦a(b).P ⟧ h = ⟨ ι n,h(a) ↦ ⟦P ⟧ h ′ ⟩ ⟦ā⟨b⟩.P ⟧ h = ⟨ o n,h(a),h(b) ↦ ⟦P ⟧ h ⟩
We now describe closed-world traces, which are then used as a criterion for success of tests. Closed-world actions were defined (Definition 5.1) as those not involving any interaction with the environment, i.e., formally, pushouts of a seed of any shape among ν n ,τ n ,♡ n ,π n , and τ n,a,m,c,d . A trace is closed-world when it is a composite of closed-world actions. Let W(X) i X T(X) denote the full subcategory of T(X) consisting of closed-world traces, and let the category of closed-world strategies be W(X).

Notation 6.23. Recalling the discussion below Proposition 6.6, we denote by B ↦ B the composite functor

V X ran j op X → T X ∆ k op X → T(X) ∆ i op X → W(X),
where ∆ f denotes restriction along f .

A closed-world trace is successful when it contains a ♡ action, and unsuccessful otherwise. A state σ ∈ S(u) of any S ∈ W(Z) over a closed-world trace u∶ Z ′ Z is successful iff u is. Define ⊥ ⊥ Z as the set of closed-world strategies S ∈ W(Z) such that any unsuccessful closed-world state admits a successful extension, i.e. S ∈ ⊥ ⊥ Z iff for all unsuccessful u ∈ W(Z) and σ ∈ S(u), there exists a successful u ′ ∈ W(Z), a morphism f ∶ u → u ′ , and a state σ ′ ∈ S(u ′ ) such that σ ′ ⋅ f = σ. Finally, in order to compare behaviours for semantic fair testing equivalence, we specify what a test is for a given behaviour B ∈ B X . A test consists of a position Y and a behaviour T ∈ B Y . Recalling Definition 3.8, we say that the pair (X, B), with B ∈ B X , should pass the test (Y, T ) iff I X = I Y and [B, T ] ∈ ⊥ ⊥ Z , where Z is the pushout X + I X Y (X and Y thus form two teams on Z). At last, we define semantic fair testing equivalence, for any B ∈ B X and B ′ ∈ B X ′ : Definition 6.24. Let (X, B) ∼ f (X ′ , B ′ ) iff they should pass the same tests.

We may at last state: Theorem 6.25. The translation ⟦-⟧∶ ob(Conf) → ∑ X B X is intensionally fully abstract for ∼ f , i.e.,

• For all configurations C 1 and

C 2 , C 1 ∼ Pi f C 2 iff ⟦C 1 ⟧ ∼ f ⟦C 2 ⟧;
• Furthermore, for all positions X and behaviours B ∈ B X , there exists C ∈ Pi X(⋆)

such that ⟦C⟧ ∼ f B.
The proof is the subject of the next section.

Intensional full abstraction

In the previous section, exploiting the playground structure of D established in Sections 4 and 5, we have defined and studied the notion of behaviour, into which we have translated π-calculus processes and configurations. We have then defined our semantic analogue of fair testing equivalence and stated our main result. We now work towards proving it. In Section 7.1, we define a graph with testing S whose vertices are pairs (X, B) with B a definite behaviour on the position X (Definition 6.12), such that fair testing equivalence in S coincides with fair testing equivalence in the model. In order to prove that this is the case, we introduce an intermediate graph with testing C which is in fact quite intricate. We are then in a position where our main result is reduced to intensional full abstraction of a translation between two graphs with testing, Conf and S, for which we may hope to apply the results of Section 2.3. In fact, in Section 7.2, we further reduce to a translation to a more syntactic graph with testing, M. In Section 7.3, we prove intensional full abstraction of the translation to M, from which we deduce Theorem 6.25. Finally, we generalise to a large class of testing equivalences in Section 7.4.

7.1.

A first graph with testing for behaviours. Definition 7.1. Let S denote the graph with vertices in ∑ X D X , where we recall (Definition 6.12) that D X denotes the category of definite behaviours on X, and with non-identity edges (X, D) ← (Y, D ′ ) all closed-world actions M ∶ Y X such that for all agents y in Y , there exists σ y ∈ D ⋅ M ⋅ y such that

D ′ ⋅ y ≅ (D ⋅ M ⋅ y) σy .
Moreover, let p S ∶ S → Σ denote the map sending (X, D) M ← (X ′ , D ′ ) to the ♡ edge in Σ if M is a tick action and to τ otherwise.

Let us now equip S with testing structure. Definition 7.2. We define the relation S by (Z, D) ∈ ((X 1 , D 1 ) S (X 2 , D 2 )) iff X 1 (⋆) = X 2 (⋆) and there is a pushout square Proof. We exhibit a weak bisimulation relating any two such pushouts (Z, D) and (Z ′ , D ′ ).

I X 1 X 2 X 1 Z inj l injr such that D 1 ≅ D ⋅ inj
The relation containing two such pairs as soon as there exists a horizontal isomorphism h∶ Z → Z ′ such that D ≅ D ′ ⋅ h does the job.

The crucial result for proving that fair testing equivalence in S coincides with semantic fair testing equivalence is:

Lemma 7.4. For any definite behaviour D ∈ D X , we have D ∈ ⊥ ⊥ X iff (X, D) ∈ S .
Our strategy for proving this is to introduce and study an intermediate graph with testing C, which is closer to semantic fair testing in that its transitions may comprise several actions. However, defining C just as S with arbitrary traces instead of actions would be wrong: ). Instead of relying on ∏ y∈Agents(Y ) D ⋅ P ⋅ y as in Definition 7.1, we would like to rely on D(P ). This may be done by constructing a map Furthermore, we also have

ψ D P ∶ D(P ) → y∶[ny]→Y D ⋅ P ⋅ y , (7.1
D(P ) ≅ (v,x)∈V X D(v, x) T X ((v,x),(P,id X )) ,
which is a subset of ∏ (v,x)∈V X D(v, x) T X ((v,x),(P,id X )) . We may thus define:

ψ P (σ)(y) = σ(v y,P , y P )(id • [ny] , α y,P ).
Here, σ(v y,P , y P ) is in D(v y,P , y P ) T X ((v y,P ,y P ),(P,id X )) . So by applying it to α y,P viewed as a morphism in (v y,P , y P ) → (P, id X ) in T X , we obtain an element of D(v y,P , y P ) = D ⋅P ⋅y , as desired.

We may now define the intermediate graph with testing C. We first extend the notion of restriction: Notation 7.6. We extend Notation 6.15: if B ∈ B X and σ ∈ ∏ n,x∶[n]→X B ⋅ x , let B σ be defined up to isomorphism by

B σ ⋅ x = (B ⋅ x) σ(x) .
Definition 7.7. Let C denote the graph with ob(C) = ob(S), and where C((X ′ , D ′ ), (X, D)) is the set of closed-world traces W ∶ X ′ X such that there exists a state σ ∈ D(W ) satisfying

(D ⋅ W ) ψ W (σ) ≅ D ′ .
Thus, C is a generalisation of S from closed-world actions to closed-world traces. Let us turn it into a graph with testing. As announced, C is an example of a non-free graph with testing. The rest of this section is devoted proving Lemma 7.4, and reducing Theorem 6.25 to a statement about S. Lemma 7.4 follows from the fact that both poles are equivalent to C , as we now set out to prove. We start with a lemma saying that C has essentially the same transitions over two (specially) isomorphic traces. Lemma 7.11. For any (X, D), (X ′ , D ′ ) ∈ C, if there exists any special isomorphism

W 1 ≅ W 2 in D W v (X ′ , X), we have (p C ) -1 (X ′ ,D ′ ),(X,D) (W 1 ) ≅ (p C ) -1 (X ′ ,D ′ ),(X,D) (W 2
). Proof. The given special isomorphism induces by pseudo double functoriality of B an isomorphism ϕ∶ D ⋅ W 1 -∼ D ⋅ W 2 , hence an isomorphism

ϕ id X ′ ∶ D(W 1 ) -∼ D(W 2 ).
This isomorphism is such that for any σ,

(D ⋅ W 1 ) ψ W 1 (σ) ≅ (D ⋅ W 2 ) ψ W 2 (ϕ id X ′ (σ)) .
Thus,

(D ⋅ W 1 ) ψ W 1 (σ) ≅ D ′ iff (D ⋅ W 2 ) ψ W 2 (ϕ id X ′ (σ)) ≅ D ′ .
In order to relate C to S, let us now show that transitions in C behave well w.r.t. composition of traces. First, transitions compose, and second, transitions over any composite (closed-world) trace W 1 • W 2 always decompose into a transition over W 1 followed by one over W 2 . Lemma 7.12. For all edges (X, D)

W ← (X ′ , D ′ ) W ′ ← (X ′′ , D ′′ ) in C, there is an edge (X, D) W •W ′ ← (X ′′ , D ′′ ). Proof. Consider σ ∈ D(W ) such that (D ⋅ W ) ψ W (σ) ≅ D ′ and σ ′ ∈ D ′ (W ′ ) such that (D ′ ⋅ W ′ ) ψ W ′ (σ ′ ) ≅ D ′′ . We want to construct an edge W • W ′ ∶ (X ′′ , D ′′ ) → (X, D), i.e., find σ ′′ ∈ D(W • W ′ ) such that (D ⋅ (W • W ′ )) ψ W •W ′ (σ ′′ ) ≅ D ′′ . Now, the isomorphism ϕ∶ (D ⋅ W ) ψ W (σ) -∼ D ′ yields a state σ 1 = ϕ -1 W ′ (σ ′ ) ∈ (D ⋅ W ) ψ W (σ) (W ′ ) such that ((D ⋅ W ) ψ W (σ) ⋅ W ′ ) ψ W ′ (σ 1 ) ≅ (D ′ ⋅ W ′ ) ψ W ′ (σ ′ ) . (7.2)
Now we have

(D ⋅ W ) ψ W (σ) (W ′ ) ≅ {σ ′′ ∈ D(W • W ′ ) σ ′′ W = σ}, where σ ′′ W denotes restriction of σ ′′ along the prefix inclusion W ↪ W •W ′ . So the left-hand side in (7.2) is just (D ⋅ (W • W ′ )) ψ W •W ′ (σ 1 )
, which yields the desired transition.

Lemma 7.13. The projection p C ∶ C → D W v satisfies the following weak Conduché condition: for all X ′′ W 2 X ′ W 1 X, if there is an edge (X ′′ , D ′′ )

W 1 •W 2 → (X, D) in C, then there exists D ′ ∈ D X ′ and edges (X ′′ , D ′′ ) W 2 → (X ′ , D ′ ) W 1 → (X, D).
Proof. Consider any (X, D) ∈ C and σ ∈ D(W 1 • W 2 ) witnessing the given edge. Consider also the morphism u∶ W 1 → (W 1 • W 2 ) given by (W 2 , id ), and let

σ 1 = σ ⋅ u ∈ D(W 1 ). Let D 1 = (D ⋅ W 1 ) ψ W 1 (σ 1 ) . We have σ ∈ {σ ′ ∈ D(W 1 • W 2 ) σ ′ ⋅ u = σ 1 }, hence σ ∈ D 1 (W 2 ). Furthermore, (D 1 ⋅ W 2 ) ψ W 2 (σ) ≅ (D ⋅ (W 1 • W 2 )) ψ W 1 •W 2 (σ) ≅ D ′′ ,
so we have two edges (X, D)

(W 1 ,σ 1 ) ← (X ′ , D 1 ) (W 2 ,σ) ← (X ′′ , D ′′ )
as desired.

The previous result generalises by induction to n-ary composites:

Notation 7.14. By default, composition in D W v associates to the right, i.e., W

• W ′ • W ′′ denotes W • (W ′ • W ′′ ).
Corollary 7.15. For any path p, say Our next goal is to relate transitions in C to sequences of transitions in S. First of all, C and S coincide on actions:

X = X 0 M 1 X 1 M 2 . . . X n = X ′ , (7.3
Lemma 7.16. If W ∶ X ′
X is a closed-world action (i.e., has length 1), then for all D and D ′ both fibres of C((X ′ , D ′ ), (X, D)) and S((X ′ , D ′ ), (X, D)) over W are equal.

Proof. By [START_REF] Hirschowitz | Full abstraction for fair testing in CCS (expanded version)[END_REF]Proposition 5.23]. Now, let us show that for any sequence of closed-world actions, sequences of transitions in S correspond to transitions over the composite in C. Corollary 7.17. For all closed-world paths as in (7.3), and (X, D), (X ′ , D ′ ) ∈ S, we have

((p S ) ⋆ (X ′ ,D ′ ),(X,D) ) -1 (p) ≠ ⊘ iff (p C (X ′ ,D ′ ),(X,D) ) -1 (P ) ≠ ⊘, for any special isomorphism P ≅ (M 1 • (. . . • M n )).
Proof. Consider any special isomorphism α∶ P -∼ (M 1 • (. . . • M n )). We have As a corollary, we get that the identity relation on objects is a strong bisimulation between fc(S) and C: Corollary 7.18. For all w ∈ Σ ⋆ (⋆, ⋆) and (X, D), (X ′ , D ′ ) ∈ S, we have (X, D)

((p S ) ⋆ (X ′ ,D ′ ),(X,D) ) -1 (p) ≠ ⊘ iff ((p C ) ⋆ (X ′ ,D ′ ),(X,D) ) -1 (p) ≠ ⊘ (by Lemma 7.16) iff (p C (X ′ ,D ′ ),(X,D) ) -1 (M 1 • (. . . • M n )) ≠ ⊘ (
w ⇐ (X ′ , D ′ ) in S iff (X, D) w ← (X ′ , D ′ ) in C.
The last statement is slightly subtle, in that (X, D) w ← (X ′ , D ′ ) denotes a single edge in C, lying over the composite w in fc(Σ).

Proof. If (X, D) w ⇐ (X ′ , D ′ ) in S, then there exists p ∈ W ⋆ such that fc(p W )(p) = w and there is a path e∶ (X ′ , D ′ ) → (X, D) over p in S. Let W ∶ X ′
X denote the composition of p. By Corollary 7.17, we get an edge (X ′ , D ′ ) → (X, D) over W in C. So since p W (W ) = w, this gives us the expected transition.

Conversely, if

(X, D) w ← (X ′ , D ′ ) in C, then let W ∶ X ′ X denote the corresponding edge in D W v .
In particular, we have p W (W ) = w. Decomposing W as some path p in W, we obtain by Corollary 7.17 a transition sequence (X, D)

(p W ) ⋆ (p) ⇐ (X ′ , D ′ ) in S. But (p W ) ⋆ (p) = p W (W ) = w, as desired.
As promised, we readily obtain: By hypothesis, σ admits an extension σ

′ ∈ D(W •W ′ ) for some successful W ′ ∶ X ′′ X ′ . Letting D ′′ = (D ⋅ (W • W ′ )) ψ W •W ′ (σ ′ ) , we have D ′′ ≅ (((D ⋅ W ) ψ W (σ) ) ⋅ W ′ ) ψ W ′ (σ ′ ) ≅ (D ′ ⋅ W ′ ) ψ W ′ (h W ′ (σ ′ )) ,
and hence (X ′ , D ′ ) ♡ n ← (X ′′ , D ′′ ) for some n > 0. This shows that (X, D) ∈ C . Conversely, assume (X, D) ∈ C and consider any unsuccessful, closed-world trace W ∶ X ′ X and state σ ∈ D(W ).

Letting D ′ = (D ⋅ W ) ψ W (σ) , we have (X, D) ← (X ′ , D ′ ).
By hypothesis, we find some transition

(X ′ , D ′ ) ♡ ← (X ′′ , D ′′ ), witnessed by some successful W ′ ∶ X ′′ X ′ . Hence, D ′′ ≅ (D ′ ⋅ W ′ ) ψ W ′ (σ ′ ) for a certain σ ′ ∈ D ′ (W ′ ). By definition of D ′ , σ ′ is a state in D(W • W ′ ) such that σ ′ ⋅ u = σ, where u∶ W → (W • W ′ ) is (W ′ , id
). This gives the desired successful extension of σ, which shows that D ∈ ⊥ ⊥ X .

Combining the last two results, we may now prove that the semantic pole coincides with that of S: Proof of Lemma 7.4. We have D ∈ ⊥ ⊥ X iff (X, D) ∈ C iff (X, D) ∈ S by Corollary 7.19 and Lemma 7.20.

As expected, this entails preservation and reflection of semantic fair testing equivalence:

Corollary 7.21. For all D ∈ D X and D ′ ∈ D X ′ , we have (X, D) ∼ f (X ′ , D ′ ) iff (X, D) ∼ S f (X ′ , D ′ )
Proof. Let us first show that semantic fair testing equivalence may as well be defined only with definite tests. Indeed, if I X ≠ I X ′ then the result holds trivially. So assuming I X = I X ′ , consider any test B ∈ B Y with I X = I Y , and, w.l.o.g.,

[D, B] ∈ ⊥ ⊥ Z and [D ′ , B] ∉ ⊥ ⊥ Z ′ with Z = X + I X Y and Z ′ = X ′ + I X ′ Y . Then, letting B = ∑ i∈γ D i with each D i definite, there exists i such that [D, D i ] ∈ ⊥ ⊥ Z and [D ′ , D i ] ∉ ⊥ ⊥ Z ′ , hence D i also distinguishes D from D ′ .
Returning to our main goal, for any definite test

T ∈ D Y with I Y = I X , by Lemma 7.4, [D, T ] ∈ ⊥ ⊥ Z iff (Z, [D, T ]) = ((X, D) (Y, T )) ∈ S ,
which easily entails the result.

From this we may reduce our main theorem to a result on S: Corollary 7.22. If the translation ⟦-⟧∶ ob(Conf) → ∑ X D X is intensionally fully abstract for ∼ S f , then Theorem 6.25 holds, i.e., ⟦-⟧ is also intensionally fully abstract for ∼ f . Proof. For all configurations C 1 and C 2 , by Corollary 7.21,

⟦C 1 ⟧ ∼ f ⟦C 2 ⟧ iff ⟦C 1 ⟧ ∼ S f ⟦C 2 ⟧, which holds iff C 1 ∼ Conf f C 2 by hypothesis.
It remains to prove that surjectivity up to ∼ f reduces to surjectivity up to ∼ S f . For this, let us first show that any behaviour is ∼ f -equivalent to some definite one. Indeed, consider any B ∈ B X . Letting B ⋅ x = ∑ i∈nx D x i for all agents x in X, B is fair testing equivalent to the definite behaviour D such that

D ⋅ x = ⟨τ nx ↦ i∈nx D x i ⟩,
except if B ⋅ x = ⊘ for some x. But in the latter case, B is fair testing equivalent to the definite behaviour on one nullary player with the same interface which merely ticks. Thus, we may restrict attention to definite behaviours. So consider any definite D ∈ D X . By hypothesis, there exists C such that ⟦C⟧ ∼ S f (X, D), hence ⟦C⟧ ∼ f (X, D) by Corollary 7.21, which concludes the proof. 7.2. A further graph with testing for behaviours. In the previous section, we have characterised semantic fair testing equivalence using the graph with testing S, and reduced intensional full abstraction of ⟦-⟧ w.r.t. ∼ f to intensional full abstraction w.r.t. ∼ S f . We now define a further graph with testing, M, which will help us bridge the gap between S and π-calculus configurations. Indeed, we define a surjective morphism m∶ S → M over Σ, and we then prove that m is intensionally fully abstract (Proposition 7.30), from which we deduce that our main result follows from intensional full abstractness of the composite translation T = m ○ ⟦-⟧ (Lemma 7.32).

Recall from Definition 2.3 that -⊙ denotes the finite multiset monad on sets.

Definition 7.23. Let the set M 0 of mixed behaviours be

γ∈P f (N) ( n∈N D [n] × γ n ) ⊙ .
The graph M over Σ is inductively defined by the rules in Figure 6, where S[γ 1 ⊆ γ 2 ] denotes pointwise composition of the substitution component with the inclusion h∶ γ 1 ⊆ γ 2 , i.e., each Let us now reduce Theorem 6.25 to a statement about M. In order to do this, we will use Lemma 2.22 and hence need to exhibit a fair relation ob(S) M 0 . We use the graph of the following map: Definition 7.27. Let m∶ ob(S) → M 0 map any (X, D) to the mixed behaviour

D[σ] is replaced by D[h ○ σ]. Let p M ∶ M → Σ denote the projection. i ∈ D ⋅ π l n j ∈ D ⋅ π r n ⟨γ∥D[σ]⟩ id ← ⟨γ∥(D ⋅ π l n ) i [σ], (D ⋅ π r n ) j [σ]⟩ i ∈ D ⋅ τ n ⟨γ∥D[σ]⟩ id ← ⟨γ∥(D ⋅ τ n ) i [σ]⟩ i ∈ D ⋅ ♡ n ⟨γ∥D[σ]⟩ ♡ ← ⟨γ∥(D ⋅ ♡ n ) i [σ]⟩ i ∈ D ⋅ ν n a ∉ γ ⟨γ∥D[σ]⟩ id ← ⟨γ, a∥(D ⋅ ν n ) i [n + 1 σ+⌜a⌝ → γ, a]⟩ i ∈ D 1 ⋅ ι n 1 ,a 1 j ∈ D 2 ⋅ o n 2 ,a 2 ,b 2 σ 1 (a 1 ) = σ 2 (a 2 ) ⟨γ∥D 1 [σ 1 ], D 2 [σ 2 ]⟩ id ← ⟨γ∥(D 1 ⋅ ι n 1 ,a 1 ) i [n 1 + 1 [σ 1 ,⌜σ 2 (b 2 )⌝] → γ], (D 2 ⋅ o n 2 ,a 2 ,b 2 ) j [σ 2 ]⟩ ⟨γ 1 ∥S 1 ⟩ α ← ⟨γ 2 ∥S 2 ⟩ ⟨γ 1 ∥S ∪ S 1 ⟩ α ← ⟨γ 2 ∥S[γ 1 ⊆ γ 2 ] ∪ S 2 ⟩ ⟨γ∥S⟩ id ← ⟨γ∥S⟩
⟨X(⋆)∥[(D ⋅ x)[σ x ] (n, x) ∈ Agents(X)]⟩,
where σ x is the map n

[⌜x⋅s i ⌝] i∈n → X(⋆).
We now need to show that m yields a fair relation. Most points are direct, like totality or the fact that (X, D) ¨(X ′ , D ′ ) iff m(X, D) ¨m(X ′ , D ′ ). Furthermore, we have:

← M ′ , there exists (X, D) α ← (X ′ , D ′ ) such that m(X ′ , D ′ ) = M ′ , as below right. (X, D) m(X, D) (Y, D ′ ) I (Z, D ′′ ) m m(Z, D ′′ ) α α m (X, D) m m(X, D) (Y, D ′ ) m M ′ α α
The right-hand diagram is a tedious yet straightforward case analysis. The left-hand one is also a tedious case analysis, whose main point is that for all transitions (X, D) α ← (Y, D ′ ), some renaming of elements of X may take place, which cannot happen in any transition from m(X, D). So in each case we need to find the Z and corresponding D ′′ which avoids such renaming. In fact, this goes by indentifying the right transition from m(X, D) and showing that the obtained M ′ is of the form m(Z, D ′′ ) for (Y, D ′ ) I (Z, D ′′ ). Let us do one case. If (X, D) ♡ ← (Y, D ′ ), then we have an iso h∶ X -∼ Y , and there is some agent (n 0 , x 0 ) in X and i such that D ′ ⋅ h(x 0 ) = (D ⋅ x 0 ⋅ ♡ n 0 ) i and furthermore for all (n, x) ≠ (n 0 , x 0 ) in Agents(X), we have D ′ ⋅ h(x) = D ⋅ x. So, letting y = h(x) for all such x, we indeed have We are now ready to show: Proposition 7.30. The map m∶ ob(S) → ob(M) is intensionally fully abstract for fair testing equivalence.

M = ⟨γ∥(D ⋅x 0 )[σ x 0 ]∶∶[(D ⋅x)[σ x ] x ≠ x 0 ]⟩ ♡ ⟨γ∥(D ′ ⋅y 0 )[σ x 0 ]∶∶[(D ⋅x)[σ x ] x ≠ x 0 ]⟩ = M ′ with M = m(X,
Proof. As announced, for preservation and reflection of fair testing equivalence we apply Lemma 2.22: we have established all necessary hypotheses, except the last one, which follows by choosing a pushout with the same set of channels as its summands.

For surjectivity up to ∼ M f , consider any ⟨γ∥S⟩ ∈ M 0 . Because a is a section of m, we have m(a(⟨γ∥S⟩)) = ⟨γ∥S⟩, hence m(a(⟨γ∥S⟩)) ∼ M f ⟨γ∥S⟩, thus providing the desired antecedent.

Let us now reduce Theorem 6.25 to its analogue about M. Concretely, we have

T⟨γ∥P 1 , . . . , P n ⟩ = ⟨γ∥⟦P 1 ⟧ hγ [h -1 γ ], . . . , ⟦P n ⟧ hγ [h -1 γ ]⟩. Lemma 7.32. The translation ⟦-⟧ from Definition 6.22 is intensionally fully abstract for ∼ S f if T is for ∼ M f .
Proof. Assuming T is intensionally fully abstract, then for all configurations C and C ′ , we have that

C ∼ f C ′ iff T(C) ∼ M f T(C ′ ).
But by Proposition 7.30, we have

T(C) = m⟦C⟧ ∼ M f m⟦C ′ ⟧ = T(C ′ ) iff ⟦C⟧ ∼ S f ⟦C ′ ⟧, hence C ∼ f C ′ iff ⟦C⟧ ∼ f S⟦C ′ ⟧.
Finally, for any (X, D) ∈ S, by intensional full abstractness of T, we find a configuration C such that T(C) ∼ M f m(X, D), hence by Proposition 7.30 again ⟦C⟧ ∼ f (X, D).

7.3. Intensional full abstraction. We at last prove our main result, by proving intensional full abstractness of T. Our strategy is to define a relation ⋈∶ Conf M over Σ which

• relates any configuration to its image under T, and • is surjective, i.e., relates any mixed behaviour to some configuration.

We will then show that this relation is a weak bisimulation over Σ, which will entail the result.

Let us start with the second point, and define a map Z ∈ ob(M) → ob(Conf), which associates a configuration to each mixed behaviour. We first coinductively define ζ for definite behaviours on representable positions by:

ζ(n ⊢ D D) = ⎛ ⎜ ⎜ ⎜ ⎜ ⎜ ⎜ ⎜ ⎜ ⎝ ∑ i∈ D⋅π l n ,j∈ D⋅π r n τ.(ζ(n ⊢ D (D ⋅ π l n ) i ) ζ(n ⊢ D (D ⋅ π r n ) j )) + ∑ i∈ D⋅τn τ.ζ(n ⊢ D (D ⋅ τ n ) i ) + ∑ i∈ D⋅♡n ♡.ζ(n ⊢ D (D ⋅ ♡ n ) i ) + ∑ i∈ D⋅νn ν(n + 1).ζ(n + 1 ⊢ D (D ⋅ ν n ) i ) + ∑ a∈n,i∈ D⋅ιn,a a(n + 1).ζ(n + 1 ⊢ D (D ⋅ ι n,a ) i ) + ∑ a,b∈n,i∈ D⋅o n,a,b ā⟨b⟩.ζ(n ⊢ D (D ⋅ o n,a,b ) i ) ⎞ ⎟ ⎟ ⎟ ⎟ ⎟ ⎟ ⎟ ⎟ ⎠ , where n ⊢ D D means D ∈ D [n] .
Except perhaps for the first term of the sum, this should be rather natural: each definite behaviour on a representable position corresponds to a guarded sum, with one term for each state over each basic action -the translation is direct. The twist in the first term is due to the fact that forking is not a guard in π, so P Q cannot appear in any guarded sum. But τ.(P Q) can, and it is clearly weakly bisimilar to P Q, so this is precisely what ζ does.

Let us now extend ζ to arbitrary configurations: Definition 7.33. Let Z∶ ob(M) → ob(Conf) be defined by

Z⟨γ∥D 1 [σ 1 ], . . . , D n [σ n ]⟩ = ⟨γ∥ζ(D 1 )[σ 1 ], . . . , ζ(D n )[σ n ]⟩.
Remark 7.34. Let us emphasise that brackets on the right denote proper substitutions, while on the left D i [σ i ] is just syntactic sugar for (n i , D i , σ i ) by Notation 7.24.

In order for Z to return an antecedent up to ∼ M f , we immediately observe that for any D and i ∈ D ⋅ π l n and j ∈ D ⋅ π r n , • on the one hand D has a silent transition to ∂ i,j D, the behaviour on (In the last rule, ǫ γ is understood in Conf on the left, and in M on the right.) Proof. First, we observe that ⋈ may equivalently be defined by first letting ⋈ 0 be generated by all rules except the last two, and then adding the rule

[n] [n] such that (∂ i,j D) ⋅ x 1 = (D ⋅ π l n ) i and (∂ i,j D) ⋅ x 2 = (D ⋅ π r n ) j (
γ ′ ⊢ P h∶ γ ′ -∼ n σ∶ n → γ P [σ ○ h] ⋈ ⟦P ⟧ h [σ] n ⊢ D D σ∶ n → γ ζ(D)[σ] ⋈ D[σ] n ⊢ D D 1 , D 2 σ∶ n → γ (ζ(D 1 ) ζ(D 2 ))[σ] ⋈ D 1 [σ], D 2 [σ] C ⋈ M D ⋈ N C@D ⋈ M @N ǫ γ ⋈ ǫ γ ⋅
C 1 ⋈ 0 M 1 . . . C n ⋈ 0 M n C 1 @ . . . @C n ⋈ M 1 @ . . . @M n (n ∈ N)⋅
The advantage of this presentation is that proofs of C ⋈ M all have depth at most 1.

The rest is then a tedious case analysis, which we defer to Appendix A. In summary, we easily observe that the 'forwards' clause of weak bisimulation is satisfied, the only subtlety being that heating (ζ(D 1 ) ζ(D 2 ))[σ] should be matched by the identity edge on the corresponding behaviour. Furthermore, the 'backwards' clause is also easily satisfied, the only subtlety being that if the considered behaviour performs a transition involving one or several

, C 2 , M 1 , M 2 , if C 1 ⋈ M 1 and C 2 ⋈ M 2 , then C 1 ∼ f C 2 iff M 1 ∼ f M 2 .
Proof. The relation ⋈ is weakly fair, the only difficult points being proved by Lemmas 7.36 and 7.37 above. We thus conclude by Corollary 2.25.

Theorem 7.39. The map T∶ ob(Conf) → ob(M) is intensionally fully abstract.

Proof. Lemma 7.38 directly entails preservation and reflection of fair testing equivalence. Regarding surjectivity up to ∼ M f , for any M ∈ M 0 , we have M ∼ M f T(Z((M ))). Indeed, for any M ′ , we have M @M ′ ∈ iff Z(M )@Z(M ′ ) ∈ (because Z(M )@Z(M ′ ) ⋈ M @M ′ and by Lemma 7.37) iff T(Z(M ))@M ′ ∈ (because Z(M )@Z(M ′ ) ⋈ T(Z(M ))@M ′ and by Lemma 7.37), as desired.

We are now able to prove our main result:

Proof of Theorem 6.25. By Theorem 7.39, T is intensionally fully abstract for ∼ M f , so by Lemma 7.32 ⟦-⟧ is intensionally fully abstract for ∼ S f . We thus conclude by Corollary 7.22.

7.4. Generalisation. We now show that our main results generalise beyond fair testing equivalence. Indeed, let us put: Definition 7.40. A pole is a property of states over fc(Σ) which is stable under strong bisimilarity.

There is a slight size issue in this definition, as it quantifies over elements of all graphs over fc(Σ). The reader may understand this using whatever fix they prefer, e.g., using a universe or some modal logic.

Example 7.41. Consider any x ∈ G over fc(Σ). We have • x is in the pole for fair testing equivalence iff for all x ← x ′ there exists x ′ ♡ ← x ′′ ; • x is in the pole for may testing equivalence iff there exists x ♡ ← x ′ . Must testing equivalence is less easy to capture, for reasons explained in [START_REF] Hirschowitz | Innocent strategies as presheaves and interactive equivalences for CCS[END_REF]. Here is an exotic, yet perhaps relevant pole: x is in it iff for all finite, not-necessarily silent transition sequences x ← ⋆ x ′ , there exists x ′ ♡ ← x ′′ . In other words, x never loses the ability to tick. The induced equivalence is clearly at least as fine as fair testing equivalence, but we leave open the question of whether or not it is strictly finer. Semantic testing equivalence may then be taken to be testing equivalence on C (Definition 7.7), and we get the exact analogue of Theorem 6.25 (without changing the model in any way).

Conclusion and future work

We have described our playground for π and the induced sheaf model, which we have proved intensionally fully abstract for a wide range of testing equivalences.

Regarding future work: our proof that traces form a playground uses a new technique based on factorisation systems. Since submission of this paper, we have designed [START_REF] Eberhart | Justified sequences in string diagrams: a comparison between two approaches to concurrent game semantics[END_REF][START_REF] Eberhart | Justified sequences in string diagrams: a comparison between two approaches to concurrent game semantics[END_REF] a general setting where this technique applies, and used it to bridge the gap between our notion of plays based on string diagrams and the standard one based on justified sequences [START_REF] Tsukada | Nondeterminism in game semantics via sheaves[END_REF]. We also consider applying our notion of trace to error diagnostics [START_REF] Gösler | Causality analysis in contract violation[END_REF] or efficient machine representation of reversible π-calculus processes [START_REF] Cristescu | A compositional semantics for the reversible π-calculus[END_REF]. Longer-term directions include applying the approach to more complex calculi, e.g., calculi with passivation [START_REF] Lenglet | Normal bisimulations in calculi with passivation[END_REF] or functional calculi, and eventually consider some full-fledged functional language with concurrency primitives. Finally, deriving the complex notion of trace evoked in Section 1.5 from the one exposed here is akin to deriving ltss from reduction rules [START_REF] Leifer | Deriving bisimulation congruences for reactive systems[END_REF][START_REF] Rathke | Deconstructing behavioural theories of mobility[END_REF]. Since the issue still seems easier on traces than on a full operational semantics specification, this might be worthwile to investigate further. In the same vein, the emphasis we put on traces suggests that we might be able to deduce properties of type systems (soundness, progress, etc) or compilers (correctness) from corresponding properties on traces.

Case 1

Case 2 P 1 There exist γ ′ 1 ⊢ P ′ 1 = a ′ 1 (b ′ ).P ′ + k 1 R ′ 1 and h 1 ∶ γ ′ 1 -∼ n 1 such that → γ]@(D 2 ⋅ o n 2 ,a 2 ,c 2 ) j [σ 2 ]@M 0 = M ′ .

P 1 = P ′ 1 [σ 1 ○ h 1 ] σ 1 (h 1 (a ′ 1 )) = a P = P ′ [γ ′ 1 , b ′ h 1 +! → n 1 + 1 σ 1 +⌜b⌝ → γ, b] D 1 = ⟦P ′ 1 ⟧ h 1 R 1 = R ′ 1 [σ 1 ○ h 1 ].
Q = Q ′ [γ ′ 2 , b h 2 +1 → n 2 + 1 σ 2 +⌜b⌝ → γ, b] σ 2 (h 2 (a ′ 2 )) = a σ 2 (h 2 (c ′ 2 )) = c D 2 = ⟦P ′ 2 ⟧ h 2 R 2 = R ′ 2 [σ 2 ○ h 2 ].
As in the previous cases, one can show that [P [b ↦ c], Q]@C 0 ⋈ M ′ . Heating, (LH). We now consider the case of heating, i.e., when one has a transition

C = (P Q)@C 0 τ ← [P, Q]@C 0 = C ′ .
We want to show that there exists a transition M τ ← M ′ with [P, Q]@C 0 ⋈ M ′ . We now have to consider a few cases, depending on which rule is applied for P Q in the proof of (P Q)@C 0 ⋈ M . Notice that P Q cannot be of the form ζ(D) [σ]. We are therefore left with two cases, depending on whether the first or third rule is applied.

• If the first rule is applied, we find M 0 , γ ′ ⊢ P ′ Q ′ , h∶ γ ′ -∼ n, and σ∶ n → γ such with P @C 0 ⋈ M ′ , as desired. We have thus proved that (LH) holds. We now proceed with the case analysis for (RH).

that P Q = (P ′ Q ′ )[σ ○ h] and M = ⟦P ′ Q ′ ⟧ h [σ]@M 0 , with C 0 ⋈ M 0 . Letting D = ⟦P ′ Q ′ ⟧ h ,
Synchro, (RH). We start, once again, with the case of the synchronisation, i.e., when M has the shape ⟨γ∥D 1 [σ 1 ], D 2 [σ 2 ]⟩@M 0 and we consider a silent transition to

M ′ = ⟨γ∥(D 1 ⋅ ι n 1 ,a 1 ) i [n 1 + 1 [σ 1 ,⌜σ 2 (b 2 )⌝] → γ], (D 2 ⋅ o n 2 ,a 2 ,b 2 ) j [σ 2 ]⟩@M 0 ,
where n i ⊢ D D i and σ i ∶ n i → γ for i = 1, 2, σ 1 (a 1 ) = a = σ 2 (a 2 ), and σ 2 (c 2 ) = c. We want to show that there exists a transition C id ← C ′ with C ′ ⋈ M ′ . There are exactly 10 cases here. Firstly, we have the case where the third rule is applied to D 1 [σ 1 ], D 2 [σ 2 ]. Otherwise, one could have used each of the three rules for ⋈ 0 for each of D 1 and D 2 , yielding nine cases. We start with the first case, and then treat the nine others.

• If the third rule is applied on D In the remaining cases, we have C = P 0 1 @P 0 2 @C 0 with P 0 i ⋈ D i [σ i ] for i = 1, 2, and C 0 ⋈ M 0 . We thus have four cases, described in Figure 9 just as we did in Figure 8.

• If the second rule is applied for both D 1 and D 2 , then there is a transition

C id ← C ′ = ζ((D 1 ⋅ ι n 1 ,a 1 ) i )[[σ 1 , ⌈c⌉]]@ζ((D 2 ⋅ o n 2 ,a 2 ,c 2 ) j )[σ 2 ]@M 0
with C ′ ⋈ M ′ as desired.

• If we apply the first rule for D 1 and the second rule for D 2 , then, choosing the same representative as before for P 1 [σ 1 ○ h 1 ], there is a transition

C id ← P ′ 1 [(σ 1 + 1) ○ h ′ 1 ][γ + 1 ↦ c]@ζ((D 2 ⋅ o n 2 ,a 2 ,c 2 ) j )[σ 2
]@C 0 = C ′ satisfying C ′ ⋈ M ′ (for the same reason as in the last case).

Fork, (RH). We consider the case of a forking action, i.e., M = ⟨γ∥D[σ]⟩@M 0 with n ⊢ D D and σ∶ n → γ, and we have a transition

⟨γ∥D[σ]⟩@M 0 id ← ⟨γ∥(D ⋅ π l n ) i [σ], (D ⋅ π r n ) j [σ]⟩@M 0
for some i and j. We want to show that there exists a transition C id ← C ′ with C ′ ⋈ M ′ . We proceed by case analysis on the rule applied for D[σ] in the proof of C ⋈ M .

• If the first rule is applied, then we find C 0 ⋈ M 0 , γ ′ ⊢ P = P 1 P 2 , and h∶ γ ′ -∼ n such that D = ⟦P ⟧ h , C = P [σ ○ h]@C 0 , (D ⋅ π l n ) i = ⟦P 1 ⟧ h , and (D ⋅ π r n ) j = ⟦P 2 ⟧ h . Thus, there is a transition Nu, (RH). We consider the case of a ν rule, i.e., one has a transition

P [σ ○ h]@C 0 id ← P 1 [σ ○ h]@P 2 [σ ○ h]@C 0 = C ′
C = ⟨γ∥D[σ]⟩@M 0 id ← ⟨γ∥(D ⋅ ν n ) i [n + 1 σ+⌈a⌉ → γ, a]⟩@M 0 [γ ⊂ γ, a]
with n ⊢ D D and σ∶ n → γ. We want to show that there exists a transition C id ← C ′ with C ′ ⋈ M ′ . We again proceed by case analysis on the rule applied for D[σ].

• If the first rule is applied, then we find C 0 ⋈ M 0 , γ ′ ⊢ P = νa.P ′ + k R, and h∶ γ ′ -∼ n such that C = P @C 0 , D = ⟦P ⟧ h and (D ⋅ ν n ) i = ⟦P ′ ⟧ h+1 . There are thus transitions

C = P [σ ○ h]@C 0 id ← P ′ [γ ′

Example 1 . 8 (

 18 [START_REF] Cacciagrano | Explicit fairness in testing semantics[END_REF]). The π-calculus features a well-known encoding of internal choice using channel creation and parallel composition. Mixing this with replication leads to intriguing examples of fair testing. Consider the following subtly different encodings of !(b ⊕ c), where ⊕ denotes internal choice and ! denotes replication: let R 1 =!νa.(a a.b a.c) and R 2 = νa.!(a a.b a.c). These are clearly fair testing equivalent. However, each encoding has an execution that always makes, say, the left choice, and Cacciagrano et al. argue that for R 1 this execution is fair, as the involved channel is different each time. They use similar examples to argue that fair testing is in fact too coarse, and instead propose alternative notions (which lie beyond the scope of this paper).

Figure 1 : 3 .

 13 Figure 1: Reduction rules for Conf

Definition 2 . 30 .

 230 A playground is a double category D such that cod is a fibration, equipped with • a full subcategory I ↪ D h of objects called individuals, • a full, replete 1 subcategory M ↪ D H , whose objects are called actions, with full subcategories B and F of basic and full actions, with F replete, • a map -∶ ob(D H ) → N called the length, satisfying the following conditions: (P1) I is discrete. Basic actions have no non-trivial automorphisms in D H . Vertical identities on individuals have no non-trivial endomorphisms. (P2) (Individuality) Basic actions have individuals as both domain and codomain. (P3) (Atomicity) For any cell α∶ v → u in D H , if u = 0 then also v = 0. Up to a special isomorphism in D H , all plays u of length n > 0 admit decompositions into n actions.

(

  P4) (Fibration, continued) Restrictions of actions (resp. full actions) to individuals either are actions (resp. full actions), or have length 0. (P5) (Views) For any action M ∶ Y X, and y∶ d → Y with d ∈ I, there exists a cell

α 1 α 2 (

 2 P8) (Finiteness) For any object X, the comma category I X (taken in D h ) is finite. (P9) (Basic vs. full) For all d ∈ I and actions M ∶ X d, M ′ ∶ X ′ d, and b∶ d ′ d with M and M ′ full and b basic, if there exist cells

Figure 2 :

 2 Figure 2: Categories of elements for [3], π 2 , and τ 1,1,3,2,3 , with graphical representation

Figure 3 :

 3 Figure 3: Pictures and corresponding cospans for π l p , π r p , o m,c,d , ι n,a , ♡ p , τ p , and ν p

Notation 3 . 6 .

 36 We denote by [m] a 1 ,...,ap c 1 ,...,cp[n] the position consisting of an m-ary agent x and an n-ary agent y, quotiented by the equations x ⋅ s a k = y ⋅ s c k for all k ∈ p. When both lists are empty, by convention, m = n and the agents share all channels in order. Definition 3.7. These cospans are called seeds.

  Intuitively, taking pushouts glues string diagrams together. Let us do a few examples. Example 3.10. The seed [2] [2] [ls,rs] → π 2 lt ← [2] has as interface the presheaf I [2] = ⋆ + ⋆, consisting of two channels, say a and b. Consider the position [2] + ⋆ consisting of an agent y connected to two channels b ′ and c, plus an additional channel a ′ . Further consider the map h∶ I [2] → [2] + ⋆ defined by a ↦ a ′ and b ↦ b ′ . The pushout

Figure 4 :

 4 Figure 4: Example traces

Lemma 3 . 15 .

 315 For any trace Y s → U t ← X, s and t are monos.

←Lemma 4 . 8 .

 48 Y with t ∈ V. Its vertical morphisms are stable under composition and contain identities by Lemma 4.3, i.e.: Lemma 4.5. D 1 forms a sub-double category of D 0 . Lemma 4.6. Traces are in D 1 v , i.e., we have D ⊆ D 1 . Proof. By Lemma 4.3.The main interest of introducing D 1 is:Lemma 4.7. The codomain functor cod∶ D 1 H → D 1 h is a fibration in which a double cell (3.2) is cartesian iff l ∈ H and the upper square is a pullback.Proof. Let us show that the lifting candidate computed in (4.1) is cartesian. Indeed, consider any double cell (4.1), and any morphism from some vertical morphism Z ′ → W ← Z to V whose bottom component factors through h∶ X → Y . By unique lifting in (V, H), we obtain a unique dashed arrow making finally obtain the desired arrow Z ′ → X ′ by universal property of pullback. Conversely, any cartesian double cell, being isomorphic to such a lifting, satisfies the conditions.As a final observation, let us record: Any morphism in D h is automatically in H.

Definition 4 . 14 .

 414 Let Agents(X) = ∑ n∈N X[n] denote the set of agents of any position X. Lemma 4.15. For any seed Y → C ← X, the morphism

4 . 5 .Lemma 4 . 18 .

 45418 [START_REF] Boreale | A fully abstract semantics for causality in the π-calculus[END_REF], it is enough to show that the middle arrow U → U ′ is in H and that its upper square is a pullback. The latter follows from Lemma 3.20. So we just have to show that any square V 0 admits a unique lifting C → U . By the Yoneda lemma, v amounts to an element of U ′ (C) of dimension > 1, but by construction U and U ′ have exactly the same such elements. This yields a candidate lifting, say k, which is unique by 1-injectivity and makes the bottom triangle commute by construction. The top one finally commutes by Corollary 4.16 with h = u and h ′ = kt. Restriction of actions. Let us now extend Lemma 4.9 from seeds to actions, following the strategy sketched at the beginning of Section 4. For any action Y s

Lemma 4 . 19 . 1 → B such that b is 1 j→making everything commute and so 1 i→

 419111 In sets, for any commuting diagram is a pullback, with the marked pushout and monos, the right-hand square is also a pullback.Proof. We check the universal property of pullback for A, relative to 1, which is enough in sets. So consider any commuting square observe that there is at most one mediating arrow 1 → A, because A → B is mono.If b has an antecedent in A, say a, then because C → D is mono, a makes both required triangles commute and we are done.Otherwise, by surjectivity of A + J → B, b admits an antecedent in J, i.e., there exists j∶ J → B, then we have a cone to C → D ← J, so we apply the universal property of pullback to obtain i as in 1 I → A suits our needs.

Definition 5 . 4 .

 54 Let B 0 be the full subcategory of D H having as objects basic actions and vertical identities between individuals. Lemma 5.5. (P5) For any action M ∶ Y X and y∶ d → Y in D h with d ∈ I, there exists a with v y,M ∈ B 0 .

Lemma 5 . 7 .

 57 (P8) For any X, I X is finite.Proof. All positions are finitely presentable presheaves. Lemma 5.8. (P9) For all d ∈ I and actions M ∶ X d, M ′ ∶ X ′ d, and b∶ d ′ d with M and M ′ full and b basic, if there exist cells M ← b → M ′ then M ≅ M ′ .

Figure 5 :

 5 Figure 5: Proof of Lemma 5.30

Lemma 6 . 10 .

 610 For any trace P ∶ Y X and y∶ d → Y in D h with d ∈ I, there exists an essentially unique cell

Definition 6 . 11 .

 611 This result allows us to describe what remains of a behaviour after a trace: Given any behaviour B ∈ B X and trace P ∶ Y X, the residual B ⋅ P of B along P is the behaviour determined (up to isomorphism) by (B ⋅ P ⋅ y)(w, id [ny] ) = B(v y,P • w, y P ) for all agents y∶ [n y ] → Y .

Definition 6 . 13 .

 613 For any n ∈ N and family B b ∈ B [n b ] indexed by all basic actions b∶ [n b ] [n], let ⟨B b ⟩ b denote the definite behaviour B determined by B ⋅ b = B b for all b. By construction, we have: Proposition 6.14. For any definite behaviour D ∈ B [n] , D ≅ ⟨D ⋅ b⟩ b .

l and D 2 ≅Proposition 7 . 3 .

 273 D ⋅ inj r , or otherwise said D ≅ [D 1 , D 2 ]. Lemma 2.18 entails: The morphism fc(p S )∶ fc(S) → fc(Σ), with S as testing relation, forms a free graph with testing.

Example 7 . 5 .

 75 Consider the trace P = (τ 0 • π 0 ) consisting of a nullary agent performing a τ action and then forking. Consider now any definite behaviour D such thatD(τ 0 ) = D(τ 0 • π l 0 ) = D(τ 0 • π r 0 ) = 2, which maps both inclusions τ 0 • π l 0 ↩ τ 0 ↪ τ 0 • π r 0 to the identity. Then D(P ) = 2: it consists of pairs (σ l , σ r ) in D(τ 0 • π l 0 ) × D(τ 0 • π r 0 )whose restrictions to D(τ 0 ) coincide, which leaves just (1, 1) and (2, 2). Using the decompositions of Section 6.2, another way to say this is thatD = ⟨τ 0 ↦ D 1 + D 2 ⟩, with D i = ⟨π l 0 ↦ D l i , π r 0 ↦ D r i ⟩, for i = 1,2. In order for C to correspond to the model, assuming D l 1 ≇ D l 2 and D r 1 ≇ D r 2 , there should be two transitions from ([0], D), one to ([0] [0], [D l 1 , D r 1 ]) and the other to ([0] [0], [D l 2 , D r 2 ]). But if we naively generalise Definition 7.1 to arbitrary traces, we obtain additional, 'incoherent' transitions, to ([0] [0], [D l 1 , D r 2 ]) and ([0] [0], [D l 2 , D r 1 ]

Definition 7 . 8 .Proposition 7 . 9 .→

 7879 Let D W v denote the smallest locally full subbicategory of D v containing all closed-world traces. The graph morphism W → Σ, where we recall that W denotes the graph of closed-world actions (Definition 5.1), extends to a pseudo functor p W ∶ D W v → fc(Σ), which essentially counts the number of ticks. Let p C ∶ C → D W v denote the obvious projection. The composite projection C fc(Σ), with S as testing relation, makes C into a graph with testing. Proof. Just as Lemma 7.3.

Notation 7 . 10 .

 710 For any morphism p∶ G → H in Gph, we denote by p A,B ∶ G(A, B) → H(p(A), p(B)) the component of p at A and B.

  ) in W and edge (X ′ , D ′ ) W → (X, D) in C over its right-associated, n-ary composition W = (M 1 • (. . . • M n )), there is a path e = (e 1 , . . . , e n ) in C ⋆ ((X ′ , D ′ ), (X, D)) such that (p C ) ⋆ (X ′ ,D ′ ),(X,D) (e) = p. Proof. By induction on n.

  by Lemma 7.12 and Corollary 7.15) iff (p C (X ′ ,D ′ ),(X,D) ) -1 (P ) ≠ ⊘ (by Lemma 7.11).

Corollary 7 . 19 .

 719 We have S = C . Let us also prove the analogous result with the semantic pole ⊥ ⊥. Lemma 7.20. We have D ∈ ⊥ ⊥ X iff (X, D) ∈ C . Proof. Assume D ∈ ⊥ ⊥ X , and consider any (X, D) ← (X ′ , D ′ ). The latter is witnessed by some unsuccessful, closed-world trace W ∶ X ′ X, state σ ∈ D(W ), and isomorphism h∶ (D ⋅ W ) ψ W (σ) -∼ D ′ .

Figure 6 :Notation 7 . 24 .Definition 7 . 25 .

 6724725 Figure 6: Transitions in M

Proposition 7 . 28 .

 728 The map m∶ ob(S) → M 0 is surjective. Let a denote any section of m.The point about bisimilarity is trickier: Proposition 7.29. We have (X, D) ∼ Σ m(X, D) for all (X, D) ∈ ob(S).

Proof.

  It is enough to prove that (the graph of) m is a strong bisimilarity up to strong bisimilarity. For this, let us record that clearly for any isomorphism h∶ X → Y of positions and D ∈ D Y , we have (Y, D) ∼ Σ (X, D ⋅ h) in S. Let us call I (for isomorphism) the relation given by all pairs ((Y, D), (X, D ⋅ h)), so that we have I ⊆ ∼ Σ . By case analysis, we can show that m is a strong bisimulation up to I, i.e., for all (X, D) α ← (Y, D ′ ), there exists (Y, D ′ ) I (Z, D ′′ ) such that m(X, D) α ← m(Z, D ′′ ), as below left. And more tightly, for all m(X, D) α

  D), and furthermore letting D ′′ be determined by D ′′ ⋅ x = D ′ ⋅ h(x) = D ⋅ x for x ≠ x 0 and D ′′ ⋅ x = D ′ ⋅ h(x 0 ), we have D ′′ = D ′ ⋅ h and hence (Y, D ′ ) I (X, D ′′ ) with m(X, D ′′ ) = M ′ , as desired.

Definition 7 . 31 .

 731 Let T∶ ob(Conf) → ob(M) denote the composite ob(Conf)

where x 1

 1 and x 2 denote the two agents of [n] [n]); • on the other hand ζ(D) has a silent transition toζ ′ i,j (D) = (ζ((D ⋅ π l n ) i ) ζ((D ⋅ π r n ) j )),which then has a further silent transition to the two-process configuration consisting of ζ((D ⋅ π l n ) i ) and ζ((D ⋅ π r n ) j ). Thus, when we try to relate D and ζ(D), the transition ζ(D) id ← ζ ′ i,j (D) has to be matched by the former transition D id ← ∂ i,j D. So our relation ⋈ should somehow include pairs (ζ ′ i,j (D), ∂ i,j D). Definition 7.35. Let the relation ⋈∶ Conf M over Σ be defined inductively by the rules in Figure 7.

Figure 7 :Lemma 7 . 36 .Lemma 7 . 37 .

 7736737 Figure 7: The relation ⋈ Lemma 7.36. We have C ⋈ T(C) for all C and Z(M ) ⋈ M for all M , and so ⋈ is total and surjective. Proof. By construction. Lemma 7.37. The relation ⋈ is a weak bisimulation over Σ.

  [D 1 [σ], D 2 [σ]]'s, related on the left to (ζ(D 1 ) ζ(D 2 ))[σ]'s, then all of the latter first have to heat to [ζ(D 1 )[σ], ζ(D 2 )[σ]], and only then perform the matching transition. This easily entails: Lemma 7.38. For all C 1

Definition 7 . 42 .

 742 For any such pole , let ∼ denote the testing equivalence induced by replacing G by in the definition of fair testing equivalence (Definition 2.14).

There exist n 2 ⊢

 2 D D 2 , a 2 , c 2 ∈ n 2 , and j ∈ D 2 ⋅ o n 2 ,a 2 ,c 2 such that σ 2 (a 2 ) = a σ 2 (c 2 ) = c P 2 = ζ(D 2 )[σ 2 ] Q = ζ((D 2 ⋅ o n 2 ,a 2 ,c 2 ) j )[σ 2 ].

Figure 8 : 1 [σ 1

 811 Figure 8: Synchro, (LH) cases• Case 2 for both P 1 and P 2 . We have a transitionM id ← (D 1 ⋅ ι n 1 ,a 1 ) i [n 1 + 1 [σ 1 ,⌈c⌉]

  we notice thatD = ⟨π l n ↦ ⟦P ′ ⟧ h , π r n ↦ ⟦Q ′ ⟧ h ⟩. Thus, there is a transition M τ ← M ′ = [⟦P ′ ⟧ h [σ], ⟦Q ′ ⟧ h [σ]]@M 0 with [P, Q]@C 0 ⋈ M ′ , as desired.• If the third rule is applied, we find M 0 , n ⊢ D D 1 , D 2 and σ∶ n → γ such thatP Q = (ζ(D 1 ) ζ(D 2 ))[σ]• If the second rule is applied, then we find M 0 , n ⊢ D D, and σ∶ n → γ such that C 0 ⋈ M 0 , M = D[σ]@M 0 , andξ.P + k R = ζ(D)[σ].Then, there exists i∈ D ⋅ ξ n such that ζ((D ⋅ ξ n ) i )[σ] = P . Hence, there is a transition M ξ ← (D ⋅ ξ n ) i [σ]@M 0 = M ′

1 [σ 1 ], D 2 [σ 2 ]

 1122 (hence n 1 = n 2 = n and σ 1 = σ 2 = σ), then we find C 0 such that C 0 ⋈ M 0 and C = (ζ(D 1 ) ζ(D 2 ))[σ]@C 0 . Then, we have a transition (ζ(D 1 ) ζ(D 2 ))[σ]@C 0 id ← [ζ(D 1 )[σ 1 ], ζ(D 2 )[σ 2 ]]@C 0 .Since the latter configuration is again related to M , this reduces to the case where the second rule is applied for bothD 1 [σ 1 ] and D 2 [σ 2 ]. • If the third rule is applied for D 1 [σ 1 ]and any of the three rules is applied forD 2 [σ 2 ],then we find P , M 1 , M 2 , C 0 , and n 1 ⊢ D D 3 such that M 1 has length 1 if the third rule is also used for D 2 and 0 otherwise,M 0 = D 3 [σ 3 ]@M 1 @M 2 , P ⋈ D 2 [σ 2 ]@M 1 , C 0 ⋈ M 2 , and C = (ζ(D 1 ) ζ(D 3 ))[σ 1 ]@P @C 0 .Thus, there is a transition(ζ(D 1 ) ζ(D 3 ))[σ 1 ]@P @C 0 id ← [ζ(D 1 )[σ 1 ], ζ(D 3 )[σ 1 ]]@P @C 0 which reduces this case to the one where the second rule is applied to D 1 . • If the third rule is applied for D 2 [σ 2 ] and any of the first two rules is applied for D 1 , then we find M 1 , P , C 0 , andn 2 ⊢ D D 3 such that M 0 = D 3 [σ 3 ]@M 1 , P ⋈ D 1 [σ 1 ], C 0 ⋈ M 1 , and C = (ζ(D 2 ) ζ(D 3 ))[σ 2 ]@P @C 0 . Again,we are reduced to the case where the second rule is applied for D 2 , using the transition (ζ(D 2 ) ζ(D 3 ))[σ 2 ]@P @C 0 id ← [ζ(D 2 )[σ 2 ], ζ(D 3 )[σ 2 ]]@P @C 0 .

2 ζ

 2 with C ′ ⋈ M ′ as desired.• If the second rule is applied, then we findC 0 ⋈ M 0 such that C = ζ(D)[σ]@C 0 . Thus, ζ(D)[σ] has the shape τ.(ζ((D ⋅ π l n ) i ζ((D ⋅ π r n ) j )))[σ] + k R (A.1)so we haveζ(D)[σ]@C 0 id ← (ζ((D ⋅ π l n ) i ) ζ((D ⋅ π r n ) j ))[σ]@C 0 = C ′ with C ′ ⋈ M ′ (using the third rule) as desired.• If the third rule is applied, then we find n ⊢ D D ′ , M 1 , andC 0 such that C 0 ⋈ M 1 , C = (ζ(D) ζ(D ′ ))[σ]@C 0 , and M 0 = D ′ [σ]@M 1 .But then, as in the previous case, ζ(D)[σ] has the shape (A.1) and we have transitions:(ζ(D) ζ(D ′ ))[σ]@C 0 id ← ζ(D)[σ]@ζ(D ′ )[σ]@C 0 id ← ((D ⋅ π l n ) i )[σ]@ζ((D ⋅ π r n ) j )[σ]@ζ(D ′ )[σ]@C 0 = C ′with C ′ ⋈ M ′ as desired.

, a h+1 → n + 1 σ+⌈a⌉→

 h+11 γ, a]@C 0 [γ ⊂ γ, a] = C ′ with C ′ ⋈ M ′ as desired.• If the second rule is applied, then we find C 0 ⋈ M 0 such that C = ζ(D)[σ]@C 0 , and there is a transitionζ(D)[σ]@C 0 id ← ζ((D ⋅ ν n ) i )[n + 1 σ+⌈a⌉ → γ, a]@C 0 [γ ⊂ γ, a] = C ′ with C ′ ⋈ M ′ as desired.• If the third rule is applied, then we find M 1 , C 0 , and n⊢ D D ′ such that M 0 = D ′ [σ]@M 1 , C 0 ⋈ M 1 , and C = (ζ(D) ζ(D ′ ))[σ]@C 0 . But then we have (ζ(D) ζ(D ′ ))[σ]@C 0 id ← ζ(D)[σ]@ζ(D ′ )[σ]@C 0 id ← ζ((D ⋅ ν n ) i )[n + 1 σ+⌈a⌉ → γ, a]@ζ(D ′ )[σ][γ ⊂ γ, a]@C 0 [γ ⊂ γ, a] = C ′ and C ′ ⋈ M ′ as desired.Tick and Tau, (RH). We now consider the cases ♡ and τ , i.e., when one has a transition⟨γ∥D[σ]⟩@M 0 ξ ← ⟨γ∥(D ⋅ ξ n ) i [σ]⟩@M 0where ξ ∈ {♡, τ }, with n ⊢ D D and σ∶ n → γ. We want to show that there exists a transitionC ξ ← C ′ with C ′ ⋈ M ′ .Again, we proceed by case analysis on the rule applied for D[σ].• If the first rule is applied, we findC 0 ⋈ M 0 , γ ′ ⊢ P = ξ.P ′ + k R, and h∶ γ ′ -∼ n such that C = P [σ ○ h]@C 0 , D = ⟦P ⟧ h [σ],and(D ⋅ ξ n ) i = ⟦P ′ ⟧ h . But then we have P [σ ○ h]@C 0 ξ ← P ′ [σ ○ h]@C 0 ⋈ ⟦P ′ ⟧ h [σ]@M 0 ,as expected. • If the second rule is applied, then C = ζ(D)[σ]@C 0 for some C 0 ⋈ M 0 and we haveζ(D)[σ]@C 0 ξ ← ζ((D ⋅ ξ n ) i )[σ]@C 0 ⋈ (D ⋅ ξ n ) i [σ]@M 0 ,as desired.• Finally, if the third rule is applied, then we find C 0 , M 1 , and n ⊢ D D ′ such thatC = (ζ(D) ζ(D ′ ))[σ]@C 0 , M 0 = D ′ [σ]@M 1 ,and C 0 ⋈ M 1 . But then, we have (ζ(D) ζ(D ′ ))[σ]@C 0 id ← ζ(D)[σ]@ζ(D ′ )[σ]@C 0 ξ ← ζ((D ⋅ ξ n ) i )[σ]@ζ(D ′ )[σ]@C 0 = C ′ with C ′ ⋈ M ′ as desired.

  1.6. Related work. Beyond the obviously closely related, already mentioned work of Winskel et al., we should mention other causal models for π

  and x ¨G x ′ , then there exist u ∈ (x G x ′ ) and v ∈ (y H y ′ ) such that u R v.

	Lemma 2.21. A relation R∶ ob(G)	ob(H) between the vertex sets of two graphs with
	testing p G ∶ G → fc(Σ) and p H ∶ H → fc(Σ) is fair iff its converse R † is, where R † is defined by (y R † x) ⇔ (x R y). Proof. Easy. Lemma 2.22. For any fair relation R∶ ob(G) ob(H), if x R y and x ′ R y ′ , then (x ∼ G f x ′ ) ⇔ (y ∼ H f y ′ ). For proving this lemma, we need:
	Lemma 2.23. For all graphs with testing p

  hence by a similar argument (y ′ t) ∈ H , as desired.Definition 2.24. A relation R∶ ob(G)ob(H) between the vertex sets of two free graphs with testing respectively generated by p G ∶ G → Σ and p H ∶ H → Σ is weakly fair iff it satisfies the conditions of Definition 2.20, except for the third one, which is replaced by: x R y implies x ≈ Σ y.

	Corollary 2.25. For any weakly fair relation R∶ ob(G)	ob(H), if x R y and x

  ′′ → E and k∶ p(E ′′ ) → p(E ′ ), if p(r)○k = p(t) then there exists a unique s∶ E ′′ → E ′ such that p(s) = k and r ○ s = t. Definition 2.26. A functor p∶ E → B is a fibration iff for all E ∈ E, any h∶ B ′ → p(E) has a cartesian lifting, i.e., a cartesian antecedent by p. Notation 2.27. We denote by E h the domain of the (chosen) cartesian lifting, and call it the restriction of E along h.

	t
	s
	p(t)
	k
	r)
	for all t∶ E

  The only non-obvious point is that double cells in D are closed under vertical composition, and in particular that the middle component of the composite is 1-injective. This follows from Lemma 3.20 and Corollary 3.22 below. Definition 3.19. Let V 0 denote the set of 't'-legs (i.e., lower legs) of seeds.

	Proposition 3.18. D indeed forms a sub-double category of D 0 , i.e., is closed under all composition operations. H , if U and V are traces, then the upper square is a pullback. Proof. Lemma 3.20. For any morphism (3.2) in D 0 Proof. For any trace Y

2)

Definition 3.17. Let D denote the sub-double category of D 0 obtained by restricting

• vertical morphisms to traces,

• horizontal morphisms to 1-injective maps,

• double cells to diagrams (3.2) in which k, l, and h are 1-injective.

s

  ) whose image will consist precisely of all 'coherent' elements. (From now on, we omit the superscript D when clear from context.) Intuitively, this map associates to each global state the corresponding family of local states. Furthermore, ψ P is always injective, but Example 7.5 shows that it is not surjective in general. In order to construct ψ P , recalling Definition 6.11, we have by definition: ∏ y∶[ny]→Y D ⋅ P ⋅ y = ∏ y∶[ny]→Y D(v y,P , y P ).

  There exist n 1 ⊢ D D 1 , a 1 ∈ n 1 , and i ∈ D 1 ⋅ ι n 1 ,a 1 such that σ 1 (a 1 ) = a P 1 = ζ(D 1 )[σ 1 ] P = ζ((D 1 ⋅ ι n 1 ,a 1 ) i )[n 1 + 1 There exist γ ′ 2 ⊢ P ′ 2 = ā′ 2 ⟨c ′ ⟩.Q ′ + k 2 R ′ 2 and h 2 ∶ γ ′ 2 -∼ n 2 such that P 2 = P ′ 2 [σ 2 ○ h 2 ]

	σ 1 +⌜b⌝ → γ, b].
	P 2

where

• in any list ⟨b 1 ↦ B 1 , . . . , b m ↦ B m ⟩, all unmentioned basic actions are meant to be mapped to the empty behaviour; • the definite sum ⊞ i D i of definite behaviours D i is the definite behaviour determined by (⊞ i D i ) ⋅ b = ∑ i (D i ⋅ b), for all basic actions b∶ [n ′ ]

[n]; • and h ′ ∶ γ, b -∼ n + 1 maps any a ∈ γ to h(a), and b to n + 1.

Example 6.20. Let us briefly illustrate the translation. Consider any h∶ γ → γ and processes γ, b ⊢ P , γ, b ⊢ Q, and γ ⊢ R, with a ∈ γ. We can form a(b).P + a(b).Q + ā⟨a⟩.R, which is mapped to ⟨ι γ ,h(a) ↦ (⟦P ⟧ h ′ + ⟦Q⟧ h ′ ), o γ,h(a),h(a) ↦ ⟦R⟧ h ⟩.

To emphasise the difference, using coproduct of behaviours instead of definite sum in the translation would yield a behaviour with three distinct initial states, closer to the internal choice a(b).P ⊕ a(b).Q ⊕ ā⟨a⟩.R than to the original process.

Generalising this to configurations should really be intuitive: we map any ⟨γ∥P 1 , . . . , P n ⟩ to some behaviour on the position X with X(⋆) = γ and n agents of arity γ , given for each agent i ∈ n by ⟦P i ⟧. In order to fully define such a position, we need to specify maps f i ∶ γ → γ. We use for all of them the inverse of the canonical bijection h γ defined by: Definition 6.21. Let h γ ∶ γ -∼ γ map each a ∈ γ to its position in the ordering induced by the one on natural numbers.

We call the obtained position X(γ, n). Definition 6.22. Let ⟦-⟧∶ ob(Conf) → ∑ X B X map any configuration C = ⟨γ∥P 1 , . . . , P n ⟩ to the pair (X(γ, n), ⟦C⟧), where ⟦C⟧ is defined through Proposition 6.8 by ⟦C⟧( γ

for all i ∈ n. We implicitly consider processes P over γ as configurations ⟨γ∥P ⟩, and hence allow ourselves to write ⟦P ⟧ for ⟦⟨γ∥P ⟩⟧.

6.4. Semantic fair testing. In order to state our main result, it remains to define our semantic analogue of fair testing equivalence. It rests on two main ingredients: a notion of closed-world trace, and an analogue of parallel composition in game semantics. The intuitive purpose of parallel composition is to let behaviours interact. If we partition the agents of a position X into two teams, we obtain two subpositions X 1 ↪ X ↩ X 2 , each agent of X belonging to X 1 or X 2 according to its team. The crucial fact is that the category V X of views on X is isomorphic to the coproduct category V

(following Notation 6.9), as in

Appendix A. Proof of Lemma 7.37

One wants to check two properties:

The attentive reader will have noticed that (LH) imposes y to answer with a single transition. This means we actually prove that ⋈ is an expansion [68, Chapter 6]. Any expansion being in particular a weak bisimulation, this suffices.

Notation A.1. We sometimes cast processes P (resp. pairs D[σ]) over γ into configurations ⟨γ∥P ⟩ (resp. mixed behaviours ⟨γ∥D[σ]⟩). We proceed similarly for multisets of processes.

We start by proving (LH) for all cases, before proving that (RH) holds as well.

Synchro, (LH). We begin by the case of a synchronisation, i.e., when one has a transition

We want to show that there exists a transition

Neither of them are of the form (⋅ ⋅) so they can only be related to mixed behaviours using the first two rules. Therefore, four sub-cases should be considered, as detailed in Figure 8. If we are in case i 1 for P 1 and i 2 for P 2 , then we have two mixed behaviours

• Case 1 for both P 1 and P 2 . We have

]@M 0 , and there is a transition

• Case 1 for P 1 , Case 2 for P 2 . We have a transition

• Case 2 for P 1 , Case 1 for P 2 . We have a transition

Nu, (LH). We now consider the case of a ν rule, i.e., when one has a transition

We want to show that there exists a transition

We notice that νa.P + k R cannot be obtained from the third rule. We thus consider two cases corresponding to the first and second rules.

• If the first rule is applied, there exist M 0 , γ ′ ⊢ νa.P ′ + k R ′ , h∶ γ ′ -∼ n, and σ∶ n → γ

We write D = ⟦νa.

Thus, there exists i

Tick and Tau, (LH). We now consider the cases ♡ and τ , i.e., when one has a transition

where ξ ∈ {♡, τ }. We want to show that there exists a transition M ξ ← M ′ with P @C 0 ⋈ M ′ . Once again, the third rule could not have been applied, and we are left with two cases corresponding to the first and second rules.

• If the first rule is applied, then we find M 0 , γ ′ ⊢ ξ.P ′ + k R ′ , h∶ γ ′ -∼ n, and σ∶ n → γ

We write D = ⟦ξ.P ′ + k R ′ ⟧ h as ⟨ξ n ↦ ⟦P ′ ⟧ h ⟩ ⊞ ⟦R ′ ⟧ h . Thus, there is a transition

with P = P ′ [σ ○ h] and thus P @C 0 ⋈ M ′ , as desired.

Case 1 Case 2

• If the first rule is applied for both D 1 and D 2 , then we have a synchronisation between P 1 [σ 1 ○ h 1 ] and P 2 [σ 2 ○ h 2 ]. In order to determine the result of this synchronisation we need to choose a representative for P 1 [σ 1 ○ h 1 ], i.e., pick a channel for what b becomes after substitution. A reasonable choice here is γ + 1, we choose

We thus have a transition to

commutes, so

Finally, we also know:

@M 0 , which entails C ′ ⋈ M ′ as desired.