{'fraction_non_alphanumeric': 0.04742702885102075, 'fraction_numerical': 0.008975873122996457, 'mean_word_length': 3.941720860430215, 'pattern_counts': {'":': 4, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 21, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
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 [1]; and equivalences on concurrent processes through testing [2]. 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 [3] and Hoare's on failures equivalence [4]. 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 [5]. 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 [2]: 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 [6,7]-foreshadowed in the early definitions of concurrent strategy [1,8,9,10]. 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 [11]. Event structures are a central model for concurrent computation, related to other models by adjunctions [12]. 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" [13], the categorical underpinnings of which were exposed by André Joyal [14]. 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 [15]. The other, that we follow here, is through extending strategies with the extra structure of stopping configurations [16]. 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" [17], 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 [18]. 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 [19]-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 [8]. 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 [17]. 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 [20]. 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 [21,22]. 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 [2].

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 • Y ⊆ X ∈ Con implies Y ∈ Con, and 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 .) 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 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.
Consider a partial map of event structures f ∶ E → E ′ . Let Then f clearly factors into the composition 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 where g 0 is partial and g 1 is total there is a (necessarily total) unique map h ∶ E↓V → E 1 such that 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 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.
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 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, 1 i.e. it is We now apply a general construction Pr(B) for obtaining an event structure from the stable family B. Suppose (a, b) ∈ θ where θ ∈ B [23,24]. Because B is a stable family 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.
yields an event structure. There is an order isomorphism 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 [23,25].
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 We can regard such augmentations as elementary event structures in which all subsets of events are consistent. Order all augmentations by taking Augmentations under ↪ form a prime algebraic domain [11,26], 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. [27] 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 mapf ∶ 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, with the following universal property: for any factorisation of commutes; the map h is necessarily also rigid and epi.
From the universal property of rigid image we derive: 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.
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.
their polarities unchanged, with the only relations of causal dependency given by 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 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: Example 5.2. 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. ◻ 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; (iii) σ is innocent in that it is both +-innocent and −-innocent: 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 [6].
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 ∅.
commutes. In this way bare strategies in A ⊥ ∥N ∥B form a category, 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 the defined part σ ↓ is a strategy, which we call the visible part of σ.
(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 for the visible image of a configuration x ∈ C ∞ (S). The hiding operation on strategies extends to a functor between their visible parts. It acts so for all x ∈ C ∞ (S).

Composition
We can compose two bare strategies by pullback. Ignoring polarities temporarily, and padding with identity maps, we obtain τ ⊛ σ via the pullback 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 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 τ .
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 Composition of bare strategies restricts to a functor between rigid 2-cells.
We obtain the composition of strategies as the composite functor Though we generally elide the isomorphisms regarding strategies as bare strategies without neutral events, and write 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 we can present a typical configuration of T ⊙S as Composition is preserved in extracting the visible part from bare strategies: For x ∈ C ∞ (S) and y ∈ C ∞ (T ), 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 [6].
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  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].) 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).
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 [6]. 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 .
⊞ 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 [5]. 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: The game A consists of five events with the polarity and causal dependency shown. One bare strategy σ 1 is with one neutral event, while the other σ 2 is 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 σ 2

t t t t t t t t t t t t
⊞✓ .
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. ◻ This example might be puzzling to readers familiar with Harmer and Mc-Cusker's fully abstract model for (sequential) finite non-determinism [17], 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 [17], 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 tests 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 [16].) 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. [6, 30] 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
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 So, in other words, 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, 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.
for the category of 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. 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 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. Recall from Definition 8.3 the operation which takes a bare strategy σ to a stopping strategy. It preserves composition: Proof. By Lemma 6.4, it suffices to show 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.
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: Let BStrat + (A, N, B) be the subcategory where 2-cells are +-reflecting. Then

'May' and 'Must' testing
We can rephrase 'may' and 'must' testing in terms of stopping strategies. 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 ✓. Lemma 9.3. 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 τ .
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 [3]. 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: No pair would be weakly bisimilar due to the presence of pre-emptive internal events [3]. 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. 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 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. 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 σ. 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: 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 .
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 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 [8].
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 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. 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 τ .
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 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, 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 not 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.
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: 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 of 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 ??.) 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. The strategy σ 2 must pass τ ; all +-maximal configurations of τ ⊛ σ 2 are finite and contain a ✓-event. Whereas the strategy σ 1 can fail to enable a ✓-event through its extra infinite stopping configuration. ◻

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 where f is rigid epi and the rigid image σ 1 is a total map; the map σ 1 automatically inherits the properties required of a strategy. (The construction and key properties of rigid image are unaffected by the extra structure of polarity.) As has been remarked earlier [25,19], 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. ◻

Strategies as concurrent processes
The paper [16] 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 [5]. 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 [21,22]. The recursive definition of bare strategies and strategies can follow classical ideas; 2-cells include the rigid embeddings and inclusions of [23]. 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 [31]. 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 [32]. Because the semantics of composition of composition of strategies in [31] 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 [16]. 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 [31] 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' [2]. 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 [33,34,35].