an intensionally fully abstract sheaf model for pi

Following previous work on CCS, we propose a compositional model for the pi-calculus in which processes are interpreted as sheaves on certain simple sites. 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 strategy is fair testing equivalent to the interpretation of some process. The central part of our work is the construction of our sites, whose heart is a combinatorial presentation of pi-calculus traces in the spirit of string diagrams. As in previous work, the sheaf condition is analogous to innocence in Hyland-Ong/Nickau games.

section_content: 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 [17]. 

Causal models, originally designed for Petri nets [37] and Milner's CCS [42], 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. [10] to Milner's π-calculus, and (2) by Melliès [32] 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 [36, 24] ). An important challenge is now the search for a causal model of full-fledged languages with both concurrent and functional features. Winskel and collaborators are currently working in this direction, using extensions of Melliès's approach [39, 43, 8]. 

In previous work [23, 21, 22], 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.
section_name: Introduction

section_content: 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 briefly sketch. There is first a (straightforward) notion of configuration, 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 configuration to another, 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 configuration 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 configuration X and final configuration Y as morphisms Y X. Sequential composition of traces, denoted by •, yields an analogue of prefix ordering, defined by t ≤ t • w. This however fails to suit our needs on three counts. 

We start by examining the first two problems. 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 (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 either on b or on c. The process Q inputs on a and then has both possibilities of inputting on b or c. 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 [26], 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 our traces naturally form a proper category T(X), encompassing both prefix ordering and isomorphisms between traces, so we are led to considering functors T(X) op → 2. This 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.
section_name: Traces and naive concurrent strategies

section_content: In Example 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:

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 identifying 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. 

Notation 3. For any C, let Û C denote the category of presheaves of finite sets over C.
section_name: Example 2.

section_content: 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 4. Consider a configuration 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 19). 

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 configuration X, but also traces on all possible subconfigurations of X. Furthermore, this local information should fit together coherently. 

Example 5. Consider the configuration X of Example 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 she sees 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's 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 [24]. In order to formalise it, we first extend our category of traces T(X) on X with new objects representing traces on subconfigurations of X. We also add new morphisms, which are about 'locality': Example 6. Consider the configuration X with two unary agents x 1 and x 2. There is a trace t on X in which both agents fork. Consider now the subconfiguration 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, which are obtained by sequentially composing atomic actions whose final configuration 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 subcategory V X of T X. 

Example 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 [30] 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 4. 

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. (This forgetful functor has a left adjoint. ) Finally, because the considered topology is particularly simple, sheaves are equivalent to presheaves on views, i. e., S X ṼX (recalling Notation 3). In summary, we have three categories of strategies: naive strategies are presheaves on 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.
section_name: Innocence as a sheaf condition

section_content: 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. The natural thing to do is thus to choose some behavioural equivalence from the operational side, 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 translationinduces a bijection between both extensional collapses. Following [1], we call this intensional full abstraction for the considered equivalence. 

We here focus on so-called testing equivalences [11, 35, 5, 38], 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. 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 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 (see [7] for some motivation and an adaptation to π), one requires that all silent sequences (P | T ) = ⇒ P extend to some sequence P = ⇒ P ♥ -→ P ending with a ♥ transition. In this paper, we focus on the latter, i. e., we prove (Theorem 25) that our model is intensionally fully-abstract for fair testing equivalence. However, we show in the long version [12] that our proof applies to a wide range of testing equivalences.
section_name: Main result

section_content: Since this paper follows the same approach as previous work on CCS [23, 21, 22], 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 (see our online draft [12] for details), we need to show that traces form the total category of a fibration [25] over configurations. In previous work, this was done in an ad hoc way. We here introduce a more satisfactory approach based on factorisation systems [28, 15]. 

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, as sketched in Section 4. 

Finally, as mentioned above, our proof now applies not only to fair testing equivalence, but also to a whole class of testing equivalences.
section_name: Contributions

section_content: Beyond the obviously closely related, already mentioned work of Winskel et al., we should mention other causal and interleaving models for π, e. g., [34, 13, 4, 9, 10, 6, 14, 40, 19]. 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 [22]. 

Another general framework relating operational and denotational descriptions of programs is Kleene coalgebra [3], 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) π [27], 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 [18] 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 [41] adapts and extends some ideas of [23, 21] to nondeterministic, simply-typed λ-calculus. 

Let us moreover mention less closely related work: Girard's ludics [16], Melliès's game semantics in string diagrams [33], Harmer et al. 's categorical combinatorics of innocence [18], McCusker et al. 's graphical foundation for schedules [31]. Finally, Hildebrandt's work [20] also uses sheaves, though for a quite different purpose.
section_name: Related work

section_content: We describe our notion of trace at length in Section 2. We then sketch the model produced by the machinery of playgrounds, and state our main result in Section 3. We then conclude in Section 4, with a brief sketch of the proof and some future directions.
section_name: Plan

section_content: 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. Configurations 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 configurations, because we not only want to say when there is an action from one configuration 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 Û C, 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 configurations, and that M describes how one goes from X to Y. By combining such actions (by pushout), we get a bicategory D v of configurations and traces.
section_name: Traces

section_content: The category Û C will be a category of 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 [1], and two non-identity morphisms s, t : → [1]. Any such presheaf G represents the graph with vertices in G( ) and edges in G [1], the source and target of any e ∈ G [1] 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 [30]. Recall that the category of elements 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 G π G --→ C y -→ Ĉ with the Yoneda embedding. E. g., the category of elements for y [1] is the poset (, s) (, 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. 

Our string diagrams will also be defined as particular presheaves over some base category C. However, since we'll only be interested in finite structures, we restrict ourselves to the category Û C of presheaves of finite sets. In the case of graphs, presheaves of finite sets are graphs whose nodes and edges are identified by natural numbers. Such graphs are thus finite. In our case, the base category C is infinite, so presheaves of finite sets may represent infinite structures. However, our notion of trace will only involve finite ones. 

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 graphical intuition.
section_name: String diagrams

section_content: (, s 1 ) (, s 2 ) (, s 3 ) ( [3], id [3] )

Let C be the free category on G C, modulo the equations

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

The second equation should be understood in C(, π 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.
section_name: C A L C O ' 1 5

section_content: C. To explain the design of C, let us compute a few categories of elements. Let us start with an easy one, that of [3] ∈ C (we implicitly identify any c ∈ C with yc). An easy computation shows that it is the poset pictured in the top left part of Figure 1. We think of it as a configuration with one agent ( [3], id [3] ) connected to three channels, and draw it as in the top right part, where the bullet represents the agent, and circles represent channels. In the presheaf, elements over [3] represent ternary agents, while elements over represent channels. Configurations are finite presheaves empty except perhaps on and [n]'s. Other objects will represent actions. A morphism of configurations is a morphism between presheaves which is injective except perhaps on channels. The intuition for a morphism X → Y between configurations is thus that X embeds into Y, possibly identifying some channels.
section_name: Our category of string diagrams is the category of finite presheaves Û

section_content: A more difficult category of elements is that of π 2. It is the poset generated by the left-hand graph in the second row of Figure 1 (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 graphical convention is that a black triangle stands for the presence of id π2, l, ♥ ♠

[p] and r. Below, we represent just l as a white triangle with only a left-hand branch, and symmetrically for r. Furthermore, in all our pictures, time flows 'upwards'. 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 on the bottom left of Figure 1, 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 1st 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 objects. 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. 

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 2, 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 as standard in the π-calculus. The ♥ n action is a special 'tick' action used for defining fair testing equivalence. The last one is a channel creation action.
section_name: Definition 9. Configurations and morphisms between them form a category D h .

section_content: In the previous section, we have defined our category of string diagrams as Û C, and provided some graphical intuition on its objects. The next step is to construct a bicategory whose objects are configurations, 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 the local forms of actions, which are then defined by embedding seeds into bigger configurations. 

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 configurations, say X and Y, and view the whole action as a cospan
section_name: From string diagrams to actions

section_content: We have taken care, in drawing our pictures before, of placing initial configurations at the bottom, and final configurations at the top. So, e. g., the initial and final configurations for the synchronisation action are pictured above and they map into (the representable presheaf over) τ 1,1,3,2,3 in the obvious ways, yielding the cospan

We leave it to the reader to define, based on the above pictures, the expected cospans for forking and synchronisation as on the right, plus the remaining ones specified in the bottom row of Figure 2 We now define actions from seeds by embedding the latter into bigger configurations. E. g., we allow a fork action to occur in a configuration with more than one agent. 

Since channels occurring in the initial configuration 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 on the right yields a new cospan, say Y → M ← X. 

The meaning of such an action is that x forks while y is passive. 

Example 14. 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 configuration.
section_name: C A L C O ' 1 5

section_content: Having defined actions, we now define their composition to yield our bicategory D v of configurations and traces. Consider Cospan( Û C), the bicategory which has as objects all presheaves of finite sets 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. 3, 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 configuration, 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.
section_name: From actions to traces

section_content: Strategies, behaviours, and semantic fair testing
section_name: 3

section_content: We now investigate 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 on the right 1. Thus, u is an extension of u by w. 

Definition 18. Let the category of (naive) strategies on X be T(X).
section_name: Strategies and behaviours

section_content: Example 19. Consider the configuration 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 sub-configurations 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 triple (s, k, r) making the diagram on the right commute 1. 

y Example 20. We adopt the convention of picturing the above diagram for morphisms as the left-hand diagram below: Now recalling the right-hand trace of Figure 3, say u : Y X, y's first action is an input on its unique channel b. This yields a trace ι 1,1 : [2] [1]. There is a morphism (ι 1,1, y) → (u, id X ) in T X, pictured as the right-hand diagram, which we think of 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 configuration. 

We now define views within T X :

Definition 21. Let basic seeds be all seeds of any shape among ι n,a, o n,a,b, ν n, ♥ n, τ n, π l n, and π r n, for a, b ∈ n. Views are (possibly empty) composites of basic seeds in D v. Let V X denote the full subcategory of T X spanning pairs (u, h) where u is a view. 

Intuitively, basic seeds 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 22. The inclusion V X → T X induces a Grothendieck topology, for which a family (u i αi -→ u) i∈I of morphisms to some trace u is covering iff it contains all morphisms from views into u. Let the category S X → TX of innocent strategies be the category of sheaves of finite sets for this topology. Let the category B X of behaviours over X be ṼX. 

As promised, S X and B X are equivalent. We obtain the innocent strategy S B associated to a behaviour B ∈ B X, by taking its right Kan extension [29] along the inclusion j op : V op X → T op X, as on the right. 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 a 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. Existence of the right Kan extension is proved in the general case in [22, Lemma 4. 34], and follows from the general fact that the considered limits are essentially finite. The forgetful functor U to naive strategies is then given by restricting along T(X) op → T op X as above right. Some local information may be forgotten by U, which is neither injective on objects, nor full, nor faithful. E. g., if two behaviours differ, but are both empty on the views of some agent, then both are mapped to the empty naive strategy. 

Example 23. Recalling X and S from Example 19, let us show that for any B ∈ B X, the associated strategy U(S B ) ∈ T(X) cannot be S. Indeed, assuming it is, then because S accepts u x,y and i z, B accepts 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 ) accepts both u x,y and u x,z, because B accepts all views mapping into them.
section_name: Strategies do not yield a satisfactory model for π:

section_content: We now define our semantic analogue of fair testing equivalence, sketch our translation from π, and state our main result. Semantic fair testing 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 strategies interact. If we partition the agents of a configuration X into two teams, we obtain two subconfigurations 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 X1 + V X2. Parallel composition of any B 1 ∈ B X1 and B 2 ∈ B X2 is then simply given by copairing [B 1, B 2 ] as above. 

We now describe closed-world actions and traces, which are then used as a criterion for success of tests. Closed-world actions are those which do not involve 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 T(X) denote the full subcategory of T(X) consisting of closed-world traces, and let the category of closed-world strategies be Ẇ(X). Further, denote by B → B the composite functor ṼX → T(X)

, where ∆ i op denotes restriction along i op. A closed-world trace is successful when it contains a ♥ action, and unsuccessful otherwise. A state σ ∈ S(u) of a strategy 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 σ
section_name: Semantic fair testing

section_content: We now sketch our translation from π-calculus processes to behaviours and state our main result. First, we consider processes to be infinite terms as generated by the grammar up to renaming of bound variables as usual. Such a coinductive definition requires some care [12] : notably, processes come equipped with their finite set Γ of free channels, which we denote by Γ P. In order to translate processes to behaviours, we denote the coproduct in B X by ⊕ (which is the pointwise coproduct of presheaves). Furthermore, let us denote by

where (1) ā b = o Γ,a,b, a(b) = ι Γ,a, νa = ν Γ, ♥ = ♥ Γ, and τ = τ Γ, (2) all unmentioned basic seeds are mapped to the everywhere empty behaviour ∅, (3) Γ • α i denotes Γ + 1 when α i is an input or a channel creation 2, and Γ otherwise. E. g., we have Γ a(b). P + a(b). Q = ι Γ,a → Γ + 1 P ⊕ Γ + 1 Q. We then define fair testing equivalence ∼ Pi f for π-calculus processes as in [7] : let ⊥ Pi denote the set of processes P such that for all P = ⇒ P there exists P = ⇒ P ♥ -→ P, and, given any two processes Γ P and Γ Q, let P ∼ Pi f Q iff for all Γ T we have (P | T ∈ ⊥ Pi ) ⇔ (Q | T ∈ ⊥ Pi ). Finally, our main result is: Theorem 25. 1. For all P, Q,

For all B over [Γ], there exists a process Γ P such that Γ P ∼ f B.
section_name: Intensional full abstraction

section_content: We have described our notion of trace and the induced model of π. We then have stated our main theorem. In our online long version [12], the interested reader may find the proof that our traces organise into a playground [22], and the proof of Theorem 25. For lack of space, we cannot give any detail. Still, we sketch the latter. The idea is to reduce semantic fair testing equivalence to fair testing equivalence in the standard sense for some ad hoc lts S. We then single out a particular quotient M of S, which admits a syntactic description very close to Berry and Boudol's chemical abstract machine [2], though with a kind of persistent explicit substitutions. Elements of M thus roughly consist of finite multisets of molecules. Multisets are here thought of as chemical soups, in which synchronisation is viewed as interaction between compatible molecules. In order to simplify matters, we also work with a chemical abstract machine presentation of the π-calculus. We then define a candidate 'pseudo-inverse' ζ to the translation map -. These are maps between molecules for π and molecules for M, which extend straightforwardly to chemical soups. We finally design a relation between π-calculus soups and M soups, which modularly allows π-calculus processes to correspond to their translation, and M-molecules to correspond to their image under ζ. We are then able to show that this relation is a weak bisimulation which straightforwardly entails thatboth preserves and reflects fair testing equivalence and is surjective up to fair testing equivalence, i. e., is intensionally fully-abstract. 

Regarding future work, we of course plan to extend our approach to more complex calculi, e. g., calculi with passivation or functional calculi, and eventually consider some full-fledged functional language with concurrency primitives. Furthermore, we consider generalising our technique for constructing playgrounds and applying them, e. g., to graph rewriting, error diagnostics, or efficient machine representation of reversible π-calculus processes.
section_name: Conclusion and future work