scientifiques de niveau recherche, publiés ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Coalgebraic Multigames

Marina Lenisa 1 Dipartimento di Matematica e Informatica, Università di Udine, Italy.

marina.lenisa@uniud.it

Abstract. Coalgebraic games have been recently introduced as a generalization of Conway games and other notions of games arising in different contexts. Using coalgebraic methods, games can be viewed as elements of a final coalgebra for a suitable functor, and operations on games can be analyzed in terms of (generalized) coiteration schemata. Coalgebraic games are sequential in nature, i.e. at each step either the Left (L) or the Right (R) player moves (global polarization), moreover only a single move can be performed at each step. Recently, in the context of Game Semantics, concurrent games have been introduced, where global polarization is abandoned, and multiple moves are allowed. In this paper, we introduce coalgebraic multigames, which are situated half-way between traditional sequential games and concurrent games: global polarization is still present, however multiple moves are possible at each step, i.e. a team of L/R players moves in parallel. Coalgebraic operations, such as sum and negation, can be naturally defined on multigames. Interestingly, sum on coalgebraic multigames turns out to be related to Conway's selective sum on games, rather than the usual (sequential) disjoint sum. Selective sum has a parallel nature, in that at each step the current player performs a move in at least one component of the sum game, while on disjoint sum the current player performs a move in exactly one component at each step. A monoidal closed category of coalgebraic multigames in the vein of a Joyal category of Conway games is then built. The relationship between coalgebraic multigames and games is then formalized via an equivalence of the multigame category and a monoidal closed category of coalgebraic games where tensor is selective sum.

Introduction

In [START_REF] Honsell | Conway Games, coalgebraically[END_REF], coalgebraic games have been introduced as a generalization of Conway games [START_REF] Conway | On Numbers and Games[END_REF] to possibly non-terminating games. Coalgebras offer an elementary but sufficiently abstract framework, where games are represented as elements of a final coalgebra for a suitable functor, by abstracting away superficial features of positions, and operations are smoothly defined as final morphisms via (generalized) coiteration schemata. Coalgebraic games have been further studied and generalized in [START_REF] Honsell | Conway Games, algebraically and coalgebraically[END_REF][START_REF] Honsell | Equivalences and Congruences on Infinite Conway Games[END_REF][START_REF] Honsell | Categories of Coalgebraic Games[END_REF][START_REF] Honsell | Categories of Coalgebraic Games with Selective Sum[END_REF]. In particular, in [START_REF] Honsell | Categories of Coalgebraic Games[END_REF], coalgebraic games have been shown to subsume also games arising in the context of Game Semantics. In [START_REF] Abramsky | Coalgebraic Analysis of Subgame-perfect Equilibria in Infinite Games without Discounting[END_REF] Work supported by MIUR PRIN Project CINA 2010LHT4KM.

a similar notion of coalgebraic game has been used to model games arising in Economics (see also [START_REF] Lescanne | Rationality and escalation in infinite extensive games[END_REF][START_REF] Lescanne | Backward coinduction, Nash equilibrium and the rationality of escalation[END_REF]). Coalgebraic games are 2-player games of perfect information, the two players being Left (L) and Right (R). A game is identified with its initial position. At any position, there are moves for L and R taking to new positions of the game. Contrary to other approaches in the literature, where games are defined as graphs, we view possibly non-wellfounded games as points of a final coalgebra of graphs, i.e. minimal graphs w.r.t. bisimilarity. This coalgebraic representation is more in the spirit of Conway's original presentation, and it is motivated by the fact that the existence of winning/non-losing strategies is invariant w.r.t. graph bisimilarity.

Coalgebraic games are sequential in nature, i.e. at each step either L or R moves (global polarization), moreover only a single move can be performed at each step. Recently, in the context of Game Semantics, concurrent games have been introduced [START_REF] Abramsky | Concurrent games and full completeness[END_REF][START_REF] Ghica | On the compositionality of round abstraction[END_REF][START_REF] Rideau | Concurrent Strategies[END_REF][START_REF] Clairambault | The winning ways of concurrent games[END_REF], where global polarization is abandoned, and multiple moves are allowed.

In this paper, we introduce coalgebraic multigames, which are situated halfway between traditional sequential games and concurrent games: global polarization is still present, however multiple moves are possible at each step, i.e. a team of L/R players moves in parallel. Coalgebraic operations, such as sum and negation, can be naturally defined on multigames via (generalized) coiteration schemata.

The notion of coalgebraic multigame introduced in the present paper is inspired by that of multigame recently defined by the same authors in [START_REF] Honsell | Polarized Multigames[END_REF], in the context of Game Semantics. The approach in [START_REF] Honsell | Polarized Multigames[END_REF] is slightly different, in that (multi)games are defined via trees of positions, rather than coalgebraically as sets/minimal graphs.

The main difference between coalgebraic multigames and games lies in the fact that in the sum of games, at each step, the current player can move in exactly one component, while in the multigame sum, by exploiting the parallel nature of multigames, the current player can perform a multimove consisting of atomic moves on both components. Sum on games amounts to Conway's disjoint sum, which corresponds to interleaving semantics and standard tensor product in Game Semantics (see e.g. [START_REF] Abramsky | Full abstraction for PCF[END_REF][START_REF] Hyland | On Full Abstraction for PCF: I, II, and III[END_REF]), while multigame sum is related to Conway's selective sum, a form of parallel sum on games, where the current player can possibly move in both components.

We formalize the relationship between coalgebraic games and multigames in categorical terms. In particular, inspired by Joyal's categorical construction of Conway games [START_REF]Remarques sur la Theorie des Jeux a deux personnes[END_REF], we build a symmetric monoidal closed category of coalgebraic multigames, where tensor is multigame sum. Namely, in [START_REF]Remarques sur la Theorie des Jeux a deux personnes[END_REF], Joyal showed how to endow (well-founded) Conway games and winning strategies with a structure of compact closed category. This construction is based on the disjunctive sum of games, which induces a tensor product, and, in combination with negation, yields linear implication. Recently, the above categorical construction has been generalized to non-wellfounded games with disjoint or selective sum [START_REF] Honsell | Equivalences and Congruences on Infinite Conway Games[END_REF][START_REF] Honsell | Categories of Coalgebraic Games[END_REF][START_REF] Honsell | Categories of Coalgebraic Games with Selective Sum[END_REF], while, in the context of Linear Logic and Semantics, various categories of possibly non-wellfounded Conway games have been introduced and studied in [START_REF] Mellies | Comparing hierarchies of types in models of linear logic[END_REF][START_REF] Mellies | Asynchronous games 3: an innocent model of linear logic[END_REF][START_REF] Mellies | An explicit formula for the free exponential modality of linear logic[END_REF][START_REF] Honsell | Polarized Multigames[END_REF].

In the present paper, we build a category of coalgebraic multigames and strategies in the line of the above constructions. Moreover, we show that this is equivalent to a category of coalgebraic games with a parallel tensor product inspired by Conway' s selective sum. In particular, we carry out these categorical constructions in the context of polarized (multi)games, i.e. (multi)games where each position is marked as L or R, that is only L or R can move from that position, R starts, and L/R positions strictly alternate. Polarized games typically arise in Game Semantics, see e.g. [START_REF] Abramsky | Full abstraction for PCF[END_REF][START_REF] Hyland | On Full Abstraction for PCF: I, II, and III[END_REF][START_REF] Honsell | Polarized Multigames[END_REF].

Technically, the main difficulty in defining the above categories of (multi)games with parallel tensor product lies in the definition of strategy composition, which is not a straightforward adaptation of usual composition, but it requires a non-standard parallel application of strategies.

Our categorical constructions are related in particular to those carried out in [START_REF] Honsell | Polarized Multigames[END_REF] in the context of Game Semantics. In [START_REF] Honsell | Polarized Multigames[END_REF], the usefulness of multigames for modeling parallel languages is shown by providing a (universal) model of a simple parallel language, i.e. unary PCF with parallel or.

The interest of coalgebraic (multi)games is manifold. Multigames help in clarifying/factorizing the steps taking from sequential games (with global polarization and single moves) to concurrent games (no global polarization, multiple moves), offering a model of parallelism with a low level of complexity but still of a set-theoretic nature, compared to more complex concurrent games. Notably, the coalgebraic approach, both in the game and multigame version, appears significantly simpler than the traditional Game Semantics approach, where definitions of games and strategies require complex additional structures, such as equivalences on plays and strategies in the style of [START_REF] Abramsky | Full abstraction for PCF[END_REF], or pointers in the arena style [START_REF] Hyland | On Full Abstraction for PCF: I, II, and III[END_REF]. Such extra structure is not needed in the coalgebraic framework.

Related Work. Coalgebraic methods for modeling games have been used also in [START_REF] Barwise | Vicious Circles[END_REF], where the notion of membership game has been introduced. This corresponds to a subclass of our coalgebraic games, where at any position L and R have the same moves, and all infinite plays are deemed winning for player II (the player who does not start). However, no operations on games are considered in that setting. In the literature, various notions of bisimilarity equivalences have been considered on games, see e.g. [START_REF] Pauly | From Programs to Games: Invariance and Safety for Bisimulation[END_REF][START_REF] Van Benthem | Extensive games as process models[END_REF]. But, contrary to our approach, such games are defined as graphs of positions, and equivalences on graphs, such as trace equivalences or various bisimilarities are considered. By defining games as the elements of a final coalgebra, we directly work up to bisimilarity of game graphs.

Summary. In Section 2, we introduce the notions of coalgebraic multigame, play and strategy. In Section 3, we define operations on the final coalgebra of multigames via suitable (generalized) coiteration schemata. In Section 4, we build a monoidal closed category of polarized coalgebraic multigames and strategies, where tensor is sum. In Section 5, the relationship between coalgebraic multi-games and games is expressed in categorical terms via an equivalence between the category of multigames and a monoidal closed category of coalgebraic games where tensor is selective sum. Conclusions and directions for future work appear in Section 6.

We assume the reader familiar with basic notions of coalgebras, see [START_REF] Jacobs | A tutorial on (co)algebras and (co)induction[END_REF], and basic categorical definitions.

Coalgebraic Multigames and Strategies

In this section, we introduce the definitions of coalgebraic multigame, play, and strategy.

We consider a general notion of 2-player multigame of perfect information, where the two players are called Left (L) and Right (R). On a multigame, at each step, players can perform a multimove, i.e. a non-empty finite set of atomic moves. A multigame X is identified with its initial position; at any position, there are (multi)moves for L and R, taking to new positions of the game. By abstracting superficial features of positions, multigames can be viewed as elements of the final coalgebra for the functor F M A (A) = P <κ (M A × A), where A is a set of atomic moves, each atomic move is marked with the name of the player who performs the move, M A is the set of multimoves, i.e. the finite powerset of atomic moves with the same polarity, and P <κ is the set of all subsets of cardinality < κ, where κ can be ω if only games with finitely many moves are considered, or it can be an inaccessible cardinal if we are interested in more general games. The coalgebra structure captures, for any position, the moves of the players and the corresponding next positions.

We work in the category Set * of sets belonging to a universe satisfying the Antifoundation Axiom, see [START_REF] Forti | Set-theory with free construction principles[END_REF][START_REF] Aczel | Non-wellfounded sets[END_REF], where the objects are the sets with hereditary cardinal less than κ, and whose morphisms are the functions with hereditary cardinal less than κ1 . Of course, we could work in the category Set of wellfounded sets, but we prefer to use Set * so as to be able to use identities, i.e. extentional equalities in formal set theory, rather than isomorphisms in some naive set theory. Formally, we define:

Definition 1 (Coalgebraic Multigames).
-Let A be a set of atoms with functions:

(i) µ : A → N yielding the name of the move (for a set N of names), (ii) λ : A → {L, R} yielding the player who has moved. We assume that A is closed under complementation, i.e. a ∈ A ⇒ a ∈ A, where µa = µa and λa = λa, with R = L and L = R.

-Let M A be the powerset of all finite sets of atomic moves with the same polarity, i.e.

M A = {α ∈ P f (A) | ∀a, a ∈ α. λa = λa } .
-Let F M A : Set * → Set * be the functor defined by

F M A (A) = P <κ (M A × A)
with the usual definition on morphisms, and let (M A , id ) be the final

F M A - coalgebra 2 .
A coalgebraic multigame is an element X of the carrier M A of the final coalgebra.

The elements of the final coalgebra M A are the minimal graphs up to bisimilarity.

Clearly, every multigame can be viewed as a game whose moves are the multimoves. However, as we will see, multigame sum (as well as other constructions) is not preserved under this mapping.

We call player I the player who starts the multigame (who can be L or R in general), and player II the other. Once a player has moved on a multigame X, this leads to a new multigame/position X . We define the plays on X as the sequences of pairs move-position from X; moves in a play are alternating: Definition 2 (Plays). A play on a coalgebraic game X 0 is a possibly empty finite or infinite sequence of pairs in

M A × M A , s = α 1 , X 1 . . . such that ∀n > 0. ( α n , X n ∈ X n-1 & λα n+1 = λα n ) .
We denote by Play X the set of plays on X and by FPlay X the set of finite plays.

Here we focus on a general notion of (deterministic) partial strategy. Formally, strategies in our framework are partial functions on finite plays ending with a position where the player is next to move, and yielding (if any) a pair in M A × M A , consisting of "a move of the given player together with a next position" on the game X. In what follows, we denote by -FPlay LI X (FPlay RI X ) the set of possibly empty finite plays on the game X on which L (R) acts as player I, and ending with a position where the turn is

L (R), i.e. s = or s = α 1 , X 1 . . . α n , X n , where λα 1 = L (λα 1 = R) and λα n = R (λα n = L).
-FPlay LII X (FPlay RII X ) the set of finite plays on the game X on which L (R) acts as player II, and ending with a position where R (L) was last to move, i.e. s = α 1 , X 1 . . . α n , X n , where λα 1 = R (λα 1 = L) and λα n = R (λα n = L).

Formally, we define: Definition 3 (Strategies). Let X be a coalgebraic multigame. A strategy σ for LI ( i.e. L acting as player I) is a partial function σ :

FPlay LI X → M A × M A such that, for any s ∈ FPlay LI X , σ(s) = α, X =⇒ λα = L & s α, X ∈ FPlay X .
Similarly, one can define strategies for players LII, RI, RII.

For any player LI, LII, RI, RII, we define the opponent player as RII, RI, LII, LI, respectively. A counterstrategy of a strategy for a player in {LI,LII,RI,RII} is a strategy for the opponent player.

We are interested in studying the interactions of a strategy for a given player with the (counter)strategies of the opponent player. When a player plays on a game according to a strategy σ, against an opponent player who follows a (counter)strategy σ , a play arises. Formally, we define: Definition 4 (Product of Strategies). Let X be a coalgebraic multigame. (i) Let s be a play on X, and σ a strategy for a player in {LI,LII,RI,RII}. Then s is coherent with σ if, for any proper prefix s of s, ending with a position where the player is next to move, σ(s ) = α, X =⇒ s α, X is a prefix of s.

(ii) Given a strategy σ on X and a counterstrategy σ , we define the product of σ and σ , σ * σ , as the unique play coherent with both σ and σ .

Notice that a play arising from the product of strategies is alternating. We call well-founded multigames those multigames which correspond to wellfounded sets as elements of the final coalgebra M A , and non-wellfounded multigames the non-wellfounded sets in M A . Clearly, strategies on well-founded multigames generate only finite plays, while strategies on non-wellfounded multigames can generate infinite plays.

A special subclass of multigames on which we focus on in the sequel is that of polarized multigames. Such multigames have the following special structure: R starts, at any non-ending position only moves either for R or for L are available and along any path in the game graph R/L moves strictly alternate. Polarized multigames play a central rôle in the construction of our categories of multigames. Such games arise in traditional Game Semantics of Linear Logic and Programming Languages, see e.g. [START_REF] Abramsky | Full abstraction for PCF[END_REF][START_REF] Hyland | On Full Abstraction for PCF: I, II, and III[END_REF].

Multigame Operations

In this section, we show how to define various operations on multigames, including sum, negation, linear implication, and infinite sum. The crucial operation on multigames is sum, which, as we will see, is related to Conway's selective sum on traditional games, and it will give rise to a tensor product on the category of multigames defined in Section 4 below. In our coalgebraic framework, operations can be conveniently defined via final morphisms, using (some generalizations of) the standard coiteration schema. Before defining multigame operations, we start by recalling a useful generalized coiteration schema introduced in [START_REF] Cancila | Generalized Coiteration Schemata[END_REF].

Guarded Coiteration Schema

Here we recall a generalized coiteration schema based on λ-bialgebras, for λ a distributive law, which will be used in the sequel for defining multigame operations.

Definition 5 (Guarded Coiteration). Let (Ω, α Ω ) be a final coalgebra for a functor F : Set * → Set * , and let A be a set. A guarded specification for a morphism h : A → Ω is of the form:

α Ω • h = F (g • G(h)) • δ A , (1)
where δ A : A → F (GA) and g : G(Ω) → Ω are given, g is the guard. I.e. h makes the following diagram commutes:

A δ A h / / Ω α Ω F GA F (g•Gh)
/ / F Ω Under suitable conditions, the above schema admits a unique solution, see [START_REF] Cancila | Generalized Coiteration Schemata[END_REF] for more details. In particular, a functor G : Set * → Set * is required and a generalized distributive law λ : GF • → F G for which (Ω, g, α Ω ) is a λ-bialgebra.

Operations on Multigames

Sum. In the context of multigames, the following notion of sum arises naturally. On the sum multigame, at each step, the next player selects either one (nonended) or both component multigames, and makes a legal move in each of the selected components, while the component which has not been chosen (if any) remains unchanged.

Definition 6 (Sum). The sum of two multigames : M

A × M A -→ M A is defined by: X Y = { α , X Y | α, X ∈ X} ∪ { β , X Y | β, Y ∈ Y } ∪ { α + β, X Y | α, X ∈ X & β, Y ∈ Y }
, where α , β are the sets obtained from α, β by adding tags to atomic moves.

The above definition corresponds to a standard coiteration schema, namely the function is the final morphism from the coalgebra (M A × M A , f ) to the final coalgebra (M A , id), where the coalgebra morphism f :

M A × M A -→ F M A (M A × M A ) is defined by: f (X, Y ) = { α , X , Y | α, X ∈ X} ∪ { β , X, Y | β, Y ∈ Y } ∪ { α + β, X , Y | α, X ∈ X & β, Y ∈ Y } .
Remark. Notice that, in composing multigames via the sum, we keep track of the moves coming from the two different components by using tags. This definition is different from original Conway's sum on games, which is a purely set-theoretic extensional operation, possibly allowing for identifications between the two components. Our sum definition, where we keep track of the component in which each move has been performed, is necessary e.g. for extending sum to a bifunctor in categories of multigames and strategies such as that defined in Section 4 below, or even to define strategy composition in this category. Nonetheless, notice that, from a determinacy point of view, this sum and Conway's original one behave in the same way, i.e. they are equivalent w.r.t. the existence of (winning) strategies.

Negation. The negation is a unary multigame operation, which allows us to build a new game, where the rôles of L and R are exchanged. For α ∈ M A , we define α = {a | a ∈ α} .

The definition of multigame negation is as follows:

Definition 7 (Negation). The negation -: M A -→ M A is defined by:

X = { α, X | α, X ∈ X} .
Also negation is an instance of the coiteration schema. It is the final morphism from the coalgebra (M A , f -) to the final coalgebra (M A , id), where the coalgebra morphism f -:

M A -→ F M A (M A ) is defined by: f -(X) = { α, X | α, X ∈ X} .
Linear implication. Using the above notions of sum and negation, we can now define the following linear implication, which corresponds to the notion of linear implication in Linear Logic: Definition 8 (Linear Implication). The linear implication of the multigames X, Y , X Y , is defined by

X Y = X Y .
Infinite sum. We can enrich multigames with a further interesting unary coalgebraic operation, ∞ , an infinite sum: on the game ∞ x, at each step, the current player can perform a move in finitely many of the infinite components of X. Our infinite sum is related to the exponential modality defined on a category of games in [START_REF] Mellies | An explicit formula for the free exponential modality of linear logic[END_REF], and it will induce a comonad on the categories of multigames that we will consider in Section 4.

Definition 9 (Infinite Sum). We define the infinite sum ∞ : M A -→ M A by:

∞ X = { α 1 + . . . + α n , X 1 . . . X n ( ∞ X) | n ≥ 1 & α 1 , X 1 , . . . , α n , X n ∈ X & λα 1 = . . . = λα n } .
The above specification defines a unique function ∞ , since it is an instance of the guarded coiteration of Definition 5 above, where the functor G : Set * → Set * is defined by

G(A) = n≥1 (M n A × A) -the guard g : G(M A ) -→ M A is defined by g(X 1 , . . . , X n+1 ) = X 1 . . . X n+1 -the function δ M A : M A → P <κ (M A × n≥1 (M n A × M A )) is defined by δ M A (X) = {(α 1 + . . . + α n , X 1 , . . . , X n , X) | n ≥ 1 & λα 1 = . . . = λα n & (α 1 , X 1 ), . . . , (α n , X n ) ∈ X} -(M A , g, id ) is a λ-bialgebra for λ : GF • → F G distributive law defined by λ A : n≥1 (M n A × P <κ (M A × A)) → P <κ (M A × n≥1 (M n A × A)) λ A (X 1 , . . . , X n+1 ) = {(α 1 + . . . + α k , X 1 , . . . , X n+1 ) | k ≥ 1 & α 1 , X i1 ∈ X i1 , . . . , α k , X i k ∈ X i k & 1 ≤ i 1 , . . . , i k ≤ n & ∀j ∈ {1, . . . , n} \ {i 1 , . . . , i k }. X j = X j } .

Operations on Polarized Multigames

Notice that polarized multigames are not closed under the operations defined above. However, one can define corresponding sums and linear implications on polarized multigames, simply by "pruning" the graphs of the resulting multigames. A similar construction has been considered also in [START_REF] Honsell | Categories of Coalgebraic Games with Selective Sum[END_REF], in the case of games. In our setting, the pruning operation of a multigame into a polarized one can be defined as a coalgebraic operation, using a definition by mutual recursion:

Definition 10 (Pruning). Let ( ) + , ( ) -: M A -→ M A be the mutually recursive functions defined as:

(X) + = { α, (X ) -| α, X ∈ X & λα = L} (X) -= { α, (X ) + | α, X ∈ X & λα = R} .
We define the pruning operation as ( ) -.

Once we have the pruning operation, we can define polarized sums and linear implication:

Definition 11 (Polarized Operations). Let X, Y be polarized multigames. We define:

the polarized sum as the multigame (X Y ) -; the polarized linear implication as the multigame (X Y ) -; the polarized infinite sum as the multigame ( ∞ X) -.

In the following, by abuse of notation, we will use the same symbols for polarized operations and the corresponding operations on all multigames.

Categories of Multigames and Strategies

We define a monoidal closed category Y M A , whose objects are polarized multigames and whose morphisms are strategies. We work with polarized multigames, since the whole class of multigames fails to give a category, because of lack of identities, as we will see.

The main difficulty in defining this category is the definition of composition, which is based on a non-standard parallel composition of strategies. The difficulty arises from the fact that a move in a strategy between X and Y can include atomic moves on both X and Y .

A Monoidal Closed Category of Multigames. Let Y M A be the category defined by: Objects: polarized multigames. Morphisms: a morphism between multigames X and Y , σ : X Y , is a strategy for LII on X Y . Notice that in a strategy on X Y , Player R can only open in Y , but then the Player L can move in X or Y or in both components, and so on. Identity: the identity id X : X X is the copy-cat strategy. This definition works thanks to the fact that multigames are polarized, so as, on the multigame X X = (X X), R can only open on X, then L proceeds by copying the move on X and so on, at each step R has exactly one component to move in. Notice that, if the games were not polarized, then R could play on both components X and X, preventing L to apply the copy-cat strategy. Composition: strategy composition is defined as follows.

Given strategies σ : X Y and τ : Y Z, τ • σ : X Z is obtained via the swivel-chair strategy, using the terminology of [START_REF] Berlekamp | Winning Ways[END_REF] (or the copy-cat strategy, in Game Semantics terminology), and a non-standard parallel application of strategies as follows.

The opening move by R on X Z must be on Z, since multigames are polarized. Then consider the L reply given by the strategy τ on Y Z, if it exists, otherwise the whole composition is undefined. If L moves in Z, then we take this as the L move in the strategy τ • σ. If the L move according to τ is in the Y component of Y Z or in both components Y and Z, then we use the swivel chair to view the L move in the Y component as a R move in the Y component of X Y . Now, if L has a reply in X Y according to σ, then L moves in X or in Y or in both X and Y . In the first case, the L move in X together with the possible previous move by L in Z form the L reply to the opening R move. In the latter two cases, using the swivel chair, the move in Y can be viewed as a R move in the Y component of Y Z, and we go on in this way: three cases can arise. Eventually, the L multimove is all in X or in Z, or σ or τ is undefined, or the dialogue between the Y components does not stop. In the first case, the last move on X or Z, together with a possible previous move on Z or X, form the answer to the opening R move, in the latter two cases the composition is undefined. Now, in case of convergence, in order to understand how the strategy τ • σ behaves after the first pair of RL moves, it is convenient to list all situations which can arise after these initial moves, according to which player is next to move in each component. Namely, by case analysis, one can show that, after the first RL moves, the following four cases can arise:

1. X L Y R Y L Z R 2. X R Y L Y R Z R 3. X R Y L Y R Z R 4. X R Y R Y L Z R
where X L (X R ) denotes that L (R) is next to move in that component. Notice that case 1 above corresponds to the initial situation. Thus we are left to discuss the behavior of τ •σ in the other cases. In case 2, R can only open in X; this case can be dealt with similarly as the initial case 1, and after a pair of RL moves, it takes again in one of the four situations above. Cases 3 and 4 are the interesting ones, where we need to apply the strategies σ and τ in parallel, by exploiting the parallelism of multigames. These two cases are dealt with similarly. Let us consider case 3. Then R can open in Z or in X or in both components.

-If R opens in Z, then the reply of L via τ must be in Z, since, by definition of configuration 3, L cannot play in the Y component of Y Z. This will be also the reply of L in the composition τ • σ, and the final configuration coincides with configuration 3.

-If R opens in X, then the L reply given by σ can be in X, or in Y , or both in X and Y . In the first case, i.e. if the L reply is in X, this will be the reply of τ • σ, and the new configuration coincides with configuration 3. In the latter two cases, the L move in the Y component of X Y can be viewed, via the swivel chair, as a R move in Y Z. By definition of configuration 3, L can only reply in Y via τ , and, either after finitely many applications of the swivel chair the L reply via σ ends up in X, or the dialogue between the Y components goes on indefinitely, or σ or τ are undefined. In the latter two cases, the overall composition is undefined, while in the first case the L move in X will be the reply in τ • σ to the R move, and the final configuration still coincides with configuration 3.

-Finally, if R opens in X and Z, we apply the two strategies σ and τ in parallel: by the form of configuration 3, the L answer of τ must be in Z, while the L answer via σ can be either in X or in Y or both in X and Y . In this latter case, an infinite dialogue between the Y components arises (or σ or τ is undefined at some point), and hence the overall composition is undefined.

If the L reply via σ is in X, then this, together with the L reply via τ in Z, will form the L move in τ • σ, and the final configuration coincides with configuration 3 itself. If the L reply via σ is in Y , then again, either the dialogue between the Y components goes on indefinitely, or σ or τ is undefined at some point, or, after finitely many applications of the swivel chair, σ will finally provide a L move in X. This, together with the L reply via τ in Z, will form the L move in τ •σ, and the final configuration coincides with configuration 3 again.

Similarly, one can deal with case 4. This proves closure under composition of the category Y M A .

Associativity of composition can also be proven by case analysis on the polarity of the current player in the various components.

Assume

strategies σ : X Y , τ : Y Z, θ : Z W . We have to prove that θ • (τ • σ) = (θ • τ ) • σ.
Since multigames are polarized, in any of the two compositions, R can only open in W . Now, in any of the two compositions, one should consider the possible replies by L. We only discuss one case, the remaining being dealt with similarly. Assume the L reply via θ is in Z. In both compositions, we proceed to apply the swivel chair, by viewing this latter move as a R move in the Z component of Y Z. Then, in both compositions, we consider the L reply via τ . Assume L replies both in Y and in Z. At this point, the two compositions proceed differently, since in θ • (τ • σ) we first apply the swivel chair to the move in Z and we go on until we get a L answer in W , and then we apply the swivel chair to the L move in Y . In (θ • τ ) • σ, these two steps are reversed, first we apply the swivel chair to the L move in Y until we get a L reply in X, then we apply the swivel chair to the L move in Z until we get a L reply in W . The point is that these two steps, working on separate parts of the board (i.e. different components), are independent and can be exchanged. As a consequence, the behavior of θ • (τ • σ) and (θ • τ ) • σ is the same.

The multigame constructions of tensor product and linear implication can be made functorial, determining a structure of a symmetric monoidal closed category on Y M A , with the empty multigame as tensor unit. In particular, in defining the bifunctor , we proceed as follows. Let σ 1 : X 1 → Y 1 and σ 2 : X 2 → Y 2 be strategies. In order to define the strategy σ 1 + σ 2 : X 1 + X 2 → Y 1 + Y 2 , we let the two strategies σ 1 and σ 2 play in parallel. I.e. we consider R opening move: if it is in the Y 1 (Y 2 ) component, then the L answer will be given by the strategy σ 1 (σ 2 ); if the R move is both in Y 1 and Y 2 , then we apply the two strategies in parallel. We proceed in a similar way for the next moves. Clearly, for the above definition of σ 1 + σ 2 , it is essential that in the sum multigame we keep track of the components from which each move comes from. Otherwise, without tags in the moves of the sum, when e.g. Y 1 = Y 2 , we would not know on which component the R opening move on Y 1 + Y 2 comes, and then we do not know whether applying σ 1 or σ 2 . This justifies our definition of sum in Section 3.2.

Summarizing, we have:

Theorem 1. The category Y M A is symmetric monoidal closed.
Finally, one could show that the infinite sum operation ∞ induces a symmetric monoidal comonad, determining on Y M A a structure of linear category in the sense of [START_REF] Bierman | What is a categorical Model of Intuitionistic Linear Logic? TLCA'95[END_REF]. We omit the details of this construction. Notice that, contrary to traditional Game Semantics, in our coalgebraic framework this construction does not require the definition of an equivalence on strategies and a quotient operation on them in the style of [START_REF] Abramsky | Full abstraction for PCF[END_REF].

Relating Multigames to Games

In this section, we show that coalgebraic multigames are related to coalgebraic games, when a notion of parallel sum reminiscent of Conway's selective sum is considered on games, in place of disjoint sum. Here we recall the notion of coalgebraic game as it has been defined in [START_REF] Honsell | Categories of Coalgebraic Games[END_REF]:

Definition 12 (Coalgebraic Games).
-Let A be a set of atoms with functions:

(i) µ : A → N yielding the name of the move (for a set N of names), (ii) λ : A → {L, R} yielding the player who has moved. Assume A be closed under complementation. -Let F A : Set * → Set * be the functor defined by

F A (A) = P <κ (A × A)
with the usual definition on morphisms, and let (G A , id ) be the final F Acoalgebra.

A coalgebraic game is an element x of the carrier G A of the final coalgebra.

Plays and strategies are defined similarly as for multigames, see [START_REF] Honsell | Categories of Coalgebraic Games[END_REF] for more details.

The above definition of coalgebraic games generalizes Conway games and games arising in Game Semantics, see [START_REF] Honsell | Categories of Coalgebraic Games[END_REF] for more details. Following [START_REF] Conway | On Numbers and Games[END_REF], coalgebraic games can be endowed with various notions of sum, the most studied being disjoint sum, which corresponds to tensor product in standard Game Semantics. Here we focus on a notion of parallel sum inspired by Conway's selective sum, where at each step the current player can perform a move either in the first or in the second component or in both components. This notion of sum admits a straightforward definition by coiteration. As usual, one can define negation and then linear implication on games, i.e.:

Definition 13 (Selective Sum). The selective sum of two games ∨ : G

A × G A -→ G A is defined by: x ∨ y = { a , x ∨ y | a, x ∈ x} ∪ { b , x ∨ y | b, y ∈ y} ∪ { a, b , x ∨ y | a, x ∈ x & b, y ∈ y} ,
x = { a, x | a, x ∈ x} x y = x ∨ y .
Similarly as for multigames, when we restrict to polarized games, these can be endowed with a structure of symmetric monoidal category where tensor is selective sum. As in the case of multigames, also in the present case strategy composition is defined via the swivel-chair and a non-standard parallel application of strategies. We skip the details of this construction. Let call Y G A be the category so obtained.

An analogous construction has been also carried out in [START_REF] Honsell | Categories of Coalgebraic Games with Selective Sum[END_REF] in the case of coalgebraic games and total strategies, and in [START_REF] Honsell | Polarized Multigames[END_REF] for a notion of game in the [1]-style.

Categorical Correspondence

The category Y G A of games with selective sum turns out to be equivalent to the category Y M A of multigames, i.e. there exist functors S :

Y G A → Y M A and T : Y M A → Y G A , and natural isomorphisms η : G • F • → Id Y G A and η : Id Y M A • → F • G.
Namely, given a multigame X in M A , this induces a game X g , where the atomic moves are the sets of (multi)moves on the multigame X. Vice versa, given a game, x, one build a multigame x m , where each atomic move a is replaced by the singleton multimove {a}. Clearly, for any multigame X, (X g ) m is isomorphic to X, and for any game x, (x m ) g is also isomorphic to x.

This allows us to define the object part of functors S :

Y G A → Y M A and T : Y M A → Y G A .
Notice that S and T preserve tensor product on objects, up to isomorphism.

Functors S and T can be extended to strategies as follows.

For any strategy on multigames σ : X Y , we can associate a strategy σ g : X g Y g , where the plays of σ g are obtained from the plays of σ by splitting each multimove of σ containing atomic moves both in A and in B into a pair of moves on A and B, respectively. Vice versa, any strategy on games σ : x y induces a strategy on multigames σ m : x m y m , whose plays are obtained from the plays of σ by transforming each move instance of x or y into a singleton multimove, and each pair of moves a, b as the multimove {a, b}.

Summarizing, we can define functors S :

Y G A → Y M A and T : Y M A → Y G A by:
for any game x, Sx = x m , for any strategy σ : X Y , Sσ = σ m , for any multigame X, T X = X g , for any strategy σ : X Y , T σ = σ g . Then, we have:

Final Remarks and Directions for Future Work

We have introduced coalgebraic multigames, where at each step the current player performs a multimove, i.e. a (finite) set of atomic moves. Coalgebraic multigames introduce a certain level of parallelism, and they are situated halfway between traditional sequential games and concurrent games. Multigame operations are smoothly defined in our coalgebraic framework as final morphisms via (generalized) coiteration schemata. A monoidal closed category of multigames and strategies is built, where tensor is sum. The relationship between coalgebraic multigames and games is expressed in categorical terms via an equivalence between the category of multigames and a monoidal closed category of coalgebraic games where tensor is selective sum.

Here is a list of comments and directions for future work.

-Total strategies. In this paper, coalgebraic (multi)games are endowed with a notion of partial strategy, whereby the given player can possibly refuse to provide an answer and give up the game. Alternatively, one could consider notions of total strategies, in the line of [START_REF] Honsell | Conway Games, algebraically and coalgebraically[END_REF][START_REF] Honsell | Categories of Coalgebraic Games[END_REF][START_REF] Honsell | Categories of Coalgebraic Games with Selective Sum[END_REF], where the player is forced to give an answer, if there exists any. On total strategies one can then define the notion of winning/non-losing strategy for a player, if it generates winning/non-losing plays against any possible counterstrategy. A finite play is taken to be winning for the player who performs the last move, while infinite plays are taken to be winning for L/R or draws. In order to formalize winning/non-losing strategies, one shall introduce a payoff function on plays, and enrich the notion of multigame with a payoff. We claim that the results of the present paper can be rephrased also in the context of total strategies. -Other notions of sum. In [START_REF] Conway | On Numbers and Games[END_REF], Chapter 14 "How to Play Several Games at Once in a Dozen Different Ways", Conway introduces a number of different ways in which games can be played. Apart from disjunctive and selective sum, Conway defines the conjunctive sum, where at each step the current player makes a move in each (non-ended) component. A first attempt to extend Joyal's categorical construction to conjunctive sum fails, even in the case of polarized games, since trivially copy-cat strategies do not work. Alternative approaches are called for. -Semantics of concurrency. In the literature, notions of concurrent games [START_REF] Abramsky | Concurrent games and full completeness[END_REF], asynchronous games [START_REF] Mellies | Asynchronous games 2: the true concurrency of innocence[END_REF], and distributed games [START_REF] Ghica | On the compositionality of round abstraction[END_REF][START_REF] Rideau | Concurrent Strategies[END_REF][START_REF] Clairambault | The winning ways of concurrent games[END_REF] have been introduced as concurrent extensions of traditional games. Our categories of coalgebraic multigames and coalgebraic games with selective sum are more in the traditional line, but nonetheless, they reflect a form of parallelism.

Namely, in [START_REF] Honsell | Polarized Multigames[END_REF] it has been shown that, in the context of functional languages, categories of multigames in the style of [START_REF] Abramsky | Full abstraction for PCF[END_REF] accommodate parallel or. It would be interesting to explore to what extent multigames can be used for modeling concurrent and distributed languages, possibly featuring true concurrency. This would require an extension of our approach in order to account also for interference between moves/events. -Relating multigames to domains. Since multigames introduce a level of parallelism, and as it is shown in [START_REF] Honsell | Polarized Multigames[END_REF], they accommodate for e.g. parallel or in functional programming, one may expect a tighter connection between multigames and traditional denotational semantics based on domains.

  where a , b are obtained from a, b by adding suitable tags, and a, b denotes the pairing of the moves a, b (we assume the set of moves to be closed under pairing).

Theorem 2 .

 2 The functors S : Y G A → Y M A and T : Y M A → Y G A are monoidal, and they give an equivalence between the categories Y G A and Y M A .

We recall that the hereditary cardinal of a set is the cardinality of its transitive closure, namely the cardinality of the downward membership tree which has the given set as its root.

The final coalgebra of the powerset functor exists since the powerset functor is bounded by κ.


Baltasar Trancón
email: baltasar.trancon@tu-ilmenau.de

Widemann

Towards Systematic Construction of Temporal Logics for Dynamical Systems via Coalgebra

Temporal logics are an obvious high-level descriptive companion formalism to dynamical systems which model behavior as deterministic evolution of state over time. A wide variety of distinct temporal logics applicable to dynamical systems exists, and each candidate has its own pragmatic justification. Here, a systematic approach to the construction of temporal logics for dynamical systems is proposed: Firstly, it is noted that dynamical systems can be seen as coalgebras in various ways. Secondly, a straightforward standard construction of modal logics out of coalgebras, namely Moss's coalgebraic logic, is applied. Lastly, the resulting systems are characterized with respect to the temporal properties they express.

Introduction

Dynamical systems are the classical constructive formalism for behaviour arising from the deterministic evolution of system state over time [START_REF] Birkhoff | Dynamical Systems[END_REF], dating back to the works of Newton and Laplace. Clearly temporal logics, with operators such as 'next', 'always', 'eventually' and 'for-at-least', constitute a companion descriptive formalism. However, the relation is not one-to-one: One the one hand, there is a unifying theory underlying the various perspectives on dynamical systems as monoid actions, which uniformly covers discrete and continuous, as well as hybrid systems [START_REF] Jacobs | Object-oriented hybrid systems of coalgebras plus monoid actions[END_REF]. But on the other hand, the diversity of temporal logics in literature is immense, see [START_REF] Venema | Temporal Logic[END_REF], and the choice for a particular system is often justified by ad-hoc pragmatic arguments. The present article explores a potentially systematic approach to the construction of temporal logics for dynamical systems, via the relatively recent mathematical field of universal coalgebra which has been shown to be intimately connected to both dynamical systems [START_REF] Rutten | Universal coalgebra: a theory of systems[END_REF] and modal logics [START_REF] Cîrstea | Modal Logics are Coalgebraic[END_REF]. A different approach, also based on coalgebras and the Stone duality, has been suggested [START_REF] Bonsangue | Duality for Logics of Transition Systems[END_REF] for constructing modal logics of transition systems, a close relative of dynamical systems from theoretical computer science.

The method outlined in the remainder of this article, while theoretically simple, touches on many different fields of mathematics: order theory, category theory, algebra, coalgebra, classical modal logics à la Kripke, and coalgebraic logics à la Moss [START_REF] Moss | Coalgebraic Logic[END_REF]. Thus a significant fraction of this paper is dedicated to reviewing the relevant definitions and propositions from the respective standard literature. This review makes up the sections 2 and 3. The expert reader is encouraged to skip ahead: Section 4 ties up all the loose ends and gives a novel contribution. There a selection of obvious coalgebraic perspectives on dynamical systems is explored, and the respective logics entailed by applying Moss's construction are characterized.

Review: Classical Ingredients

This section reviews some basic definitions and propositions.

Order Relations

We assume that the reader is familiar with basic order-theoretic properties of binary relations, namely with reflexive, transitive, symmetric relations, and with preorders, partial orders and equivalences. We give two additional related definitions that are not quite as universal:

Definition 1 (Non-Branching & Linear Relations). Let X be a set. A binary relation R ⊆ X 2 is called
non-branching if and only if x R y and x R z imply y R z or z R y, and linear if and only if x R y or y R x, respectively, for all x, y, z ∈ X. Clearly, every linear relation is non-branching.

Monoids

We assume that the reader is familiar with the notions of a monoid M = (M, 0, +), and of monoid generators. We recall that every monoid induces an ordering relation: Definition 2 (Monoid Order). Let M = (M, 0, +) be a monoid. For any elements a, b ∈ M , we write a ≤ M b if and only if there is some c ∈ M such that a + c = b. We say that a ≤ M b via c. It follows directly from the monoid axioms that ≤ M is reflexive and transitive, and hence a preorder. By extension, M itself is called symmetric/non-branching/linear if and only if ≤ M is symmetric/nonbranching/linear, respectively.

Note that being symmetric in this sense is different from being Abelian. In fact, symmetry characterizes a famous subclass of monoids, namely the groups:

Lemma 1 (Groups). A monoid M is a group if and only if it is symmetric.

Every symmetric monoid is trivially linear, with the degenerate order (≤ M ) = M 2 , the full relation.

The proof of this simple but non-standard proposition is left as an exercise to the reader.

Dynamical Systems

Definition 3 (Dynamical System). Let T = (T, 0, +) be a monoid called time (durations). A dynamical system is an enriched structure S = (T, S, Φ) with a set S called state space, and a map Φ : S × T → S called dynamics, such that Dynamical systems are a fundamental model class of many natural and social sciences. In comparison with their younger counterparts in computer science, automata and transition systems, dynamical systems are typically behaviourally weaker; deterministic, non-pointed (without distinguished initial states) and total (without spontaneous termination), but structurally stronger; with additional features of time (density, completeness) and state space (topology, metric, differential geometry, measures).

Φ(s, 0) = s Φ Φ(s, t), u = Φ(s, t + u)
Automata-like constructions can be emulated by dynamical systems; see Example 1 below.

Definition 4 (Step, Trajectory & Orbit).

From the dynamics map Φ we may derive three forms of secondary maps:

Φ t : S → S Φ s : T → S Φ • : S → PS Φ t (s) = Φ(s, t) Φ s (t) = Φ(s, t) Φ • (s) = Img(Φ s ) = {Φ(s, t) | t ∈ T } -Φ t is

Propositional Modal Logics

We assume that the reader is familiar with the syntax and semantics of classical propositional logics and their presentation solely in terms of the connectives ¬ and →. For the modal extensions, see [START_REF]Handbook of Modal Logic[END_REF] or some other textbook.

Definition 5 (Syntax of Propositional Modal Logics). The modal extension of classical propositional logics adds two unary connectives and ♦, taking as primitive and defining

♦A = ¬ ¬A

Definition 6 (Semantics of Propositional Modal Logics). A normal modal extension of classical propositional logics adds at least the deduction rule of necessitation or generalization, and the axiom of distribution:

A A (A → B) → ( A → B)
Example 2. Important normal modal logics are obtained by adding certain axioms:

-A → A added to the minimal system results in the logic T .

-A → A added to T results in the logic S4.

-( A → B) ∨ ( B → A) added to S4 results in the logic S4.3. -♦A → ♦A added to S4 or S4.3 results in the logic S5.

Kripke Semantics Definition 7 (Kripke Frame).

A Kripke frame is a structure (W, R) with a set W of worlds and a binary relation R on W called accessibility. Definition 8 (Kripke Model). Let (W, R) be a Kripke frame. A Kripke model (of propositional modal logic) is an extended structure (W, R, ), where is a relation between W and the language Form of logical formulas, such that:

w ¬A ⇐⇒ w A w A → B ⇐⇒ w A implies w B w A ⇐⇒ v A whenever w R v
We say that w satisfies A in (W, R, ) if and only if w A.

Lemma 3. The satisfaction relation of a Kripke model is determined uniquely by the satisfaction of atomic propositions.

Definition 9 (Validity). A formula

A is called valid in -a Kripke model (W, R, ) if

Review: Non-Classical Ingredients

This section briefly reviews some definitions and propositions from categorial coalgebra and coalgebraic logics. See [START_REF] Rutten | Universal coalgebra: a theory of systems[END_REF] and [START_REF] Kupke | Coalgebraic semantics of modal logics: An overview[END_REF][START_REF] Moss | Coalgebraic Logic[END_REF], respectively, for full details.

Category Theory

We assume that the reader is familiar with basic endofunctors on the category Set, in particular the identical functor Id, the constant functor Const(C) for any object C, the covariant Hom-functors and the covariant powerset functor P. All functors considered in the following are tacitly Set-endofunctors.

F ω X = {F Y | Y ⊆ X ∧ Y finite} F ω (h : X → Y ) = F h| FωX
Relation liftings for functors are conventionally defined in terms of span diagrams, but a pointwise notation will be more convenient for the following discussions:

Definition 13 (Relation Lifting). Let F be a functor. Every relation R ⊆ X × Y has a lifting F [R] ⊆ F X × F Y
defined as the set of pairs (x, ŷ) for which there is some r ∈ F R such that (F π 1 )(r) = x and (F π 2 )(r) = ŷ.

Universal Coalgebra

We assume that the reader is familiar with the notion of F -coalgebras for a functor F , their associated homomorphisms, F -bisimulations and F -bisimilarity.

Definition 14 (Parallel Coalgebra Composition).

Coalgebras with the same carrier can be combined in parallel: Let (X, f ) be an F -coalgebra and (X, g) be a G-coalgebra. Then (X, f, g ) is an (F × G)-coalgebra, where f, g (x) = f (x), g(x)

Moss's Coalgebraic Logic

The idea of Moss's coalgebraic logic [START_REF] Moss | Coalgebraic Logic[END_REF] is to replace Kripe frames by F -coalgebras for some functor F , and to derive a universal and natural modality from F itself: Definition 15 (Moss's Coalgebraic Logic, Abstractly). Fix a standard functor F . Extend the syntax of propositional logic by a pseudo-unary connective ∇ that, unlike the classical modalities like , applies not to a single formula A ∈ Form but to an expression of type either A ∈ F (Form) or A ∈ F ω (Form). For infinitary F where the choice makes a difference, the cases are called infinitary and finitary F -coalgebraic logics, respectively. A Moss model is a structure (X, f, ) where (X, f ) is an F -coalgebra and is a relation between coalgebra states and formulas, such that

x ¬A ⇐⇒ x A x A → B ⇐⇒ x A implies x B
as for Kripke models, but

x ∇ A ⇐⇒ f (x) F [ ] A
Moss's coalgebraic logic as presented here specifies satisfaction only up to atomic propositions, in analogy to Kripke frames. In Moss's original presentation, the specification is unique, in analogy to Kripke models: Definition 16 (Moss's Coalgebraic Logic, Concretely). Let (X, f ) be an F -coalgebra. Let s : X → P(Prop) be the map that assigns to each state x ∈ X the desired set of valid atomic propositions. Then (X, s) is a Const P(Prop)coalgebra. For the parallel composite coalgebra (X, g = f, s ), a unique Moss model is specified by the additional clause

x A ⇐⇒ A ∈ s(x) (A ∈ Prop)
The following two propositions state that traditional Kripke frames are essentially equivalent to the special case F = P: Lemma 4. P-coalgebras (X, f ) are in one-to-one correspondence to relations R on X by putting x R y if and only if y ∈ f (x). Theorem 3. The Kripke modalities , ♦ and the Moss modality ∇ for finitary P-coalgebraic logics are equivalent. For infinitary P-coalgebraic logics, they are also equivalent in the presence of infinitary conjunction and disjunction; otherwise ∇ is generally more expressive.

w K A ⇐⇒ w M ∇{A} ∨ ∇∅ w K ♦A ⇐⇒ w M ∇{A, } w M ∇ A ⇐⇒ w K A ∧ ♦ A where ♦ A = {♦B | B ∈ A}
where K / M denote satisfaction à la Kripke/Moss, respectively.

In general, the infinitary version of the operator ∇ is better matched with a logic where conjunction and disjunction are also infinitary. While an uncommon topic classically, infinitary logics are an important topic in modal logic because of their connection to bisimulations; they always satisfy the Henessy-Milner property:

Theorem 4 (Expressivity). In any fully (∧, ∨, ∇)-infinitary F -coalgebraic logic, two states s, t ∈ S satisfy the same set of formulas if and only if they are bisimilar.

Generally finitary logics are nicer to work with, and of course more likely to be decidable. See example 5 below for popular temporal operators that are not finitary in this framework.

Constructions

This section gives novel theoretical results by investigating the ramifications of the following recipe:

1. Identify some generic F -coalgebraic view on dynamical systems; 2. use Moss's construction to obtain logics with ∇ F modality, depending on the functor F ; 3. relate ∇ F to established temporal logic operators.

Note that all of the following constructions have the state space S of a fixed dynamical system as the carrier of some coalgebra for various standard functors. Hence the associated logical languages can coexist naturally in a single system, by the parallel composition given in Definition 14.

Step Logics

Definition 17 (Step Coalgebra). Let S = (T, S, Φ) be a dynamical system. For any element t ∈ T , the Id-coalgebra (S, Φ t ) is called the t-step coalgebra of S.

Definition 18 (Multistep Coalgebra).

Let S = (T, S, Φ) be a dynamical system. For any subset U ⊆ T , the Hom(U, -)-coalgebra (S, s → Φ s • in), given the inclusion map in : U → T , is called the U -multistep coalgebra of S.

Lemma 5. The ∇ modality of step coalgebras amounts to

for the t-step: s ∇A ⇐⇒ Φ(s, t) A for the U -multistep:

s ∇ A ⇐⇒ Φ(s, t) A(t) for all t ∈ U
The functors for t-steps and finite U -multisteps are finitary; hence no additional distinction between finitary and infinitary logics arises.

Definition 19 (Step Modality). We define the temporal modality , with the intuitive meaning next, in terms of ∇.

A = ∇A t A = ∇u → A (t = u) (t = u) Example 4. (Multi-)
Step coalgebras are of particular interest for finite generators, since they specify the dynamics uniquely and concisely. The following are generating in the sense of Example 1:

-For time (N, 0, +), the 1-step coalgebra maps every state to its successor. The resulting temporal logic has as the next operator of traditional unidirectional discrete-time temporal logic.

-For time (Z, 0, +), the (±1)-multistep coalgebra maps every state to its successor/predecessor, respectively. The resulting temporal logic has ±1 as the next/previously operators of traditional bidirectional discrete-time temporal logic, respectively. -For "time" (Σ * , ε, •), the Σ-multistep coalgebra maps every automaton state to its response function (row of the transition table). The resulting logic has ( a ) a∈Σ as the generating cases of Pratt's necessity operators [a] in dynamic logic [START_REF] Pratt | Semantical Considerations on Floyd-Hoare Logic[END_REF], where they are extended to the free Kleene algebra over Σ.

Interesting infinite, non-generating examples include:

-For time (R, 0, +) and δ > 0, let U denote the open interval (-δ, δ). The U -multistep coalgebra maps every state to its temporal δ-neighbourhood.

Step generators benefit from Moss's Expressivity Theorem 4:

Corollary 3. The modality ∇ and the family of modalities ( t ) t∈U for generating U are straightforwardly equivalent if U is finite, and equivalent in the presence of infinitary conjunction otherwise.

x ∇ A ⇐⇒ x t∈U t A(t)
The following construction is the multistep limit case U = T .

Trajectory Logics

Definition 20 (Trajectory Coalgebra). Let S = (T, S, Φ) be a dynamical system. The Hom(T, -)-coalgebra (S, s → Φ s ) is called the trajectory coalgebra of S.

Lemma 6. The ∇ modality of trajectory coalgebras amounts to

s ∇ A ⇐⇒ Φ(s, t) A(t) for all t ∈ T
The ∇ trajectory modality is a surprisingly powerful logical operator, with the severe disadvantage that there is no canonical syntactic representation. The following examples are but a small subset of useful special cases:

Example 5. Arguments of the ∇ trajectory modality are maps of type T → Form. Various intensional notations for such maps, or time-dependent formulas, give rise to well-known temporal operators. Note that all following examples work for finitary ∇.

-Consider discrete time (N, 0, +) or (Z, 0, +). Define a zip operator

A B = ∇t → A t even B t odd
Then a dynamic system is bipartite, with characteristic formula A, if and only if (A ¬A) ∨ (¬A A) is valid in the Moss model associated with its trajectories.

-Consider automaton time (Σ * , ε, •). Define a consumption operator

eat(L, A, B) = ∇t → A t ∈ L B t ∈ L
for languages L ⊆ Σ * and formulas A, B. Now let A be a formula characterizing accepting states. Then an automaton, as a dynamical system, accepts at least/exactly the language L ⊆ Σ * if and only if eat(L, A, )/eat(L, A, ¬A), respectively, is valid for its initial state(s) in the Moss model associated with its trajectories. -Consider time with a linear antisymmetric order <. Define a change operator

chg(t, A, B, C) = ∇u →      A u < t B u = t C u > t
for time duration t and formulas A, B, C. Then minimum/maximum-duration operators can be defined directly, in two variants differing in the inclusion of boundary cases:

min t. A = chg(t, A, , ) max t. A = chg(t, , , ¬A) min t. A = chg(t, A, A, ) max t. A = chg(t, , ¬A, ¬A)
Imprecise operators such as until can be expressed as infinitary disjunctions:

A U B = t∈T chg(t, A, B, )

Orbit Logics

The following construction shifts the coalgebraic focus from trajectories to orbits which are images of trajectories, hence abstracting from durations. The result is a family of qualitative temporal logics that can be expressed naturally in the classical modal operators, uniformly for all kinds of time structure:

Definition 21 (Orbit Coalgebra). Let S = (T, S, Φ) be a dynamical system. The P-coalgebra (S, Φ Proof.

1. Reflexivity and transitivity follow directly from the monoid axioms: x S x via 0, and if x S y via t and y S z via u, then x S z via t + u. 2. Assume that x S y via t and x S z via u. By linearity of T assume, without loss of generality, that t ≤ T u via v. Then y S z via v. 3. For symmetric T, if x S y via t, then y S x via -t.

The caveat in case 2 of this proposition is necessary:

Example 6 (Nonlinear Linear-Time Dynamical System). Set T = {0}, giving rise to the singleton monoid which is trivially linear. This fixes Φ completely as Φ(s, t) = Φ(s, 0) = s, giving rise to a "still-life" structure of time. Then neither x S y nor y S x for x = y. Proof. Construct a dynamical system S = (T, S, Φ) with ( S ) = R. In any case, clearly S = W . Proceed in reverse order and increasing flexibility of cases. For the latter two, consider the partition of W into strongly connected components (sccs) of the preorder R: nonempty, maximal subsets C ⊆ W such that x R y for all x, y ∈ C. We write x ∼ y if and only if x, y are in the same scc, that is x R y and y R x.

Definition 22 (Orbital Frame

3. Set T = (Z, 0, +). By symmetry of R there are no related pairs across sccs.

For each scc C choose an arbitrary cyclic permutation. Set Φ 1 to their union. Then x S y via some i < k, where k is the size of the scc containing both, if x R y, and otherwise x S y. 2. Set T = (N, 0, +). We say that y is a successor of x, writing x y, if and only if x R y but not y R x. Clearly, x R y if and only if either x ∼ y or x y, exclusively. We say that x is transient if it has successors. Since W is finite and R is non-branching, every transient x has a unique scc of least successors, from which we may choose one, say x , and all elements reachable from x are successors. Set Φ 1 (x) = x . For non-transient x, all elements reachable from x are in the same scc. Proceed as above. Then x S y via some i < k, where k is the number of successors of x, if x y, x S y via some i < k, where k is the size of the scc containing both, if

x ∼ y, and otherwise x S y. 1. There are in general no least successors, and there may be non-successors reachable from transient elements. A more basic construction is needed: Set T = (N * , ε, •), the free monoid over N. For each x ∈ W choose some infinite sequence y = (y 0 , y where R is an arbitrary/non-branching/symmetric preorder, respectively, and have the finite frame property. By Lemma 9, they are also complete for the subclasses of arbitrary/linear-time/invertible orbital frames, respectively.

Example 7. The operators and ♦ are well-suited to express "long-term" behavioral properties of dynamical systems. For instance, let A be the characteristic formula of a subset U ⊆ S of the state space. Then U is a stationary solution of a dynamical system if and only if A → A is valid in the Moss model associated with its orbits.

Conclusion and Outlook

Many operators discussed in the temporal logic literature can be subsumed under a common framework by viewing them as instances of Moss's modality ∇, for some coalgebraic presentation of the underlying dynamical system models. As a rule of thumb, -step coalgebras go with discrete time, -trajectory coalgebras go with quantitative operators for either discrete or dense time, and orbit coalgebras go with arbitrary time and qualitative operators, in particular the classical modal operators and the framework of normal modal logics.

The examples given in this article are of course only a small selection to prove the viability of the approach. There is considerable potential for generalization. The trajectory modality is an extremely expressive tool, and it is likely that many other temporal operators can be shown to coincide with particular intensional notations for it. Besides, coalgebraic perspectives on dynamical systems other than the three detailed above could be considered. An interesting open problem and direction for future research is the integration of measure-theoretic temporal operators, for instance in duration calculus [START_REF] Chaochen | A Calculus of Durations[END_REF], into the framework.

Coalgebraic modal logics from predicate liftings [START_REF] Pattinson | Expressivity Results in the Modal Logic of Coalgebras[END_REF] are an alternative to Moss's logic, with somewhat different properties. A study of the predicate liftings arising from the functorial perspective on dynamical systems is expected provide some interesting additional insights.

Recently, some progress has been made in the use of non-standard analysis to clarify the relationship of discrete-time and continuous-time systems, in a way that is compatible with a coalgebraic perspective [START_REF] Suenaga | Hyperstream processing systems: nonstandard modeling of continuous-time signals[END_REF]. That approach might also be helpful in bridging the gap between our trajectory and orbit logics.

Example 3 .

 3 The liftings for some basic functors are as follows: -The identical functor lift a relation to itself: x Id[R] y if and only if x R y. -A constant functor lifts to the identical relation: c Const(C)[R] d if and only if c = d. -Y P[R] Z if and only if for all y ∈ Y there is a z ∈ Z, and vice versa, such that y R z. f Hom(C, -)[R] g if and only if f (c) R g(c) for all c ∈ C.

Corollary 2 (Generating Steps). If

  called the step of duration t, or just the t-step. -Φ s is called the trajectory of initial state s. -Φ • (s) is called the orbit of state s. G ⊆ T generates the monoid T, then Φ is determined uniquely by the collection of steps (Φ t ) t∈G .

	Example 1 (Instances of Time).
	-The time monoid (N, 0, +) yields standard non-invertible, linear-time, discrete-
	time dynamical systems. The step Φ 1 is generating. Trajectories are (one-
	sided) infinite sequences.
	-The time monoid (Z, 0, +) yields standard invertible, hence linear-time,
	discrete-time dynamical systems. The step Φ 1 is generating and must be
	invertible. Trajectories are two-sided infinite sequences.
	-The time monoid (R + , 0, +) yields standard non-invertible, linear-time,
	continuous-time dynamical systems. No finite step generator collection exists.
	Trajectories are one-sided parametric curves.
	-The time monoid (R, 0, +) yields standard invertible, hence linear-time,
	continuous-time dynamical systems. No finite step generator exists; clas-
	sically definitions are given as solutions to ordinary differential equations.
	Trajectories are two-sided parametric curves.
	-The free "time" monoid (Σ * , ε, •) over some finite alphabet Σ yields total
	semiautomata, or deterministic finitely-labelled transition systems. The steps
	{Φ
	Lemma 2 (Homomorphic Steps). The dynamical systems with time T are
	precisely those systems (T, S, Φ) such that the step construction is a monoid
	homomorphism from T into the monoid of maps of type S → S with right
	composition.
	Φ 0 = id S	Φ t+u = Φ u • Φ t

a | a ∈ Σ} (columns of the transition table) are generating. Trajectories are big-step transition functions of total automata, mapping input words to final states.

  • ) is called the orbit coalgebra of S. We say that in S, y is reachable from x, written x S y, if and only if y ∈ Φ • (x). More precisely, we say x S y via t, if and only if y = Φ t (x).Clearly, x S y if and only if there is some witness t ∈ T such that x S y via t.

	Lemma 7. For dynamical systems S, the reachability relation S is
	1. always a preorder,
	2. additionally non-branching, but not generally linear, if S is linear-time, and
	3. additionally symmetric if S is invertible.

  ). A Kripke frame is called orbital if and only if it corresponds, in the sense of Lemma 4, to the orbit coalgebra of some dynamical system. An orbital frame is called linear-time/invertible if and only if it corresponds to the orbit coalgebra of some linear-time/invertible dynamical system, respectively.This statement has a partial, finitary converse, which is by far the most technical result of the present paper:

	Lemma 9. A finite Kripke frame (W, R) is
	1. always orbital if R is a preorder,
	2. additionally linear-time if R is non-branching,
	3. additionally invertible if R is symmetric.
	Using this definition, Lemma 7 extends to Kripke frames:
	Lemma 8. For any orbital Kripke frame F = (W, R), the relation R is
	1. always a preorder,
	2. additionally non-branching if F is linear-time,
	3. additionally symmetric if F is invertible.

  1 , . . . ) ∈ W ω such that x R z if and only if z = y i for some i. This is always possible by invocation of countable choice, since the set {z | x R z} is finite and nonempty. For the generating steps {Φ n | n ∈ N}, set Φ n (x) = y n . Then x S y via 1, if x R y, and otherwise x S y.

	Proof. S4/S4.3/S5 are sound for the class of Kripke frames (W, R) where R
	is an arbitrary/non-branching/symmetric preorder, respectively. By Lemma 8,
	they are also sound for the subclasses of arbitrary/linear-time/invertible orbital
	frames, respectively.
	Conversely, S4/4.3/S5 are complete for the class of Kripke frames (W, R)
	Theorem 5. The modal logics S4/S4.3/S5 are sound and complete for arbi-
	trary/linear-time/invertible orbital frames, respectively.