Simon Castellan

Pierre Clairambault

Glynn Winskel

The Mays and Musts of Concurrent Strategies

Concurrent strategies based on event structures are examined from the viewpoint of 'may' and 'must' testing in traditional process calculi. In their pure form concurrent strategies fail to expose the deadlocks and divergences that can arise in their composition. This motivates an extension of the bicategory of concurrent strategies to treat the 'may' and 'must' behaviour of strategies under testing. One extension adjoins neutral moves to strategies but in so doing loses identities w.r.t. composition. This in turn motivates another extension in which concurrent strategies are accompanied by stopping configurations; the ensuing stopping strategies inherit the structure of a bicategory from that of strategies. The technical developments converge in providing characterisations of the 'may' and 'must' equivalences and preorders on strategies.

Introduction

This article relates to work on process calculi of the 1980's but from a modern perspective of processes as strategies, specifically as distributed/concurrent strategies based on event structures. It expands on two areas close to Samson Abramsky's heart, game semantics and concurrency: on a development of concurrent games based on event structures which extends his early ideas with Paul-André Melliès of deterministic concurrent strategies as closure operators [START_REF] Abramsky | Concurrent games and full completeness[END_REF]; and equivalences on concurrent processes through testing [START_REF] Abramsky | Observation equivalence as a testing equivalence[END_REF].

Robin Milner and Tony Hoare's work of late seventies and early eighties drew attention to equivalences on processes; Milner's on forms of bisimulation [START_REF] Milner | A Calculus of Communicating Systems[END_REF] and Hoare's on failures equivalence [START_REF] Brookes | A theory of communicating sequential processes[END_REF]. Hoare had described failure equivalence informally as the minimum extension of trace equivalence that takes account of the possibility of failure due to deadlock. Matthew Hennessy and his PhD student Rocco de Nicola provided a rationale through an idea of testing processes [START_REF] De Nicola | Testing equivalences for processes[END_REF]. For them a test was a process with distinguished "success" states at which an action ✓ could occur. Putting a test in parallel composition with a process, may lead to success if some run does or must lead to success if all runs do. Processes can be regarded as equivalent if they have the same 'may' and 'must' behaviour w.r.t. tests. Modulo subtleties to do with the divergence of processes, Hennessy and de Nicola recovered failure equivalence as testing equivalence. What about Milner's central equivalence? Samson Abramsky investigated the extent to which bisimulation could be viewed as a testing equivalence [START_REF] Abramsky | Observation equivalence as a testing equivalence[END_REF]: it could, but only at the cost of strengthening the power of tests considerably, by allowing testing to run and copy processes quite liberally.

Here we shall examine the 'may' and 'must' equivalence of concurrent strategies based on event structures [START_REF] Rideau | Concurrent strategies[END_REF][START_REF] Castellan | Games and strategies as event structures[END_REF]-foreshadowed in the early definitions of concurrent strategy [START_REF] Abramsky | Concurrent games and full completeness[END_REF][START_REF] Ghica | Angelic semantics of fine-grained concurrency[END_REF][START_REF] Melliès | Asynchronous games : innocence without alternation[END_REF][START_REF] Faggian | Partial orders, event structures and linear strategies[END_REF]. Informally, a strategy for Player in a twoparty game against Opponent, expresses a choice of Player moves, most often in reaction to moves made by Opponent, unpredictable for Player but for the constraints of the game. We shall implicitly regard a strategy as a strategy for Player. We regard Opponent as the environment uncontrollable by Player. We can express both the game-its moves and their constraints-and a strategy-its choice of Player moves subject to the moves of Opponent-as event structures. This chimes with our view of strategies and games as highly distributed. Player and Opponent are more accurately thought of as teams of players and opponents acting at possibly very different locations. Though we take the rather abstract view of location advocated by Petri in his concept of local state as a condition (or place): then locality reveals itself through the causal dependence and independence of events.

Event structures are the concurrent analogue of trees; just as transition systems unfold to trees, so Petri nets unfold to event structures. Whereas an unfolded behaviour of a transition system comprises sequences of actions/events, the unfolded behaviour of a Petri net, in which events make local changes to conditions, comprises partial orders of causal dependency between event occurrences [START_REF] Nielsen | Petri nets, event structures and domains[END_REF]. Event structures are a central model for concurrent computation, related to other models by adjunctions [START_REF] Winskel | Models for concurrency[END_REF]. This plants concurrent strategies based on event structures firmly within theories of concurrency and interaction-anticipated in Abramsky's presentation of game semantics, with its emphasis on composition of strategies as given by their parallel interaction followed by hiding. Perhaps more controversially, the view of processes as strategies suggests refinements to the assumptions usual in process calculi. In concurrent strategies, gone is the usual symmetry between a process and its environment; the conditions on a concurrent strategy take account of the unpredictability and uncontrollability of Opponent moves. This affects the appropriate equivalences to impose between concurrent strategies.

There is surely a long history behind the idea of composing strategies. Certainly the idea plays a key role in John Conway's "On Numbers and Games" [START_REF] Conway | On Numbers and Games[END_REF], the categorical underpinnings of which were exposed by André Joyal [START_REF] Joyal | Remarques sur la théorie des jeux à deux personnes[END_REF]. For two-party games there is the obvious operation of reversing the roles of the two participants, Player and Opponent; this operation, forming the dual G ⊥ of a game G, played the role of negation for Conway. A useful convention is to regard a strategy in a game G as a strategy for Player; then a strategy for Opponent, or counter-strategy, is a strategy in the dual game G ⊥ . If the games are broad enough, they often support a form of parallel composition, G∥H; for Conway it was the sum of games. A strategy from a game G to a game H is a strategy σ in the game G ⊥ ∥H. Given another strategy this time from the game H to the game K, i.e. a strategy τ in the game H ⊥ ∥K, we can let the strategies interact as τ ⊛ σ, essentially by playing them against each other over the common game H; there the strategies σ and τ adopt complementary roles-where one makes a move of Player in H the other sees a move of Opponent and vice versa.

The interaction τ ⊛ σ involves moves in the parallel composition of all three games, G ⊥ ∥H∥K, though in writing the parallel composition in this way an imprecision has crept in: whereas the moves over G ⊥ and K described by τ ⊛ σ are choices of moves for Player or moves open to choices of Opponent, those over H are either instantiations of Opponent moves of σ by Player moves of τ , or the converse, instantiations of Opponent moves of τ by Player moves of σ. As such the moves of τ ⊛ σ over H behave like synchronisations between complementary moves of σ and τ , and as events internal to the interaction. Though internal, the events over H can affect the behaviour of the interaction by introducing deadlocks or divergence. In the composition of strategies it is usual to hide the internal events of interaction to obtain a strategy τ ⊙τ in the game G ⊥ ∥K, where the game H is elided to obtain a strategy from G to K. However when the original strategies σ or τ are nondeterministic significant behavioural distinctions can be lost in hiding internal events. In particular, the hidden events can affect the 'must' behaviour of the composition of strategies.

Contributions of the paper

This brings us to the concerns of this paper. It motivates the definition of bare concurrent strategies in which internal events are exposed as neutral moves in the strategy. Through bare strategies we can examine the 'may' and 'must' testing of strategies. Although bare strategies compose their composition does not have identities, so they fail to form a bicategory. We have explored two ways to recover a bicategory while remaining faithful to the 'must' behaviour of strategies. One is through "essential events" in which one strips a bare strategy down to just those neutral moves critical to its behaviour [START_REF] Castellan | Non-angelic concurrent game semantics[END_REF]. The other, that we follow here, is through extending strategies with the extra structure of stopping configurations [START_REF] Castellan | Strategies as concurrent processes[END_REF]. By distinguishing certain configurations as stopping we keep track of those visible configurations at which the strategy may appear to get stuck through the occurrence of hidden neutral moves.

Stopping configurations are the event-structure analogue of Russ Harmer and Guy McCusker's "divergences" [START_REF] Harmer | A fully abstract game semantics for finite nondeterminism[END_REF], though event structures add the refinement of locality and independence to the concept. In an interleaving model, in which behaviour is captured through sequences of actions, divergence anywhere has a global effect; generally, in the parallel composition of two processes if one can perform an infinite sequence of actions, these may block progress of the other process, unless additional fairness assumptions are enforced. This is not so in a model such as event structures where the independence/concurrency of actions is explicit. In a nondeterministic strategy a Player move is not blocked by the occurrence of moves with which it is independent. Whereas an interleaving model may require weak fairness assumptions these are generally built into the behaviour of strategies as event structures [START_REF] Winskel | Events in computation[END_REF]. This makes for subtle differences in the nature of 'must' testing in concurrent games w.r.t. traditional games.

Perhaps surprisingly, in many situations a concurrent strategy may be replaced by its simpler "rigid image" in the game, despite this often forgetting nondeterministic branching-rigid-image strategies form a category rather than just a bicategory [START_REF] Castellan | Distributed strategies made easy[END_REF]-and indeed this remains true for strategies with stopping configurations; none of the 'may' or 'must' behaviour is lost.

Our technical contribution concludes with characterisations of the 'may' and 'must' equivalences and preorders on strategies. The 'may' equivalence of strategies is captured through their inducing the same set of finite traces; a trace being understood as a sequence of moves in the game. This echoes the earlier results of Ghica and Murawski when showing their non-alternating games model is fully-abstract for Idealized Parallel Algol with respect to may-convergence [START_REF] Ghica | Angelic semantics of fine-grained concurrency[END_REF]. For 'must' equivalence, our result is to be compared with that of Harmer and McCusker for their sequential games model, based on Hyland-Ong games with explicit divergences [START_REF] Harmer | A fully abstract game semantics for finite nondeterminism[END_REF]. But whereas in a sequential setting only the first divergence matters, for us 'must' equivalence of strategies is equivalent to their sharing the same traces of all (possibly infinite) stopping configurations. See Example 7.2 and what follows for an in-depth discussion.

Because we restrict attention to linear bicategories of strategies, the tests here are linear too; they do not permit the tested strategy to be copied and rerun. From the point of view of distributed computation linearity is natural: it is often infeasible to copy a distributed system or strategy [START_REF] Winskel | Linearity and nonlinearity in distributed computation[END_REF]. Then single-run 'may' and 'must' tests are appropriate.

On the other hand, most programming languages do allow some form of copying and nonlinearity. Through the addition of symmetry we can adjoin pseudo (co)monads-where the traditional laws hold up to symmetry, and model nonlinear features [START_REF] Castellan | Symmetry in concurrent games[END_REF][START_REF] Castellan | Thin games with symmetry and concurrent hyland-ong games[END_REF]. Through symmetry and pseudo comonads, we can realise a variety of nonlinear forms of testing, in which a test could dynamically copy and retest the strategy of interest. The nature of such broader testing on strategies, the equivalences and logics induced, are not well understood and deserve a systematic study, for which this paper forms a foundation. As shown by Samson Abramsky such broader tests are needed to realise equivalences such as bisimulation as testing equivalences [START_REF] Abramsky | Observation equivalence as a testing equivalence[END_REF].

Event structures

An event structure comprises (E, ≤, Con), consisting of a set E of events which are partially ordered by ≤, the causal dependency relation, and a nonempty consistency relation Con consisting of finite subsets of E. The relation e ′ ≤ e expresses that event e causally depends on the previous occurrence of event e ′ . That a finite subset of events is consistent conveys that its events can occur together by some stage in the evolution of the process. Together the relations satisfy several axioms. We insist that the partial order is finitary, i.e.

• [e] = def {e ′ e ′ ≤ e} is finite for all e ∈ E , and that consistency satisfies

• {e} ∈ Con for all e ∈ E ,
• Y ⊆ X ∈ Con implies Y ∈ Con, and

• X ∈ Con & e ≤ e ′ ∈ X implies X ∪ {e} ∈ Con .
There is an accompanying notion of state, or history, those events that may occur up to some stage in the behaviour of the process described. A configuration is a, possibly infinite, set of events x ⊆ E which is:

• consistent, X ⊆ x and X is finite implies X ∈ Con ; and

• down-closed, e ′ ≤ e ∈ x implies e ′ ∈ x .
Two events e, e ′ are called concurrent if the set {e, e ′ } is in Con and neither event is causally dependent on the other; then we write e co e ′ . In games the relation of immediate dependency e e ′ , meaning e and e ′ are distinct with e ≤ e ′ and no event in between, plays a very important role. We write [X] for the down-closure of a subset of events X. Write C ∞ (E) for the configurations of E and C(E) for its finite configurations. (Sometimes we shall need to distinguish the precise event structure to which a relation is associated and write, for instance, ≤ E , E or co E .) Example 2.1. In examples it is often convenient to draw event structures. Often, though not always, consistency is determined in a binary fashion, in that a set of events is consistent if all of its pairs are. Then, it is economical to draw the binary relation of conflict, or inconsistency. For example, in the diagram

❴ L L R ❴ L L R Z Z e ❅ ❅ ❅ ❅ ❅ ❅ ❴ L L R / o / o
f ∶ E → E ′ is a partial function on events f ∶ E ⇀ E ′ such that for all x ∈ C ∞ (E) its direct image f x ∈ C ∞ (E ′ )
and if e 1 , e 2 ∈ x and f (e 1 ) = f (e 2 ) (with both defined), then e 1 = e 2 .

(Those maps defined is unaffected if we replace possibly infinite configurations C ∞ (E) by finite configurations C(E) above; this is because any configuration is the union of finite configurations and direct image preserves such unions.)

Maps of event structures compose as partial functions, with identity maps given by identity functions. Say a map is total if the function f is total. Notice that for a total map f the condition on maps now says it is locally injective, in the sense that w.r.t. any configuration x of the domain the restriction of f to a function from x is injective; the restriction of f to a function from x to f x is thus bijective. Say a total map of event structures is rigid when it preserves causal dependency.

Although a map f ∶ E → E ′ of event structures does not generally preserve causal dependency, it does locally reflect causal dependency: whenever e, e ′ ∈ x, a configuration of E, and f (e) and f (e ′ ) are both defined with f (e ′ ) ≤ f (e), then e ′ ≤ e. Consequently, f preserves the concurrency relation: if e co e ′ in E and f (e) and f (e ′ ) are both defined then f (e) co f (e ′ ).

Constructions

We provide the constructions which we use in the paper.

Partial-total factorisation

We shall realise an operation of hiding events via a factorisation property of maps of event structures.

Let (E, ≤, Con) be an event structure. Let V ⊆ E be a subset of 'visible' events. Define

E↓V = def (V, ≤ V , Con V ), where v ≤ V v ′ iff v ≤ v ′ & v, v ′ ∈ V and X ∈ Con V iff X ∈ Con & X ⊆ V . The operation projects E to visible events V . Consider a partial map of event structures f ∶ E → E ′ . Let V = def {e ∈ E f (e) is defined} .
Then f clearly factors into the composition

E f0 / / E↓V f1 / / E ′
of f 0 , a partial map of event structures taking e ∈ E to itself if e ∈ V and undefined otherwise, and f 1 , a total map of event structures acting like f on V . We call f 1 the defined part of the partial map f . We say a map f ∶ E → E ′ is a projection if its defined part is an isomorphism.

The partial-total factorisation is characterised to within isomorphism by the following universal property: for any factorisation

f ∶ E g0 / / E 1 g1 / / E ′
where g 0 is partial and g 1 is total there is a (necessarily total) unique map h ∶ E↓V → E 1 such that

E f0 / / g0 ! ! ❈ ❈ ❈ ❈ ❈ ❈ ❈ ❈ E↓V h ✤ ✤ ✤ f1 / / E ′ E 1 g1 = = ③ ③ ③ ③ ③ ③ ③ ③ commutes.

Pullback

Event structures and their maps have pullbacks. For the composition of strategies we shall only need pullbacks of total maps. Consider a pullback

P π1 ⑦ ⑦ ⑦ ⑦ ⑦ ⑦ ⑦ ⑦ ❄ ⑧ π2 ❅ ❅ ❅ ❅ ❅ ❅ ❅ ❅ A f ❅ ❅ ❅ ❅ ❅ ❅ ❅ B g ⑦ ⑦ ⑦ ⑦ ⑦ ⑦ ⑦ ⑦ C
where f and g are total. Pullbacks are difficult to construct directly on the "prime" event structures we are using here, essentially because they associate each event with a unique minimum causal history. Such constructs are best first carried out in a broader model. Here we build the pullback of event structures out of the stable family of secured bijections. Definition 3.1. A secured bijection comprises a composite bijection

θ x,y ∶ x ≅ f x = gy ≅ y between configurations x ∈ C ∞ (A) and y ∈ C ∞ (B) s.t. f x =
gy, which is secured in the sense that the transitive relation generated on θ x,y by taking

(a, b) ≤ (a ′ , b ′ ) if a ≤ A a ′ or b ≤ B b ′
is a finitary partial order. Let B be the family of secured bijections. Say a subset

Z ⊆ B is compatible iff ∃θ ′ ∈ B∀θ ∈ Z. θ ⊆ θ ′ .
Proposition 3.2. The family B is a stable family, 1i.e. it is

• Complete: ∀Z ⊆ B. Z is compatible ⇒ ⋃ Z ∈ B ; • Stable: ∀Z ⊆ B. Z = ∅ & Z is compatible ⇒ ⋂ Z ∈ B; • Finitary: ∀θ ∈ B, (a, b) ∈ θ∃θ 0 ∈ B. θ 0 is finite & (a, b) ∈ θ 0 ⊆ θ; and • Coincidence-free: For all θ ∈ B, (a, b), (a ′ , b ′ ) ∈ θ with (a, b) = (a ′ , b ′ ), ∃θ 0 ∈ B. θ 0 ⊆ θ & ((a, b) ∈ θ 0 ⇐⇒ (a ′ , b ′ ) ∉ θ 0 ) .
We now apply a general construction Pr(B) for obtaining an event structure from the stable family B. Suppose (a, b) ∈ θ where θ ∈ B [START_REF] Winskel | Event structure semantics for CCS and related languages[END_REF][START_REF] Winskel | Event structures[END_REF]. Because B is a stable family

[(a, b)] θ = def ⋂ {φ ∈ B φ ⊆ θ & (a, b) ∈ φ} ∈ B
and moreover is a finite set; it represents a minimal way in which (a, b) can occur. We build the pullback of event structures taking such minimal elements as events. Proposition 3.3. Defining Pr(B) = (P, Con, ≤) where:

P = {[(a, b)] θ (a, b) ∈ θ & θ ∈ B} , Z ∈ Con iff Z ⊆ P & ⋃ Z ∈ B and p ≤ p ′ iff p, p ′ ∈ P & p ⊆ p ′
yields an event structure. There is an order isomorphism

β ∶ (C(Pr(B)), ⊆) ≅ (B, ⊆)
where β(y) = ⋃ y for y ∈ C(Pr(B)); its mutual inverse is γ where γ

(θ) = {[(a, b)] θ (a, b) ∈ θ} for θ ∈ B.
There are obvious maps π 1 ∶ Pr(B) → A and π 2 ∶ Pr(B) → B given by

π 1 ([(a, b)] θ ) = a and π 2 ([(a, b)] θ ) = b.
These make the required pullback Pr(B), π 1 , π 2 of event structures. Why? The family B is a pullback in the category of stable families (its maps are similar to those of event structures). There is a coreflection from the category of event structures to that of stable families. Its right adjoint is Pr which consequently preserves pullbacks, yielding the pullback of event structures when applied to B [START_REF] Winskel | Event structure semantics for CCS and related languages[END_REF][START_REF] Winskel | Event Structures, Stable Families and Concurrent Games[END_REF]. Definition 3.4. We shall write x∧y for the configuration γ(θ x,y ) of Pr(B) which correponds to a secured bijection θ

x,y ∶ x ≅ f x = gy ≅ y between x ∈ C ∞ (A) and y ∈ C ∞ (B). Note that any configuration of the pullback is of the form x ∧ y for unique x ∈ C ∞ (A) and y ∈ C ∞ (B). Of course, given x ∈ C ∞ (A) and y ∈ C ∞ (B)
we cannot be assured that they form a secured bijection even when f x = gy. We shall treat ∧ as a partial operation with x ∧ y only defined when x ∈ C ∞ (A) and y ∈ C ∞ (B) form a secured bijection.

Rigid image

This section is only used late on in the paper when showing how 'may' and 'must' behaviour transfer to the rigid image of a strategy-Section 11.

There is an adjunction between E r , the category of event structures with rigid maps, to E t , the category of event structures with total maps. Its right adjoint's action on an event structure B is given as follows. For x ∈ C ∞ (B), an augmentation of x is a finitary partial order

(x, α) where ∀b, b ′ ∈ x. b ≤ B b ′ ⇒ b α b ′ .
We can regard such augmentations as elementary event structures in which all subsets of events are consistent. Order all augmentations by taking

(x, α) ↪ (x ′ , α ′ ) iff x ⊆ x ′ and the inclusion i ∶ x ↪ x ′ is a rigid map i ∶ (x, α) → (x ′ , α ′ ).
Augmentations under ↪ form a prime algebraic domain [START_REF] Nielsen | Petri nets, event structures and domains[END_REF][START_REF] Winskel | Prime algebraicity[END_REF], so are isomorphic to the configurations of an event structure, aug(B); its events are the complete primes, which are precisely the augmentations with a top element. Proposition 4.1. [START_REF] Winskel | Event structures with symmetry[END_REF] The inclusion functor E r ↪ E t has a right adjoint aug.

The category E t is isomorphic to the Kleisli category of the monad induced on E r by the adjunction.

Rigid maps f ∶ A → B have a useful image given by restricting the causal dependency of B to the set of events f A, the direct image of the events of A, and taking a finite set of events to be consistent if they are the image of a consistent set in A. More generally, a total map f ∶ A → B has a rigid image given by the image of its corresponding Kleisli map, the rigid map f ∶ A → aug(B). Put more directly, a total map f ∶ A → B has a rigid image comprising a factorisation f = f 1 f 0 where f 0 is rigid epi and f 1 is a total map,

A f ❅ ❅ ❅ ❅ ❅ ❅ ❅ ❅ f0 / / / / B 0 f1 B ,
with the following universal property: for any factorisation of

f = f ′ 1 f ′ 0 where f ′ 0 is rigid epi, there is a unique map h such that the diagram A f0 $ $ $ $ f ❅ ❅ ❅ ❅ ❅ ❅ ❅ ❅ f ′ 0 / / / / B ′ 0 f ′ 1 h / / ❴ ❴ ❴ B 0 f1 5⑤ ⑤ ⑤ ⑤ ⑤ ⑤ ⑤ B
commutes; the map h is necessarily also rigid and epi.

From the universal property of rigid image we derive:

Proposition 4.2. Let f ∶ A → B and g ∶ B → C be maps of event structures.
Assume that f is rigid and epi. Then, g and g ○ f have the same rigid image.

Event structures with polarity

Both games and strategies will be represented by event structures with polarity.

An event structure with polarity comprises (A, pol ) where A is an event structure with a polarity function pol A ∶ A → {+, -, 0} ascribing a polarity + (Player), -(Opponent) or 0 (neutral) to its events. The events correspond to (occurrences of) moves. It will be technically useful to allow events of neutral polarity; they arise, for example, in the interaction between a strategy and a counterstrategy. We write A 0 for the event structure with polarity in which all the polarities are reassigned 0, so made neutral. A game shall be represented by an event structure with polarity in which no moves are neutral.

Notation 5.1. In an event structure with polarity (A, pol ), with configurations x and y, write x ⊆ -y to mean inclusion in which all the intervening events are moves of Opponent, i.e. pol (y ∖ x) ⊆ {-}. Similarly, x ⊆ 0 y signifies an inclusion in which all the intervening moves are neutral. However, we shall write x ⊆ + y for inclusion in which the intervening events are either neutral or moves of Player.

(The latter choice reflects the fact that neutral moves in a strategy behave as internal moves of Player.) We say a configuration

x ∈ C ∞ (A) is +-maximal iff x is maximal in C ∞ (A) w.r.t. ⊆ + , i.e.
the only way that x extends to a larger configuration is through the occurrence of Opponent moves.

Operations on games

We introduce two fundamental operations on games.

Dual

The dual, A ⊥ , of a game A, comprises the same underlying event structure as A but with a reversal of polarities. As mentioned in the introduction, we shall implicitly adopt the view of Player and understand a strategy in a game A as strategy for Player. A counterstrategy in a game A is a strategy for Opponent in the game A, i.e. a strategy (for Player) in the game A ⊥ .

Simple parallel composition

This operation simply juxtaposes two games, and more generally two event structures with polarity. Let (A, ≤ A , Con A , pol A ) and (B, ≤ B , Con B , pol B ) be event structures with polarity. The events of A∥B are ({1} × A) ∪ ({2} × B), their polarities unchanged, with the only relations of causal dependency given by

(1, a) ≤ (1, a ′ ) iff a ≤ A a ′ and (2, b) ≤ (2, b ′ ) iff b ≤ B b ′ ;
a finite set X of events is consistent in A∥B iff its components X A in A and and X B in B are individually consistent. The unit w.r.t. simple composition is the empty event structure with polarity, written ∅. We shall adopt the same operation for configurations of a game A∥B, regarding a configuration x of the parallel composition as x A ∥x B . If we are not a little careful we can run into distracting technical issues through (A∥B)∥C not being strictly the same as A∥(B∥C). For our purposes it will suffice to adopt the convention that when we write e.g. A∥B∥C the simple parallel composition of three event structures with polarity we shall mean the event structure with events

{1} × A ∪ {2} × B ∪ {3} × C ,
with causal dependency and consistency copied from those of A, B and C. As in the binary case, we adopt the same notation for configurations and can describe a typical configuration x of A∥B∥C as x A ∥x B ∥x C .

Strategies between games

A strategy from a game A to a game B is a strategy in the compound game A ⊥ ∥B. Of course we shall have to define what it means to be a strategy in a game. Given another strategy τ from the game B to a game C, informally we obtain their composition τ ⊙σ from A to C by playing the two strategies off against each other in the common game B and hiding the resulting interaction.

The composition of strategies can introduce hidden deadlocks, conflicts and divergences which affect its observable behaviour: If we are to distinguish the two compositions of the example, we need to take some account of their internal moves of interaction.

Strategies with neutral moves

Thus motivated, we study bare strategies with neutral moves, in which we can see the events of interaction not visible in the game. Recall we assume that in games all events have +ve or -ve polarity. Definition 6.1. A bare strategy from a game A to a game B comprises a total map σ ∶ S → A ⊥ ∥N ∥B of event structures with polarity (in which S may also have neutral events) where (i) N is an event structure consisting solely of neutral events;

(ii) σ is receptive, ∀x ∈ C(S), y ∈ C(A ⊥ ∥N ∥B). σx ⊆ -y ⇒ ∃!x ′ ∈ C(S). x ⊆ x ′ & σx ′ = y ;
(iii) σ is innocent in that it is both +-innocent and --innocent:

+-innocent: if s s ′ & pol (s) = + then σ(s) σ(s ′ ) ; --innocent: if s s ′ & pol (s ′ ) = -then σ(s) σ(s ′ ) .
Note that s ′ in +-innocence and s in --innocence may be neutral events. 2 A strategy from a game A to a game B comprises a total map σ ∶ S → A ⊥ ∥B of event structures with polarity for which the composite σ ∶ S → A ⊥ ∥B ≅ A ⊥ ∥∅∥B is a bare strategy [START_REF] Rideau | Concurrent strategies[END_REF].

We shall often identify strategies with bare strategies with no neutral events, and (bare) strategies in a game with (bare) strategies from the empty game ∅.

Consider two bare strategies σ ∶ S → A ⊥ ∥N ∥B and σ ′ ∶ S ′ → A ⊥ ∥N ∥B. A map between them, a 2-cell f ∶ σ ⇒ σ ′ , comprises a map f ∶ S → S ′ of event structures with polarity such that S σ f / / S ′ σ ′ z z ✈ ✈ ✈ ✈ ✈ ✈ ✈ ✈ ✈ A ⊥ ∥N ∥B commutes.
In this way bare strategies in A ⊥ ∥N ∥B form a category,

BStrat(A, N, B) .
We obtain the category Strat(A, B) of strategies from A to B from the special case when N = ∅.

Strategies from bare strategies

We obtain a strategy as the visible part of a bare strategy when we hide neutral events via a projection p: Proposition 6.2. Let σ ∶ S → A ⊥ ∥N ∥B be a bare strategy-so satisfying properties (i), (ii) and (iii) of Definition 6.1. Then, σ satisfies an additional property:

(iv) in the partial-total factorisation of the composition of σ with the projection

A ⊥ ∥N ∥B → A ⊥ ∥B, S σ p / / S ↓ σ↓ A ⊥ ∥N ∥B / / A ⊥ ∥B
the defined part σ ↓ is a strategy, which we call the visible part of σ.

2 This definition of linear innocence, which applies in the presence of neutral events, appears in the work of Claudia Faggian and Mauro Piccolo [START_REF] Faggian | Partial orders, event structures and linear strategies[END_REF]. It is not to be confused with the innocence of Martin Hyland and Luke Ong, to which it only relates indirectly; to disambiguate the two notions "courtesy" has been used for that here. An extension of Hyland-Ong innocence to concurrent games is given in [START_REF] Castellan | The parallel intensionally fully abstract games model of PCF[END_REF]. Bare strategies have also been called "partial" strategies [START_REF] Castellan | Strategies as concurrent processes[END_REF] and "uncovered" strategies [START_REF] Castellan | Non-angelic concurrent game semantics[END_REF].

(Conversely, (iv) together with receptivity and no incidence of a +ve event immediately preceding a neutral event in S, suffice to establish that σ is a bare strategy.)

With the notation of the lemma above, write

x ↓ = def px ∈ C ∞ (S ↓ )
for the visible image of a configuration x ∈ C ∞ (S). The hiding operation on strategies extends to a functor

( ) ↓ ∶ BStrat(A, N, B) → Strat(A, B) ; a 2-cell f ∶ σ ⇒ σ ′ between bare strategies restricts to a 2-cell f ↓ ∶ σ ↓ ⇒ σ ′ ↓
between their visible parts. It acts so

f ↓ x ↓ = (f x) ↓ for all x ∈ C ∞ (S).

Composition

We can compose two bare strategies σ ∶ S → A ⊥ ∥M ∥B and τ ∶ T → B ⊥ ∥N ∥C by pullback. Ignoring polarities temporarily, and padding with identity maps, we obtain τ ⊛ σ via the pullback

T ⊛ S w w ♥ ♥ ♥ ♥ ♥ ♥ ♥ ♥ ♥ ♥ ♥ ♥ ❄ ⑧ ' ' S∥N ∥C σ∥N ∥C ' ' ❖ ❖ ❖ ❖ ❖ ❖ ❖ ❖ ❖ ❖ ❖ A∥M ∥T A∥M∥τ w w ♦ ♦ ♦ ♦ ♦ ♦ ♦ ♦ ♦ ♦ ♦ ♦ A∥M ∥B∥N ∥C as the ensuing map τ ⊛ σ ∶ T ⊛ S → A ⊥ ∥(M ∥B 0 ∥N )∥C
once we reinstate polarities and make the events of B neutral.

As a pullback the configurations of T ⊛ S are built from configurations of S and T . Let x ∈ C ∞ (S) and y ∈ C ∞ (T ). Let σx = x A ⊥ ∥x 0 ∥x B and τ y = y B ⊥ ∥y 0 ∥y C . Define y ⊛ x = def (x∥y 0 ∥y C ) ∧ (x A ⊥ ∥x 0 ∥y) which will be defined and a configuration in C ∞ (T ⊛ S) if x B = y B ⊥ and the corresponding bijection secured. The following property, useful later, is a consequence of the receptivity of σ and τ .

Lemma 6.3. A configuration y ⊛ x ∈ C ∞ (T ⊛ S) is +-maximal in C ∞ (T ⊛ S) iff x is +-maximal in C ∞ (S) and y is +-maximal in C ∞ (T ).
Given a 2-cell f ∶ σ ⇒ σ ′ between bare strategies in A ⊥ ∥N ∥B and g ∶ τ ⇒ τ ′ between bare strategies in B ⊥ ∥M ∥C, from the universality of pullback we obtain the 2-cell

g ⊛ f ∶ τ ⊛ σ ⇒ τ ′ ⊛ σ ′
between the two compositions in A ⊥ ∥(N ∥B 0 ∥M )∥C. It acts so

(g ⊛ f )(y ⊛ x) = (gy) ⊛ (f x)
on a typical configuration y ⊛ x. This extends composition of bare strategies to a functor

⊛ ∶ BStrat(B, N, C) × BStrat(A, M, B) → BStrat(A, M ∥B 0 ∥N, C) .
Composition of bare strategies restricts to a functor between rigid 2-cells.

We obtain the composition of strategies as the composite functor

⊙ ∶ Strat(B, C) × Strat(A, B) ≅ BStrat(B, ∅, C) × BStrat(A, ∅, B) ⊛ →BStrat(A, ∅∥B 0 ∥∅, C) ( ) ↓ →Strat(A, C) .
Though we generally elide the isomorphisms regarding strategies as bare strategies without neutral events, and write

τ ⊙σ = def (τ ⊛ σ) ↓
for the composition of strategies σ ∈ Strat(A, B) and τ ∈ Strat(B, C). Describing the strategies σ ∶ S → A ⊥ ∥B and τ ∶ T → B ⊥ ∥C as having composition

τ ⊙σ ∶ T ⊙S → A ⊥ ∥C ,
we can present a typical configuration of T ⊙S as

y⊙x = def (y ⊛ x) ↓ for x ∈ C ∞ (S) and y ∈ C ∞ (T ).
Composition is preserved in extracting the visible part from bare strategies:

Lemma 6.4. Let σ ∶ S → A ⊥ ∥M ∥B and τ ∶ T → B ⊥ ∥N ∥C be bare strategies. Then, (τ ⊛ σ) ↓ = τ ↓ ⊙σ ↓ . For x ∈ C ∞ (S) and y ∈ C ∞ (T ), (y ⊛ x) ↓ = y ↓ ⊙x ↓ ,
with one side defined if the other is.

The copycat strategy

The copycat strategy is the identity for composition of strategies. We present its construction and key property from [START_REF] Rideau | Concurrent strategies[END_REF].

Lemma 6.5. Let A be an event structure with polarity. There is an event structure with polarity C C A having the same events and polarity as A ⊥ ∥A but with causal dependency ≤ C C A given as the transitive closure of the relation The copycat strategy for A is the map cc A ∶ C C A → A ⊥ ∥A which acts as identity on events. We have σ ≅ σ⊙ cc A ≅ cc B ⊙σ, for any strategy σ ∈ Strat(A, B).

≤ A ⊥ ∥A ∪ {(c, c) c ∈ A ⊥ ∥A & pol A ⊥ ∥A (c) = +}
The axioms on strategies are precisely those needed to ensure that copycat behaves as identity w.r.t. composition ⊙ and thus obtain a bicategory Strat of games and strategies [START_REF] Rideau | Concurrent strategies[END_REF]. Of course copycat is not the identity for the composition of bare strategies; that composition will generally have extra neutral events introduced through interactions.

'May' and 'must' tests

Consider the following three bare strategies in the game A comprising a single Player move ⊞. Neutral events are drawn as .

S 1 σ1 ⊞ ❴ ∥A ⊞ S 2 σ2 ❴ ✤ , , 2 ⊞ ❴ ∥A ⊞ O O O S 3 σ3 ✤ , , 2 ❴ ⊞ ❴ ∥A
⊞ From the point of view of observing the move over the game A the first two bare strategies, σ 1 and σ 2 , differ from the the third, σ 3 . In a maximal play both σ 1 and σ 2 must result in the observation of the single move of A. However, in σ 3 one maximal play is that in which the topmost neutral event of S 3 has occurred, in conflict with the only way of observing the single move of A.

We follow Hennessy and de Nicola in making these ideas precise [START_REF] De Nicola | Testing equivalences for processes[END_REF]. Say σ may pass τ iff there exists y ⊛ x ∈ C ∞ (T ⊛ S), where x ∈ C ∞ (S) and y ∈ C ∞ (T ), with the image τ y containing ✓. (Note that we may w.l.o.g. assume that the configuration y ⊛ x is finite.) Say σ must pass τ iff for all y⊛x ∈ C ∞ (T ⊛S), where x ∈ C ∞ (S) and y ∈ C ∞ (T ) are ⊆ + -maximal, the image τ y contains ✓.

Say two bare strategies are 'may' (respectively, 'must') equivalent iff the tests they may (respectively, must) pass are the same.

The definitions extend in the obvious fashion to bare strategies of type A ⊥ ∥N ∥B.

A bare strategy is 'may' equivalent, but need not be 'must' equivalent, to the strategy which is its defined part; 'must' inequivalence is lost in moving from bare strategies to strategies.

Example 7.2. As an illustration of the subtle nature of testing for 'must' equivalence, consider the following bare strategies in the game A, as drawn:

a b c d e ⊞ ✤ , , 2 ⊟ ✤ , , 2 ⊞ ✤ , , 2 ⊟ ✤ , , 2 ⊞
The game A consists of five events with the polarity and causal dependency shown. One bare strategy σ 1 is

⊞ ✤ , , 2 ⊟ ✤ , , 2 ⊞ O O ✤ , , 2 ⊟ ✤ , , 2 ⊞
, with one neutral event, while the other σ 2 is

⊞ ✤ , , 2 ⊟ ✤ , , 2 ⊞ O O ✤ , , 2 ⊟ ✤ , , 2 ⊞ O O
, with two neutral events. Through the possible occurrence of neutral events the bare strategy σ 1 has a +-maximal configuration with just events {a, b} visible from the game, while σ 2 has in addition a +-maximal configuration comprising visible moves {a, b, c, d}. The following test strategy distinguishes σ 1 and in that σ 1 must pass the test while σ 2 need not. (The test is a strategy in A ⊥ ∥⊞✓; thus the change in polarity of moves in A.) Composed with the test, σ 1 may fail to perform the leftmost ⊞✓ but if so must then perform the rightmost ⊞✓; whereas σ 2 may fail to perform both. ◻

σ 2 ⊟ ✤ , , 2 ❴ ⊞ ✤ , , 2 ⊟ ✤ , , 2 ⊞ ✤ , , 2
This example might be puzzling to readers familiar with Harmer and Mc-Cusker's fully abstract model for (sequential) finite non-determinism [START_REF] Harmer | A fully abstract game semantics for finite nondeterminism[END_REF], in particular regarding their handling of 'must' equivalence through the addition of divergences. Indeed, there, if a trace has already potentially triggered a divergence, then any execution going past that divergence has already lost all hope for 'must' convergence. Accordingly, in [START_REF] Harmer | A fully abstract game semantics for finite nondeterminism[END_REF], only the first divergence mattersfurther divergences are not recorded.

In contrast, Example 7.2 indicates how in concurrent strategies, all divergences matter. This is not an artificiality of concurrent strategies, but something inherent to the observational power of the tests they support: here the distinguishing manage to observe beyond the first divergence by running two threads in parallel. The first thread aims to directly register success; by +maximality it will be run eventually if the observed strategy triggers the first divergence. The second thread follows the execution of the program, then immediately cancels the first thread if the program goes past the divergence; and then proceeds to test for the second divergence.

Strategies with stopping configurations

Bare strategies lack identities w.r.t. composition, so they do not form a bicategory. Fortunately, for 'may' and 'must' equivalence it is not necessary to use bare strategies; for 'may' equivalence strategies suffice; whereas for 'must' equivalence it is sufficient to carry with a strategy the extra structure of stopping configurations-to be thought of as images of +-maximal configurations in an underlying bare strategy. As we shall see, composition and copycat extend to composition and copycat on strategies with stopping configurations, while maintaining a bicategory. We tackle the simpler case in which games are assumed to be race-free. (The extension to games which are not race-free is outlined in [START_REF] Castellan | Strategies as concurrent processes[END_REF].) We recall when an event structure with polarity is race-free and the allied notion of deterministic strategy: Definition 8.1. Say A, an event structure with polarity, is race-free iff whenever x ⊆ + y and x ⊆ -z for configurations x, y, z of A then y ∪z is also a configuration.

Say S, an event structure with polarity, is deterministic iff whenever x ⊆ + y and x ⊆ z for configurations x, y, z of S then y ∪ z is also a configuration. Say a bare strategy σ ∶ S → A ⊥ ∥N ∥B is deterministic iff S is deterministic; with a strategy being deterministic iff it is so as a bare strategy. Lemma 8.2. [START_REF] Rideau | Concurrent strategies[END_REF][START_REF] Winskel | Deterministic concurrent strategies[END_REF] Let A be a game. The copycat strategy cc A is deterministic iff the game A is race-free.

Let σ ∶ S → A ⊥ ∥N ∥B be a bare strategy between race-free games A and B.

Recall its associated partial-total factorisation

S σ p / / S ↓ σ↓ A ⊥ ∥N ∥B / / A ⊥ ∥B
where p is a projection sending configurations x of S to configurations x ↓ of S ↓ . The visible part of σ is a strategy σ ↓ . Define the stopping configurations in

C ∞ (S ↓ ) to be Stop(σ) = def {x ↓ x ∈ C ∞ (S) is +-maximal} .
So, in other the stopping configurations are the visible images of configurations which are maximal w.r.t. neutral or Player moves. Note that Stop(σ) will include all the +-maximal configurations of S ↓ : any +-maximal configuration y of S ↓ is the image under p of its down-closure [y] in S, and by Zorn's lemma this extends (necessarily by neutral events) to a maximal configuration x of S with image y under p; the configuration x is +-maximal by the +maximality of y. If σ is deterministic, then Stop(σ) consists of precisely the +-maximal configurations of S ↓ . If σ is a strategy, i.e. it has no neutral events, then Stop(σ) is just the set consisting of all +-maximal configurations of S.

Definition 8.3. A stopping strategy in a game A comprises (σ, M S ), a strategy σ ∶ S → A together with a subset M S ⊆ C ∞ (S) called stopping configurations. As usual, a stopping strategy from a game A to game B is a stopping strategy in the game A ⊥ ∥B. We let St ∶ σ ↦ (σ ↓ , Stop(σ)) denote the operation motivated above from bare strategies σ to stopping strategies.

Remark. There is the issue of what axioms to adopt on stopping configurations. We do not insist that stopping configurations include all +-maximal configurations as this property will not be preserved in taking the rigid image of a stopping strategy-Example 11.3.

Given two stopping strategies σ ∶ S → A ⊥ ∥B, M S and τ ∶ T → B ⊥ ∥C, M T we define their interaction,

(τ, M T ) ⊛ (σ, M S ) = def (τ ⊛ σ, M T ⊛ M S ) ,
with the stopping configurations of the interaction T ⊛ S as

M T ⊛ M S = {y ⊛ x x ∈ M S & y ∈ M T }
-sensible because of Lemma 6.3. Define their composition by

(τ, M T )⊙(σ, M S ) = def (τ ⊙σ, M T ⊙M S ) ,
where the stopping configurations of T ⊙S form the set

M T ⊙M S = {y⊙x x ∈ M S & y ∈ M T } .
To make stopping strategies into a bicategory we must settle on an appropriate notion of 2-cell. The following choice of definition is useful for 'must' equivalence-see Lemma 9.5. Definition 8.4. A 2-cell f ∶ (σ, M S ) ⇒ (σ ′ , M S ′ ) between stopping strategies is a 2-cell of strategies f ∶ σ ⇒ σ ′ such that f M S ⊆ M S ′ . We write SStrat(A, B) for the category stopping strategies from game A to game B; its maps are 2-cells.

Composition extends to 2-cells between stopping strategies: their composition as 2-cells between strategies is easily shown to preserve stopping configurations.

Proposition 8.5. For games A, B and C composition of stopping strategies is a functor

⊙ ∶ SStrat(B, C) × SStrat(A, B) → SStrat(A, C) .
We should also extend copycat cc A ∶ C C A → A ⊥ ∥A to a stopping strategy. Because we are assuming A is race-free, we do this by taking

M C C A = def {(x∥x) ∈ C ∞ (C C A ) x ∈ C ∞ (A)} . Because A is race-free, M C C A comprises all the +-maximal configurations of C C A . Then, ( cc A , M C C A ) is an identity w.r.t. the extended composition.
With the operations and constructions above, stopping strategies inherit the structure of a bicategory SStrat from strategies; the objects are restricted to race-free games in order to have the above simple form of stopping configurations for copycat.

Bare strategies and stopping strategies

We turn to relations between bare strategies and stopping strategies. We have seen that there is a functor ( ) ↓ ∶ BStrat(A, N, B) → Strat(A, B) from bare strategies to their visible part. However, it is not the case that St is a functor from bare strategies BStrat(A, N, B) to stopping strategies SStrat(A, B). Given an arbitrary 2-cell f ∶ σ ⇒ σ ′ between bare strategies f ↓ can fail to preserve stopping configurations. However:

Proposition 8.7. Let σ ∶ S → A ⊥ ∥N ∥B and σ ′ ∶ S ′ → A ⊥ ∥N ∥B be bare strate- gies. Say a 2-cell f ∶ σ ⇒ σ ′ is +-reflecting iff, for x ∈ C(S), y ∈ C(S ′ ), f x ⊆ + y ⇒ ∃x ′ ∈ C(S). x ⊆ x ′ & f x ′ = y .
Let BStrat + (A, N, B) be the subcategory where 2-cells are +-reflecting. Then

St ∶ BStrat + (A, N, B) → SStrat(A, B) taking f ∶ σ ⇒ σ ′ to f ↓ ∶ St(σ) ⇒ St(σ ′ ) is a functor.

'May' and 'Must' testing

We can rephrase 'may' and 'must' testing in terms of stopping strategies. Definition 9.1. Let (σ, M S ) be a stopping strategy in a game A. Let τ ∶ T → A ⊥ ∥N ∥⊞ be a 'test' bare strategy from A to a the game consisting of a single Player move ⊞. Write St(τ ) as (τ 0 , M 0 ) where τ 0 ∶ T 0 → A∥⊞ is the visible part of τ and M 0 are its stopping configurations, obtained as images of the +-maximal configurations of T . Write ✓ = def (2, ⊞).

Say (σ, M S ) may pass τ iff there exists y ⊛ x ∈ C ∞ (T 0 ⊛ S), where x ∈ C ∞ (S) and y ∈ C ∞ (T 0 ), with the image τ 0 y containing ✓. (Note again, we may w.l.o.g. assume that the configurations x and y are finite.) Say (σ, M S ) must pass τ iff for all y ⊛ x ∈ M 0 ⊛ M S , where x ∈ C ∞ (S) and y ∈ C ∞ (T 0 ), the image τ 0 y contains ✓.

Say two stopping strategies are 'may', respectively 'must', equivalent iff the tests they may, respectively must, pass are the same. Proposition 9.2. With the notation above, (σ, M S ) may pass τ iff there exists y⊙x ∈ C ∞ (T 0 ⊙S), where x ∈ C ∞ (S) and y ∈ C ∞ (T 0 ), with the image τ 0 y containing ✓ -the configurations x, y may be assumed finite; and

(σ, M S ) must pass τ iff for all y⊙x ∈ M 0 ⊙M S , where x ∈ M S and y ∈ M 0 , the image τ 0 y contains ✓. Proof. Directly from the definitions, for the 'if' of the 'must' case, using Lemma 6.3.

Example 9.4. It is tempting to think of neutral events as behaving like the internal "tau" events of CCS [START_REF] Milner | A Calculus of Communicating Systems[END_REF]. However, in the context of concurrent strategies, because of their asynchronous nature, they behave rather differently. Consider three bare strategies, over a game comprising of just two concurrent +ve events, say a and b. The bare strategies have the following event structures in which we have named events by the moves they correspond to in the game:

S 1 a O b S 2 O ✤ , , 2 a ✤ , , 2 b S 3 O ✤ , , 2 a
b No pair would be weakly bisimilar due to the presence of pre-emptive internal events [START_REF] Milner | A Calculus of Communicating Systems[END_REF]. However, all three become isomorphic under St so are 'may' and 'must' equivalent to each other. ◻ 2-cells between stopping strategies respect 'may' and 'must' behaviour in the sense of the following lemma. Lemma 9.5. Let f ∶ (σ, M S ) ⇒ (σ ′ , M S ′ ) be a 2-cell between stopping strategies. Then for any test τ , (σ, M S ) may pass τ implies (σ ′ , M S ′ ) may pass τ ; and (σ ′ , M S ′ ) must pass τ implies (σ, M S ) must pass τ . Moreover, if f is a rigid epi and f M S = M S ′ , then (σ, M S ) and (σ ′ , M S ′ ) are both 'may' and 'must' equivalent.

Proof. In this proof, we shall identify a test with its image (τ, M T ) under St, as a strategy τ ∶ T → A ⊥ ∥⊞ with stopping configurations M T .

Let f ∶ (σ, M S ) ⇒ (σ ′ , M S ′ ) be a 2-cell. Assume σ ∶ S → A and σ ′ ∶ S ′ → A. Suppose (σ, M S ) may pass (τ, M T ). Then there is a (finite) configuration which we write y ⊛ x of T ⊛ S, built as a secured bijection out of y ∈ C(T ) and x ∈ C(S), whose image in the game contains ✓. The secured bijection built out of y and x induces a secured bijection built out of y and f x; this is because f x has no more causal dependency than x with which it is in bijection. This determines a configuration y ⊛ f x, with image containing ✓.

Suppose (σ ′ , M S ′ ) must pass (τ, M T ). Any y ⊛ x ∈ M T ⊛ M S images under τ ⊛ f to y ⊛ f x ∈ M T ⊛ M S ′ . As (σ ′ , M S ′ ) must pass τ , the configuration y ⊛ f x has image containing ✓, ensuring that y ⊛ x does too.
Finally suppose that f is rigid epi and f M S = M S ′ . We have just shown that f preserves the passing of 'may' tests and reflects the passing of 'must' tests. Because f is rigid epi it also reflects the passing of 'may' tests. Because f is rigid and f M S = M S ′ it preserves the passing of 'must' tests: any secured bijection y ⊛ f x in M T ⊛ M S ′ ensures by the rigidity of f a secured bijection y ⊛ x in M T ⊛ M S ; as (σ, M S ) must pass τ we have the image in the game of y ⊛ x contains ✓ ensuring the image of y ⊛ f x does too.

Tests based on bare strategies are more discriminating than tests based on (pure) strategies: Example 9.6. Let a game comprise a single Player move. Consider two stopping strategies: σ 1 , the empty strategy with the empty configuration ∅ as its single stopping configuration; σ 2 , the strategy performing the single Player move ⊞ with stopping configurations ∅ and {⊞}. (We can easily realise this stopping strategy via St from a bare strategy with event structure ⊞ / o .) By Lemma 9.5, we have (σ 2 , {∅, {⊞}}) must pass τ implies (σ 1 , {∅}) must pass τ , for any test τ . (The above would not hold if we had not included ∅ in the stopping configurations of σ 2 .)

Using the fact that we need only consider rigid images of tests-shown later in Section 11, a little argument by cases establishes the converse implication too, provided we restrict just to tests which are strategies. The stopping strategies would be must equivalent w.r.t. tests based just on strategies.

However with tests based on bare strategies we can distinguish them. Consider the test τ comprising three events, one of them neutral, with only nontrivial causal dependency ⊟ and in conflict with the 'tick' event ⊞. Then, it is not the case that (σ 2 , {∅, {⊞}}) must pass τ -the occurrence of the neutral event blocks success in a maximal execution-while (σ 1 , {∅}) must pass τ . Notice how the presence of the neutral event in the test turns the possibility that σ 2 can perform the Player move into a possibility of its failing the test. ◻ 10 'May' and 'Must' behaviour characterised 10.1 Preliminaries, traces of a strategy

Let S be an event structure. A possibly infinite sequence

s 1 , s 2 , ⋯, s n , ⋯
in S constitutes a serialisation of a configuration x ∈C ∞ (S) if x = {s 1 , s 2 , ⋯, s n , ⋯} and {s 1 , ⋯, s i } ∈ C(S) for all i at which the sequence is defined. We will often identify such a countable enumeration of a set with its associated total order. Note that in this way we can regard a serialisation as an elementary event structure in which causal dependency takes the form of a total order; a serialisation of a configuration is associated with a map to S whose image is the configuration. Let σ ∶ S → A be a strategy in a game

A. A trace in σ is a possibly infinite sequence α = (σ(s 1 ), σ(s 2 ), ⋯, σ(s n ), ⋯)
of events in A obtained from a serialisation

s 1 , s 2 , ⋯, s n , ⋯ of a configuration x ∈ C ∞ (S). Clearly α is a serialisation of σx ∈ C ∞ (A).
From the local injectivity of σ, the configuration x will be finite/infinite according as the trace is finite/infinite. We say that α is a trace of the configuration x in σ, or that x has trace α in σ.

Proposition 10.1. Let σ ∶ S → A be a strategy. (i) Any countable configuration of S has a trace. (ii) Let x ∈ C ∞ (S) and α be an enumeration

a 1 , a 2 , ⋯, a n , ⋯ of σx.
Then, α is a trace of x in σ iff for all s, s ′ ∈ x if s s ′ then σ(s) precedes σ(s ′ ) in the enumeration α.

Proof. (i) Let x be a countable configuration of S w.r.t. the strategy σ ∶ S → A. This follows because there is a serialisation x = {s 1 , s 2 , ⋯, s n , ⋯}, in which {s 1 , ⋯, s i } is down-closed in S at all i in the enumeration. To see this, from its countability we may assume a countable enumeration of x, which need not be a serialisation. Define s 1 ∈ x to be the earliest event of the enumeration for which [s 1 ) = ∅ in S; such an s 1 is ensured to exist by the well-foundedness of causal dependency provided x ≠ ∅. Inductively, define s n to be the earliest event of the enumeration which is in x ∖ {s 1 , ⋯, s n-1 } and for which [s n ) ⊆ {s 1 , ⋯, s n-1 }; again the well-foundedness of causal dependency ensures such an s n exists provided x∖{s 1 , ⋯, s n-1 } ≠ ∅. It is elementary to check this provides a serialisation of x.

(ii) "Only if ": Directly from the definition of trace of a configuration. "If ": Via the local bijection between x and σx given by σ we obtain an enumeration

s 1 , s 2 , ⋯, s n , ⋯ of x matching α in that σ(s i ) = a i .
The assumption that s s ′ implies σ(s) precedes σ(s ′ ) in the enumeration α, entails {s 1 , ⋯, s i } ∈ C(S) for all i. Hence the enumeration of x is a serialisation making α a trace of x.

Lemma 10.2. Let σ ∶ S → A be a strategy in a game A. Let x ∈ C ∞ (S). Let α be a serialisation of σx which is not a trace of x ∈ C ∞ (S). Then, there are s, s ′ ∈ x with pol (s) =and pol (s ′ ) = + and s S s ′ with (note the order reversal) σ(s ′ ) ≤ α σ(s) in α (regarded as a total order).

Proof. By assumption, any trace of x differs from α. We deduce there is s s ′ in x with σ(s) ≤ σ(s ′ ) in the total order of α; otherwise we could serialise x to obtain the trace α -Proposition 10.1(ii). Now, σ(s) ≤ A σ(s ′ ) in A as any serialisation must respect the order ≤ A . Hence, by the innocence of σ, we must have pol (s) =and pol (s

′ ) = +. Because α is totally ordered, σ(s ′ ) ≤ σ(s) in α.

Characterisation of the 'may' preorder

For stopping strategies (with games assumed race-free) we have: Theorem 10.3. Let (σ 1 , M 1 ) and (σ 2 , M 2 ) be stopping strategies in a common game. Then, (σ 1 , M 1 ) may pass τ implies (σ 2 , M 2 ) may pass τ , for all tests τ , iff all finite traces of σ 1 are traces of σ 2 .

Proof. Assume strategies σ 1 ∶ S 1 → A and σ 2 ∶ S 2 → A. "if ": Assume all finite traces of σ 1 are traces of σ 2 . Suppose (σ 1 , M 1 ) may pass test τ with event structure T . Then there is a successful configuration w ⊛ x 1 ∈ C(T ⊛ S 1 ), where x 1 ∈ C(S 1 ) and w ∈ C(T ); it is successful in the sense that its image contains the success event ✓. Take a serialisation of w ⊛ x 1 ; this induces a serialisation of x 1 to yield a trace. Then, by assumption, σ 2 has a configuration x 2 ∈ C(S 2 ) with the same trace, so a matching serialisation. Consequently the pairing w ⊛ x 2 is defined with w ⊛ x 2 ∈ C(T ⊛ S 2 ); sharing the same image as w ⊛ x 1 it is also successful.

"only if ": We show the contraposition: assuming not all traces of σ 1 are traces of σ 2 , we produce a test τ for which σ 1 may pass τ while it is not the case that σ 2 may pass τ .

Assume a trace α 1 of x 1 ∈ C(S 1 ) is not a trace of any x 2 ∈ C(S 2 ). Note that the trace α 1 , and correspondingly x 1 , must have at least one +ve event as otherwise, by receptivity, σ 2 could match the trace α 1 . Any trace of x 2 , with σ 2 x 2 = σ 1 x 1 , differs from α 1 . By Lemma 10.2, we deduce there are s, s ′ ∈ x 2 such that s 2 s ′ with pol (s) =and pol (s ′ ) = + and σ 2 (s ′ ) ≤ 1 σ 2 (s) in the total order α 1 .

Thus for each x 2 ∈ C(S 2 ) with σ 2 x 2 = σ 1 x 1 we can choose θ(x 2 ) = (s, s ′ ) so that s 2 s ′ in x 2 with pol (s) =and pol (s ′ ) = + and σ 2 (s ′ ) ≤ 1 σ 2 (s) in α 1 .

We now describe a test τ ∶ T → A ⊥ ∥⊞ which will discriminate between σ 1 and σ 2 . Let T ′ 1 be the elementary event structure comprising events T 1 = def σ 1 x 1 saturated with all accessible Opponent moves (note, in A ⊥ ), i.e. events

T ′ 1 = {a ∈ A pol A ⊥ ([a] ∖ T 1 ) ⊆ {-}}
with order that of A ⊥ augmented with σ 2 (s ′ ) ≤ 1 σ 2 (s) for every choice θ(x 2 ) = (s, s ′ ) where x 2 ∈ M 2 and σ 2 x 2 = σ 1 x 1 ; the ensuing relation on T 1 is included in the total order α 1 so forms a partial order in which every element has only finitely many elements below it. (By design, T ′ 1 "disagrees" with the causal dependency of each x 2 ∈ C(S 2 ) for which σ 2 x 2 = σ 1 x 1 .) The polarities of events of T ′ 1 are those of its events in A ⊥ . On T ′ 1 the map τ takes an event to its same event in A ⊥ .

Let T be the event structure with polarity obtained from T ′ 1 by adjoining a fresh 'success' event ⊞ with additional causal dependency so t 1 ≤ T ⊞ iff t 1 is -ve; as noted above there has to be at least one +ve event in x 1 and thus, by the reversal of polarity, at least one t 1 ∈ T 1 of -ve polarity. Then the obvious map τ ∶ T → A ⊥ ∥⊞ is a strategy, and a suitable test for σ 1 and σ 2 .

We have (i) σ 1 may pass τ , while (ii) it is not the case that σ 2 may pass τ .

To see (i), remark that the relation of causal dependency on T 1 is included in the the total order of the trace α 1 of x 1 . Hence τ ⊛ σ 1 has a successful configuration (T 1 ∪ {⊞}) ⊛ x 1 .

To show (ii), consider any finite configuration of τ ⊛ σ 2 . It has the form w ⊛ x 2 where w ∈ C(T ) and x 2 ∈ C(S 2 ). The configuration w ⊛ x 2 is unsuccessful because ⊞ ∉ w, as we now show. By design, τ and σ 2 enforce opposing causal dependencies on a pair of synchronisations needed for T 1 ⊛ x 2 to be defined whenever x 2 ∈ C(S 2 ) with σ 2 x 2 = T 1 . At least two events of opposing polarity in T 1 are excluded from any pairing w ⊛ x 2 ; one must be a -ve event of T 1 on which ⊞ causally depends; hence ⊞ ∉ w.

That the characterisation of the 'may' preorder above only depends on finite traces is not surprising, and familiar from previous work; the full-abstraction results of Dan Ghica and Andrzej Murawski w.r.t. 'may' behaviour rely only on finite traces [START_REF] Ghica | Angelic semantics of fine-grained concurrency[END_REF].

Clearly the proof above does not rely on stopping configurations or tests being bare rather than pure strategies; the test used in the proof patently has no neutral events. The extra discriminating power of tests based on bare strategies, illustrated in Example 9.6, does play an essential role in the analgous result in the 'must' case, to be considered now.

Characterisation of the 'must' preorder

Recall an event structure E = (E, ≤, Con) is consistent-countable iff there is a function χ ∶ E → ω from the events such that

{e 1 , e 2 } ∈ Con & χ(e 1 ) = χ(e 2 ) ⇒ e 1 = e 2 .
Any configuration x ∈ C ∞ (E) of a consistent-countable event structure E is countable and so may be serialised as x = {e 1 , e 2 , ⋯, e n , ⋯} so that {e 1 , ⋯, e n } ∈ C(E) for any finite subsequence. For the must case we assume that games are consistent-countable. It follows that strategies σ ∶ S → A in consistent-countable games A have S consistent-countable. W.r.t. such a strategy σ, we have traces of all configurations.

Theorem 10.4. Assume game A is consistent-countable. Let (σ 1 , M 1 ) and (σ 2 , M 2 ) be stopping strategies in A. Then, (σ 2 , M 2 ) must pass τ implies (σ 1 , M 1 ) must pass τ , for all tests τ , iff all traces of stopping configurations M 1 are traces of stopping configurations M 2 .

Proof. "if ": Assume all traces of stopping configurations M 1 are traces of stopping configurations M 2 . A stopping configuration of τ ⊛ σ 1 has the form w ⊛ x 1 where w and x 1 are stopping configurations of τ and σ 1 , respectively. A serialisation of w ⊛ x 1 into a (possibly infinite) sequence induces a serialisation of x 1 ∈ M 1 . By assumption, there is x 2 ∈ M 2 with the same trace in A as x 1 . Consequently, w ⊛ x 2 is a configuration of τ ⊛ σ 2 with the same image in A∥⊞.

Moreover, w ⊛ x 2 is a stopping configuration of τ ⊛ σ 2 . Supposing (σ 2 , M 2 ) must pass a test τ , the image of w ⊛ x 2 contains ✓ whence the image of w ⊛ x 1 contains ✓ ensuring (σ 1 , M 1 ) must pass a test τ .

"only if ": We show the contraposition: assuming not all traces of stopping configurations M 1 are traces of stopping configurations M 2 , we produce a test τ for which (σ 2 , M 2 ) must pass τ while it is not the case that (σ 1 , M 1 ) must pass τ .

Assume a trace α 1 of x 1 ∈ M 1 is not a trace of any x 2 ∈ M 2 .

In particular, consider any x 2 ∈ M 2 with σ 2 x 2 = σ 1 x 1 . Then, any trace of x 2 differs from α 1 . By Lemma 10.2, there are s, s ∈ x 2 such that s 2 s ′ with pol (s) =and pol (s ′ ) = + and σ 2 (s ′ ≤ 1 σ 2 (s) in the total order α 1 .

Thus for each x 2 ∈ M 2 with σ 2 x 2 = σ 1 x 1 we can choose θ(x 2 ) = (s, s ′ ) so that s 2 s ′ in x 2 with pol (s) =and pol (s ′ ) = + and σ 2 (s ′ ) ≤ 1 σ 2 (s) in α 1 .

We build an event structure with polarity T and a test as bare strategy τ ∶ T → A ⊥ ∥N ∥⊞. We build the events of T as T ′ 1 ∪ N ∪ T 2 , a union of sets of events, assumed disjoint, described as follows.

• Let T ′ 1 be the elementary event structure comprising events T 1 = def σ 1 x 1 saturated with all accessible Opponent moves, i.e. events

T ′ 1 = {a ∈ A pol A ⊥ ([a] ∖ T 1 ) ⊆ {-}}
with order that of A augmented with σ 2 (s ′ ) ≤ 1 σ 2 (s) for every choice θ(x 2 ) = (s, s ′ ) where x 2 ∈ M 2 and σ 2 x 2 = σ 1 x 1 ; the ensuing relation on T 1 is included in the total order α 1 so forms a partial order in which every element has only finitely many elements below it. (By design, T ′ 1 "disagrees" with the causal dependency of each x 2 ∈ M 2 for which σ 2 x 2 = σ 1 x 1 .) The polarities of events of T ′ 1 are those of its events in A ⊥ . On T ′ 1 the map τ takes an event to its same event in A ⊥ .

• N comprises a copy of the set of events of -ve polarity in T 1 ; all the events of N have neutral polarity; an event of N is sent by τ to its copy.

• T 2 comprises a copy of the set of events T 1 ; all the events of T 2 have +ve polarity; they are all sent by τ to ✓ = def (3, ⊞).

• Causal dependency on T is that of T ′ 1 augmented with dependencies from events of T 1 of -ve polarity to their corresponding copies in N .

• The consistency relation of T is that minimal relation which ensures that: any two distinct events of T 2 are in conflict; a +ve event of T 1 conflicts with its corresponding copy in T 2 ; and a neutral event in N conflicts with its corresponding copy in T 2 . Formally,

X ∈ Con T iff X ⊆ fin T 1 ∪ N ∪ T 2 & X ∩ T 2 ≤ 1 & (∀t 1 ∈ X ∩ T + 1 , t 2 ∈ X ∩ T 2 . t 1 , t 2 are not copies of a common event) & (∀n ∈ X ∩ N, t 2 ∈ X ∩ T 2 . n, t 2 are not copies of a common event).
Note that all the events over ✓, which together comprise the set T 2 , can occur initially but can become blocked as moves are made in T 1 . In particular, the set T 1 ∪ N is a +-maximal configuration of T with image in A ⊥ ∥N ∥⊞ not containing any event over ✓. On the other hand any +-maximal configuration of T not including all the events T 1 will contain an event over ✓. Hence St(τ ) has an unsuccessful stopping configuration consisting of precisely all the events of T 1 -it does not have an event over ✓-while all stopping configurations of St(τ ) which do contain all the events of T 1 are successful-they contain an event over ✓.

Consequently, (i) it is not the case that (σ 1 , M 1 ) must τ , while (ii) (σ 2 , M 2 ) must τ . To see (i), remark that the relation of causal dependency on T 1 is included in the the total order of the trace α 1 of x 1 . Hence St(τ ) ⊛ σ 1 has a stopping configuration T 1 ⊛ x 1 which is unsuccessful and thus (σ 1 , M 1 ) fails the must test τ . To show (ii), consider any stopping configuration of St(τ ) ⊛ σ 2 . It comprises w ⊛ x 2 where w is a stopping configuration of St(τ ) and x 2 ∈ M 2 , a stopping configuration of σ 2 . Now w ⊇ T 1 , as by design τ and σ 2 enforce opposing causal dependencies on a pair of synchronisations needed for T 1 ⊛ x 2 to be defined whenever x 2 ∈ M 2 with σ 2 x 2 = T 1 . Thus w is successful in that it contains an event over ✓. Hence (σ 2 , M 2 ) must pass τ . This completes the proof.

Remark. By Example 9.6, the result above would not hold if tests were based solely on pure strategies.

Example 10.5. Let A be the game

⊞ ⊟ ❴ ⊟ ❴ L L R

⊞

Let σ 1 be the stopping strategy given by the identity map id A ∶ A → A together with the +-maximal configurations of A. Let σ 2 be the stopping strategy derived from the event structure

⊞ / o / o ⊞ ⊟ ✤ l l r ❴ ✂ % ❇ ❇ ❇ ❇ ❇ ⊟ ❴ L L R ✤ , , 2 ✂ [ [ e ❇ ❇ ❇ ❇ ❇ ⊞ ⊞ o / o /
in which there are additional occurrences of Player moves awaiting both moves of Opponent; the map to A is the obvious one and its stopping configurations the +-maximal ones. It can be checked that the two stopping strategies share the same traces of stopping configurations so are 'must' equivalent. ◻

Infinite stopping configurations play an essential role in the 'must' behaviour of strategies:

Example 10.6. Let the game A consist of an infinite chain of alternating Player-Opponent moves:

⊞ ✤ , , 2 ⊟ ✤ , , 2 ⊞ ✤ , , 2 ⊟ ✤ , , 2 ⋯ ✤ , , 2 ⊞ ✤ , , 2 ⊟ ✤ , , 2 ⋯
The strategy σ 1 has as consistent components a copy of A itself and copies of all its initial finite sequences of events ending with an Opponent move; events different components are inconsistent with each other-we refrain from drawing the wiggly conflicts. The map σ 1 is obvious. (The construction is an instance of the sum of strategies-see Section ??.)

⊞ ✤ , , 2 ⊟ ⊞ ✤ , , 2 ⊟ ✤ , , 2 ⊞ ✤ , , 2 ⊟ ⊞ ✤ , , 2 ⊟ ✤ , , 2 ⊞ ✤ , , 2 ⊟ ✤ , , 2 ⊞ ✤ , , 2 ⊟ ⋮ ⊞ ✤ , , 2 ⊟ ✤ , , 2 ⊞ ✤ , , 2 ⊟ ✤ , , 2 ⋯ ✤ , , 2 ⊞ ✤ , , 2 ⊟ ⋮ ⊞ ✤ , , 2 ⊟ ✤ , , 2 ⊞ ✤ , , 2 ⊟ ✤ , , 2 ⋯ ✤ , , 2 ⊞ ✤ , , 2 ⊟ ✤ , , 2 ⊞ ✤ , , 2 ⋯
The lowest component is a copy of A. The stopping configurations are all its +-maximal configurations, i.e. those sets consisting of a whole component or an initial subsequence of a component which ends in a Player move. The strategy σ 2 is like σ 1 but without the extra infinite component of shape A. Its stopping configurations are all its +-maximal configurations, so are necessarily all finite.

The traces of σ 1 's and σ 2 's finite stopping configurations coincide. However the trace of the infinite stopping configuration of σ 1 cannot be a trace of σ 2 . Accordingly, from Theorem 10.4, there is a test strategy which σ 2 must pass while σ 1 does not. A distinguishing test τ ∶ T → A ⊥ ∥⊞✓ has T comprising the infinite event structure shown below.

⊟ ❴ ✤ , , 2 ⊞ ✤ , , 2 ⊟ ❴ ✤ , , 2 ⊞ ✤ , , 2 ⊟ ❴ ✤ , , 2 ⊞ ✤ , , 2 ⊟ ❴ ✤ , , 2 ⊞ ✤ , , 2 ⋯ ⊞✓ / o / o / o / o / o / o / o
11 The rigid image of a stopping strategy

In this section we rely on the material of Section 4, in particular that a strategy σ ∶ S → A in a game A has a rigid image

S σ ❅ ❅ ❅ ❅ ❅ ❅ ❅ ❅ f / / / / S 0 σ1 A ,
where f is rigid epi and the rigid image σ 1 is a total map; the map σ 1 automatically inherits the properties required a strategy. (The construction and key properties of rigid image are unaffected by the extra structure of polarity.) As has been remarked earlier [START_REF] Winskel | Event Structures, Stable Families and Concurrent Games[END_REF][START_REF] Castellan | Distributed strategies made easy[END_REF], rigid-image strategies have the advantage of forming a category rather than a bicategory. Extended with stopping configurations they can support 'may' and 'must' behaviour. Definition 11.1. Let (σ, M S ) be a stopping strategy. Let σ 1 be the rigid image of σ with accompanying 2-cell f ∶ σ ⇒ σ 1 where f is rigid epi. We define the rigid image of (σ, M S ) to be (σ 1 , f M S ). A rigid-image stopping strategy is one which is its own rigid-image.

As a direct consequence of the last part of Lemma 9.5, we are assured the rigid image of a stopping strategy does not lose any 'may' and 'must' behaviour. Proposition 11.2. A stopping strategy is both 'may' and 'must' equivalent to its rigid image.

As far as 'may' and 'must' behaviour is concerned it is sensible to regard two stopping strategies as equivalent if they share a common rigid image. Rigidimage equivalence transfers to an equivalence between bare strategies: two bare strategies are equivalent if under St we obtain equivalent stopping strategies. W.r.t. 'may' and 'must' behaviour we can choose to work in the category of rigid-image stopping strategies.

What axioms hold of stopping configurations? Such axioms should be preserved by the composition of stopping strategies and rigid image. They should also be complete in the sense that any stopping strategy which satisfied them is rigid-image equivalent to the stopping strategy of some bare strategy. We do not presently know a complete set of axioms for stopping configurations. Candidate axioms on a stopping strategy σ ∶ S → A with stopping configurations M are Axiom (i) ∀x ∈ C(S)∃y ∈ M. x ⊆ y , and Axiom (ii) ∀y ∈ M, x ∈ C ∞ (S). x ⊆ y & x is +-maximal in S ⇒ x ∈ M .

The example below shows why we do not assume all +-maximal configurations are stopping. That property is not preserved by taking the rigid image.

Example 11.3. In forming the rigid image σ 1 ∶ S 1 → A of a strategy σ ∶ S → A, related by rigid epi 2-cell f ∶ σ ⇒ σ 1 , it is possible to have an infinite configuration of S 1 which is not in the direct image under f of any configuration of S; in particular it is possible to have a +-maximal configuration of S 1 which is not a direct image of any +-maximal configuration S. For example, let A comprise an infinite chain of Player events. Take S to be the sum of all finite subchains. The rigid image of S is A itself which has +-maximal configuration comprising all the events in the infinite chain, not the image of any configuration of S 1 . Thus, in forming the rigid image of a stopping strategy, we cannot assume that all the +-maximal configurations of the rigid image are stopping. ◻

12 Strategies as concurrent processes

The paper [START_REF] Castellan | Strategies as concurrent processes[END_REF] is a closely related study of concurrent strategies from the perspective of concurrent processes, considering how concurrent games and strategies are objects which we can program. Concurrent strategies are shown to support operations yielding an economic yet rich higher-order concurrent process language, which shares features both with process calculi and nondeterministic dataflow. There a slightly weakened definition of bare strategies plays a key role in providing an operational semantics. It would be satisfying to complete this story by providing inequational proof systems for 'may' and 'must' equivalence based on its syntax for strategies, drawing inspiration from the classic work of Hennessy and de Nicola [START_REF] De Nicola | Testing equivalences for processes[END_REF]. Process calculi often allow unrestricted recursion. Strategies, as presented here, form a model of linear logic which restricts the copying of parameters needed in recursive definitions. The treatment of unrestricted recursion requires a move to nonlinear strategies over games with symmetry [START_REF] Castellan | Symmetry in concurrent games[END_REF][START_REF] Castellan | Thin games with symmetry and concurrent hyland-ong games[END_REF]. The recursive definition of bare strategies and strategies can follow classical ideas; 2-cells include the rigid embeddings and inclusions of [START_REF] Winskel | Event structure semantics for CCS and related languages[END_REF]. Less clear is how to carry out recursive definitions directly on stopping strategies; the 2-cells we have chosen would seem to be too restrictive; and the nature of stopping configurations, that they can be infinite without finite approximations, would push the development into non-continuous operations-nonstandard, if not in itself a bad thing.

A treatment of winning concurrent strategies has been presented [START_REF] Clairambault | The winning ways of concurrent games[END_REF]. Informally a strategy is winning if it must end up in a winning configuration of the game regardless of the behaviour of Opponent. In idea this is very close to controllability in [START_REF] Alur | Alternating-time temporal logic[END_REF]. Because the semantics of composition of composition of strategies in [START_REF] Clairambault | The winning ways of concurrent games[END_REF] is inattentive to the possibilities of deadlock and divergence, a strategy which is obtained as a composition may be deemed winning there and yet possibly deadlock or diverge before reaching a winning configuration [START_REF] Castellan | Strategies as concurrent processes[END_REF]. Fortunately the treatment of winning strategies ibid. generalises straightforwardly to stopping strategies which keep track of deadlock and divergence, and thus repair this defect. The role of +-maximal configurations in [START_REF] Clairambault | The winning ways of concurrent games[END_REF] is replaced by that of stopping configurations: a bare or stopping strategy is winning iff all its stopping configurations image to winning strategies in the game.

Forearmed with concurrent strategies and games with symmetry it would be interesting to revisit old ideas extending testing to other equivalences beyond those of 'may' and 'must' [START_REF] Abramsky | Observation equivalence as a testing equivalence[END_REF]. Certainly one could wish for a better integration of games and strategies with the classical work on concurrency, process algebra and its equivalences included. The medium of concurrent games and strategies based on event structures also provides an inroad into the formalisation and analysis of probabilistic and quantum languages and processes [START_REF] Winskel | Distributed probabilistic and quantum strategies[END_REF][START_REF] Castellan | The concurrent game semantics of probabilistic PCF[END_REF][START_REF] Clairambault | Game semantics for quantum programming[END_REF].

Example 5 . 2 .

 52 Let B be the game consisting of two concurrent Player events b 1 and b 2 , and C the game with a single Player event c. We illustrate the composition of two strategies σ 1 and σ 2 from the empty game ∅ to B, with τ from B to C. The strategy σ 1 in the game ∅ ⊥ ∥B nondeterministically plays b 1 or b 2 . The strategy σ 2 also in the game ∅ ⊥ ∥B just plays b 2 . The strategy τ in the game B ⊥ ∥C does nothing if just b 1 is played and plays the single Player event c of C if b 2 is played. The composition τ ⊙σ 1 in the game ∅ ⊥ ∥C may play c or not according as σ 1 plays b 1 or b 2 . The composition τ ⊙σ 2 also in the game ∅ ⊥ ∥C must play c. But the two compositions τ ⊙σ 1 and τ ⊙σ 2 are indistinguishable once the interaction over the common game B is hidden. ◻

  and finite subsets of C C A consistent if their down-closure w.r.t. ≤ C C A are consistent in A ⊥ ∥A. (For c ∈ A ⊥ ∥A we use c to mean the corresponding copy of c, of opposite polarity, in the alternative component, i.e. (1, a) = (2, a) and (2, a) = (1, a).) The configurations of C C A have the form x∥y where y ⊑ A x, i.e. y ⊇ -x ∩ y ⊆ + x, for x, y ∈ C ∞ (A). (The relation ⊑ A is a partial order, called the Scott order [29].)

Definition 7 . 1 .

 71 Let σ be a bare strategy in a game A. Let τ ∶ T → A ⊥ ∥N ∥⊞ be a 'test' bare strategy from A to the game consisting of a single Player move ⊞. Write ✓ = def (3, ⊞).

Lemma 8 . 6 .

 86 Recall from Definition 8.3 the operation St ∶ σ ↦ (σ ↓ , Stop(σ)) which takes a bare strategy σ to a stopping strategy. It preserves composition: Let σ ∶ S → A ⊥ ∥M ∥B and τ ∶ T → B ⊥ ∥N ∥C be bare strategies. Then, St(τ ⊛ σ) = St(τ )⊙St(σ) . Proof. By Lemma 6.4, it suffices to show Stop(τ ⊛ σ) = Stop(τ )⊙Stop(σ) . Configurations of Stop(τ ⊛σ) are of the form (y⊛x) ↓ where y⊛x is +-maximal for x ∈ C ∞ (S) and y ∈ C ∞ (T ). By Lemma 6.3 these coincide with configurations (y⊛ x) ↓ for which both x and y are +-maximal. Configurations of Stop(τ )⊙Stop(σ) take the form y ↓ ⊙x ↓ where x ∈ C ∞ (S) and y ∈ C ∞ (T ) are +-maximal. But by Lemma 6.4, (y ⊛ x) ↓ = y ↓ ⊙x ↓ , ensuring the desired equality.

Lemma 9 . 3 .

 93 Let A be a race-free game. Let σ be a bare strategy in A. Then, σ may pass a test τ iff St(σ) may pass τ ; σ must pass a test τ iff St(σ) must pass τ .

  Let E and E ′ be event structures. A map of event structures

	we illustrate the relations of immediate causal dependency	✤ , , 2 which yields
	the Hasse diagram of the partial order of causal dependency between events ,
	and conflict by the wiggly line	/ o / o / o . Neither the two events related by
	/ o / o / o	nor their dependants w.r.t. causal dependency can occur together in a
	configuration; there is no need draw all the conflicts that follow.	◻

Here it is useful to allow stable families to have infinite configurations, as originally[23,

[START_REF] Winskel | Event structures[END_REF].

Acknowledgments

Thanks to Jonathan Hayman, Sacha Huriot, Martin Hyland, Marc Lasson, Conor McBride and Marc de Visme for encouragement and helpful discussions. Thanks to the anonymous referee. Support of Advanced Grant ECSYM (2011-17) of the European Research Council is acknowledged with gratitude. The second author gratefully acknowledges support by ANR project DyVerSe (ANR-19-CE48-0010-01) and Labex MiLyon (ANR-10-LABX-0070) of Université de Lyon, within the program "Investissements d'Avenir" (ANR-11-IDEX-0007), operated by the French National Research Agency (ANR).