Dylan Bellier

Sophie Pinchinat

François Schwarzentruber

Dependency Matrices for Multiplayer Strategic Dependencies

Keywords: 2012 ACM Subject Classification Theory of computation → Modal and temporal logics, Theory of computation → Logic and verification, Theory Temporal dependency, Delay games, Strategic reasoning, Temporal logic Digital Object Identifier 10.4230/LIPIcs.FSTTCS.2022.31

In multi-player games, players take their decisions on the basis of their knowledge about what other players have done, or currently do, or even, in some cases, will do. An ability to reason in games with temporal dependencies between players' decisions is a challenging topic, in particular because it involves imperfect information. In this work, we propose a theoretical framework based on dependency matrices that includes many instances of strategic dependencies in multi-player imperfect information games. For our framework to be well-defined, we get inspiration from quantified lineartime logic where each player has to label the timeline with truth values of the propositional variable she owns. We study the problem of the existence of a winning strategy for a coalition of players, show it is undecidable in general, and exhibit an interesting subclass of dependency matrices that makes the problem decidable: the class of perfect-information dependency matrices.

Introduction

In perfect-information multi-player games, decisions of players depend on their knowledge about what other players have done so far. This setting is adopted in various logics for strategic reasoning such as Alternating-time Temporal Logics [START_REF] Alur | Alternating-time temporal logic[END_REF] and Strategy Logic [START_REF] Chatterjee | Strategy logic[END_REF]. A strategy for a player assigns to each history the next action to play. In imperfect-information games, a player may have partial knowledge about what other players did, enforcing her strategy to depend only on her knowledge about the current history.

However, there are situations where dependencies involve the knowledge about the future of a play. For instance, Grove and Clarkson in [START_REF] Grove | Online bin packing with lookahead[END_REF] developed an online algorithm for the bin packing problem with a look-ahead that takes advantage of information on some future items. Look-ahead also exists in parsing: for LL(1) (for Left to right, Leftmost derivation) grammars, the production rule to be chosen depends on the next symbol in the read word [START_REF] Aho | Compilers: Principles, Techniques, and Tools. Addison-Wesley series in computer science / World student series edition[END_REF]. The extreme case occurs when the decisions depend on the entire future of the play. This is the case for offline algorithms, where the future is finite (for bin packing it is given by the sequence of all incoming items). It also appears for an infinite future, such as in Quantified Propositional Linear-time Temporal Logic (QPTL) [START_REF] Prasad Sistla | The complementation problem for Büchi automata with applications to temporal logic[END_REF]: for a formula ∀a∃bφ, the choice of the truth values of proposition b depends on all those of proposition a.

In addition, players may experience delays to receive information. For instance, a proponent may have to play without having received yet information about the last three moves of her opponent. Klein et al. in [START_REF] Klein | What are strategies in delay games? borel determinacy for games with lookahead[END_REF] formalized delay games as an extension of Gale-Stewart games [START_REF] Gale | Infinite games with perfect information[END_REF], i.e. two player infinite games with perfect information.

Our paper proposes a unifying theoretical framework to specify dependencies. To this aim, we define the notion of a dependency matrix D. The entry D[a, b] is a generalized integer (i.e. in Z ∪ {-∞, +∞}) so that "Player a's decision at time-step t current depends on Player b's decisions up to time-step

t current + D[a, b]".
The semantics of a dependency matrix relies on an involved machinery based on an imperfectinformation multi-player game, called the meta game. The positions of the game, called configurations, are all the possible partial labelings of the timeline by the players -and are thus in infinite number. The dynamics of the meta game is involved because the dependencies may desynchronize players in their choices for labeling a time point.

Moreover, some matrices encode circular dependencies between players, leading to deadlocked situations where none of the players can progress anymore in the meta game, preventing them from completing their labeling of the timeline. Upon the study of this phenomenon, we introduce the class of progressing matrices, that guarantee that any play in the meta arena provides a full labeling of the timeline for each propositional variable. We establish an effective property that characterizes these matrices. Thus, plays can be qualified as winning or losing according to some linear-time formula, here an LTL formula.

We then study the problem called EWS (Existence of Winning Strategies) of deciding, given a dependency matrix, a coalition (subset of players) and an LTL formula, the existence of a joint strategy for the coalition such that any play brought about by this strategy satisfies the LTL formula. Importantly, the imperfect-information feature of the meta game addresses two issues: first, this game is not determined in general, and second, winning strategies for the coalition need being uniform, a non-trivial notion in our rich setting since players may be desynchronized.

Although we prove that EWS is unsurprisingly undecidable, we exhibit the subclass of so-called perfect information dependency matrices for which EWS turns to a decidable problem. We first consider the perfect information property for matrices whose values range over Z and show how EWS can be reduced to solving a two-player perfect-information parity game, yielding a 2-Exptime-complete complexity. We then generalize the perfect-information property to arbitrary matrices and provide a decision procedure for EWS that generalizes the one for QPTL [START_REF] Prasad Sistla | The complementation problem for Büchi automata with applications to temporal logic[END_REF], thus a non-elementary complexity.

To our knowledge, our proposal offers the first framework amenable for merging many, and yet remote, game settings such as concurrent or turn-based games [START_REF] Alur | Alternating-time temporal logic[END_REF], (two-player) delay games [START_REF] Klein | What are strategies in delay games? borel determinacy for games with lookahead[END_REF][START_REF] Klein | How much lookahead is needed to win infinite games?[END_REF][START_REF] Thomas | Degrees of lookahead in regular infinite games[END_REF], logic QPTL [START_REF] Prasad Sistla | The complementation problem for Büchi automata with applications to temporal logic[END_REF], and Church Synthesis Problem (see the survey [START_REF] Finkbeiner | Synthesis of reactive systems[END_REF]) -it can be shown that our framework also subsumes DQBF (Dependency Quantified Boolean Formulae) [START_REF] Peterson | Lower bounds for multiplayer noncooperative games of incomplete information[END_REF].

Outline. In Section 2, we define dependency matrices, and show that they embed several settings of games. Section 3 contains the necessary background. In Section 4, we present the formal machinery to define an arena specified by a dependency matrix. In Section 5, we address the problem EWS of the existence of winning strategies and show its undecidability in the general case. Next, in Section 6, we design the decision procedure for EWS when restricted to a perfect-information matrix input. We conclude our contribution in Section 7.

Dependency Matrices and Examples

In this section, we propose the generic notion of dependency matrix and show that it subsumes several classic settings in games. We denote players by lowercase letters such as a, b, c, etc. A dependency matrix specifies the mutual dependencies between players' decisions in a game where each player owns an atomic proposition and aims at filling the whole timeline with a valuation for it at each time point. Formally, On the contrary, when D[a, b] ≥ 0, Player a's decision at t depends on some Player b's decisions up to some time point after t, so that Player a is not able to make her decision without this required information. In particular, if D[a, b] = +∞, Player a's decisions do depend on the decisions of Player b's over all the timeline.

▶
Because it is natural to consider that a player is aware of her own decisions so far, values on the diagonal D[a, a] are irrelevant and are left undefined. As such, the matrix line D[a, .] specifies the dependencies of Player a with respect to all other players, and her ability to make a decision is constrained by all these dependencies. Unsurprisingly, some matrices may yield blocking situations for some players, an issue that we address in the sequel.

Beforehand, we illustrate how several settings in games can be captured with matrices.

▶ Example 2 (Concurrent Game). In a standard concurrent game (as in logics ATL, ATL*), players have to concurrently choose a move. Thus the move of one player can only depend on the strict past of the history of moves. The corresponding matrix for 3 players is D 1 , where strict past is reflected by the value -1.

D 1 =   a b c a • -1 -1 b -1 • -1 c -1 -1 •   ▶ Example 3 (Round Robin Game).
In a Round Robin game, players play in turn: first Player a, then b, then c. The matrix is D 2 : decisions of Player a depend on the strict past, hence the values -1 in the a-row; decisions of b depend on the non-strict past of a (hence the value 0), and the strict past of c (hence the value -1); decisions of c depend on the non-strict past of the other players.

D 2 =   a b c a • -1 -1 b 0 • -1 c 0 0 •   F S T T C S
D 3 =   a b c a • -∞ -∞ b +∞ • -∞ c +∞ +∞ •   ▶ Example 5 (Church Synthesis).
The Church Synthesis problem (see the survey [START_REF] Finkbeiner | Synthesis of reactive systems[END_REF]) consists in responding to a stream of inputs by a stream of outputs, so that a given property holds.

D 4 =     a b c d a • -1 -1 -1 b -1 • -1 -1 c 0 0 • -1 d 0 0 -1 •    
▶ Example 6 (Fixed Delay games). A delay game is a two-player game, say between Player a and Player b. Player a must make a given finite number k of moves beforehand and then, Players a and b play in a turn based manner, hence maintaining the delay between them (see Klein et al. [8]). 1 This setting is represented by the matrix D 5 .

D 5 = a b a • -k b k -1 •
In the next section, we fix some notations and recall some useful definitions to develop our theory around matrices.

Background

Given a finite alphabet Σ, we use the standard notations Σ ⋆ , Σ ω and Σ ∞ for the set of finite words, infinite words and their union respectively, and ε to denote the empty word. Given two words u, w ∈ Σ ⋆ , we write u • w for their concatenation. Given a non-empty word

u = u 0 u 1 • • • u n , we let |u| := n + 1 be its length and set |ε| = 0. For k ≤ n, we write u[k] for the letter u k , u[: k] for the k-th prefix u 0 • • • u k and u[k :] for the k-th suffix u k • • • u n .
We now recall the basics of Linear-time Temporal Logic (LTL) [START_REF] Pnueli | The temporal logic of programs[END_REF]. An LTL formula φ (over a set AP of propositions) is evaluated on a labeling of the (discrete) timeline N, called an LTL assignment 2 λ ∈ ({⊤, ⊥} ω ) AP . We classically write λ |= φ whenever λ satisfies φ (we omit the semantics here and refer to [START_REF] Pnueli | The temporal logic of programs[END_REF]). Alternatively, an LTL assignment can be seen as an infinite word over the alphabet {⊤, ⊥} AP , which makes a tight connection between logic and automata: given an LTL formula φ, one can build -via the Vardi-Wolper construction [START_REF] Moshe | Automata-theoretic techniques for modal logics of programs[END_REF] together with the Safra-like translation from Büchi to parity acceptance condition [START_REF] Piterman | From nondeterministic Büchi and Streett automata to deterministic parity automata[END_REF] -a deterministic infinite-word parity automaton A φ whose language L(A φ ) is composed of all LTL assignments that satisfy φ.

Noticeably, LTL can be extended with propositional quantifications to Quantified Propositional Temporal Logic (QPTL), which enjoys the prenex normal form [START_REF] Prasad | Theoretical issues in the design and verification of distributed systems[END_REF]. Therefore, we can assume that QPTL formulas are all of the form ⃗ Q φ, where ⃗ Q is a finite sequence of propositional quantifications (∃a or ∀a, where a ∈ AP) and φ is an LTL formula.

In this paper, we consider vectors of words over the alphabet {⊤, ⊥}, indexed by a finite subset P of AP. Given a vector U = (U a ) a∈P of words over {⊤, ⊥} and a player b ∈ P, we denote by U (b) the b's component of U . We extend all notations for words to word vectors with their meaning component-wise. In addition, we introduce the notation U + a u for the word vector obtain by concatenating the word u to U (a).

As we will see, in our framework, the set AP of propositions for logics LTL and QPTL will be the breeding ground to pick the finite set P of players for our matrices.

4

The Formal Setting of Dependency Matrices

From a matrix D over P, a coalition Γ ⊆ P and an LTL formula φ, we derive the meta game ⟨D, Γ, φ⟩ that specifies how players can progress to label the timeline with truth values for thier proposition, what the coalition is, and what the winning condition is. Precisely, the goal of the coalition is to make φ true. The arena for the meta game, fully determined by the matrix D, is a modified multiplayer Gale-Stewart arena [START_REF] Gale | Infinite games with perfect information[END_REF] taking into account the information flow between players according to D. We distinguish progressing matrices that yield arenas with only infinite plays where no player is blocked, thus resulting in an LTL assignment. We also provide a graph-based polynomial-time algorithm to characterize progressing matrices.

Sticking to progressing matrices, we develop the proper notions of (player and coalition) strategies, along with the property of uniformity of a strategy that takes into account the imperfect information feature of our games. Intuitively, a strategy in the meta game is uniform if it depends only on the informations prescribed by the matrix. For pedagogical purposes, we start with bounded-value matrices, then consider arbitrary ones.

The Meta Arena of a Matrix

We fix a matrix D with values in Z and we describe the meta arena of D. A position in the meta arena is called a configuration, that is a word vector C that reflects the labeling over {⊤, ⊥} chosen so far by each player of P. The set of configurations is denoted by C := ({⊤, ⊥} ⋆ ) P and the initial configuration C 0 is the empty vector, namely ε P . We define the dynamics of the game, namely which player can play/progress, in a given configuration and which moves are available to her. Here is an intuitive example of those dynamics with a Round Robin matrix. ▶ Example 8. For the matrix D 2 of Example 3 and for the first round, only Player a can make a move of length 1. Then, assuming Player a chooses ⊤, the dependencies for each player are depicted separately below: in each picture, the squares identify expected information for the considered player to make her decision about the question mark (?).

▶ Example 7.

Dependencies of Player a

Dependencies of Player b Dependencies of Player c

0 1 2 a b c ⊤ ? 0 1 2 a b c ⊤ ? 0 1 2 a b c ⊤ ?
Observe that, here, neither Player a, nor Player c can make a move as the labeling of Player b at time point 0 is not set. On the contrary, Player b is able to progress.

A move of a Player a is a word u a ∈ {⊤, ⊥} ⋆ that is to extend her labeling along the timeline. For Player a to progress in configuration C , all her dependencies must be fulfilled. This is formalized as follows: in order to make a move (necessarily starting at the time point

t = |C (a)|),
α C a def = max(0, min b̸ =a (α C a,b )) (1)
As such, α C a is the maximum number of steps that Player a can perform in configuration C . Note that, if some α C a,b is negative (including 0), then Player a is stuck in C because Player b has not yet provided the expected information.

Based on the progress value, a legitimate move for Player a in a configuration C is a word in {⊤, ⊥} α C a . Then, a legitimate joint move in C is a vector of words u ∈ ({⊤, ⊥} ⋆ ) P such that, for every Player a, u(a) is a legitimate move for a. We can now define the move function between configurations:

∆ : C × ({⊤, ⊥} ⋆ ) P ⇀ C (C , u ) → C • u when u is a legitimate joint move in C undefined otherwise
with u a legitimate joint move. Remark that all players that can move have to play concurrently and greedily (i.e. their maximum number α C a of actions). A configuration C is said reachable if there is a finite sequence of legitimate joint moves that leads to C from the initial configuration C 0 .

▶ Proposition 9. Every reachable configuration, has a unique predecessor by ∆.

Proof. Suppose that there are two reachable configurations C 1 and C 2 and two legitimate joint moves u 1 and u 2 such that

C 1 • u 1 = C 2 • u 2 .
Then, consider a reachable configuration C ′ that is a prefix of both C 1 and C 2 . Suppose toward contradiction that there are legitimate joint moves

u 1 ′ ̸ = u 2 ′ with C 1 ′ = C ′ • u 1 ′ prefix of C 1 and C 2 ′ = C ′ • u 2 ′ prefix of C 2 . Since u 1 ′ ̸ = u 2 ′ , there is t ∈ N and a ∈ P such that C 1 ′ (a)[t] ̸ = C 2 ′ (a)[t]. By definition, C i ′ is a prefix of C i for i ∈ {1, 2}. Hence C 1 (a)[t] ̸ = C 2 (a)[t] which is in contradiction with C 1 • u 1 = C 2 • u 2 . In conclusion, if C 1 • u 1 = C 2 • u 2 , then C 1 = C 2 and u 1 = u 2 .
◀ By Proposition 9, the meta arena of reachable configurations is a tree and every reachable configuration contains all moves since the start of the game.

Observe that some meta arenas have reachable configurations C where for every Player a, we have α C a = 0. This happens because of cyclic dependencies. Here is an example. Situations where some players eventually get stuck can be characterized by analyzing some graph: for the case of Example 10, the graph is depicted below, and interestingly, it contains the cycle (a, b, a) whose weight is 0, a positive value. We will see in the next section, where the graph is formally defined, that such a cycle provides evidence that Players a and b eventually get stuck.

▶
D 6 =   a b c a • -1 -1 b +1 • -1 c -4 -4 •   0 1 2 3 4 5 a b c ⊤ ? ? ⊥ ⊥ ⊤ ⊤
a b c G D6 : 1- -1 1 -1 -5 -5

Progressing Matrix

We aim at characterizing matrices where no player gets stuck because of cyclic dependencies, so that each play yields an assignment of the timeline in order to interpret the LTL winning condition. Such matrices are called progressing and can be identified by means of their adjacency weighted graph, here called the dependency graph. The following proposition gives a characterization of progressing matrices.

▶ Proposition 12. A matrix D is progressing if, and only if, its dependency graph G D has no non-negative-weighted cycle.

The graph G D6 of Example 10 has a non-negative 0-weight cycle (a, b, a), so, matrix D 6 is not progressing. As a corollary, we have the following:

▶ Theorem 13. Deciding if a matrix is progressing is in PTIME.
Proof. The size of the dependency graph is linear in the size of the matrix and finding a non-negative cycle is polynomial in the size of the graph.

◀

From now on, unless stated otherwise, we only consider progressing matrices, that we keep calling "matrices" for simplicity. On the basis of such matrices, only infinite-horizon plays take place that consist in consecutive applications of the move function ∆ in the meta arena (see page 6): ▶ Definition 14. A play in the meta arena associated to a matrix is an infinite sequence of configurations (C n ) n∈N where C 0 is the empty configuration, and for every n ∈ N, C n+1 is the successor of C n .

The interested reader can explore the dynamics of plays at: https://francoisschwarzentruber.github.io/fsttcs2022

Notice that along a play (C n ) n∈N , C n+1 extends C n , so that to the limit, the play naturally yields a temporal assignment λ of the timeline: for every t ∈ N, and every Player a, we let λ(t)(a) def = C n (a)(t), for a sufficiently large integer n so that C n (a)(t) is defined. The next section focuses on strategies and winning strategies in the meta arena, where we discuss how a strategy complies with a matrix.

Strategies in the Meta Arena

In this section, we fix a matrix D over P, a coalition Γ ⊆ P and an LTL formula φ. Classically, a strategy maps histories to moves. However, since in our setting, a configuration fully characterizes a history (Proposition 9), we can equivalently define strategies as mappings from configurations to moves. A strategy for Player a ∈ Γ is a function f : C → {⊤, ⊥} ⋆ where f (C ) prescribes a legitimate move for Player a.

Furthermore, we define a joint strategy for the Γ as a function

F : C → ({⊤, ⊥} ⋆ ) Γ such that F (C )(a) is a legitimate move for Player a ∈ Γ. A joint strategy F provides a strategy F a for each Player a ∈ Γ defined by: F a (C ) def = F (C )(a). Given a joint strategy F for a coalition Γ, a play (C n ) n∈N is an outcome of F if for any n ∈ N and any Player a ∈ Γ, we have C n+1 (a) = C n (a) • F a (C n ).
We denote by out(F ) the set of outcomes of F . A joint strategy F is winning φ whenever all assignments associated to the plays in out(F ) satisfy φ.

However, in our dependency-based setting, a strategy is relevant only if it is uniform, in the sense that they only rely on the information available to the player. We illustrate this important feature in Example 15.

▶ Example 15. Consider matrix D 7 and configurations C 1 and C 2 below.

0 1 D 7 = a b a • -2 b -2 • C 1 = a b ⊤ ⊤ ⊥ ⊥ 0 1 C 2 = a b ⊤ ⊤ ⊥ ⊤
When Player a in C 1 comes to label time point 2, and since at time point 2, she can only access Player b's labeling up to time point 0, she cannot distinguish it from C 2 . However, once she labels time point 2, she is able to access Player b's label at time point 1, and is allowed to take this information into account before choosing her label at time point 3. Now, according to the matrix D 7 , we have α

C 1 a = α C 2 a = 2.
Although Player a cannot distinguish between C 1 and C 2 , she is allowed to choose different 2-length moves that only differ in their second letters. Indeed, her choice at time point 2 has to be uniform (and therefore the same in both configurations C 1 and C 2 ). On the contrary, she may play differently for her choice at time point 3. For instance, the overall move in

C 1 can be ⊤⊥ while it is ⊤⊤ in C 2 .
We formalize the phenomenon described in Example 15 with equivalence relations between configurations. In the example, Player a has to choose a move u 0 u 1 but C 1 and C 2 are indistinguishable for her when it comes to choosing the first letter u 0 . However, they can be distinguished for the choice of the second letter u 1 . Then, we need multiple relations, one for each letter of a move.

≤ min(α C 1 a , α C 2 a ), C 1 a ∼ k D C 2 implies f (C 1 )[: k] = f (C 2 )[: k]. Observe that C 1 a ∼ k+1 D C 2 implies C 1 a ∼ k D C 2 .
We generalize Definition 16 to joint strategies in a natural way by requiring the uniform property for every individual strategy of the joint strategy. For the rest of the paper, all strategies are implicitly D-uniform.

Before addressing the central decision problem of the existence of a winning joint strategy, we extend our setting to allow matrices with infinite values.

Arbitrary Matrices

D 8 =   a b c a • +∞ +∞ b -∞ • -1 c -∞ 0 •  
As observed in Example 17, (Z ∪ {-∞, +∞})-valued matrices may yield to "transfinite" configurations (i.e. with possibly components in {⊤, ⊥} ω instead of {⊤, ⊥} ⋆ ). As a result, a play may now be a finite sequence of (possibly infinite) sequences of configurations. We can adapt the notion of reachable configuration accordingly -since this is routine, we omit the precise definition here.

From now on, unless stated otherwise, we consider arbitrary matrices. In the next section, we address the decision problem EWS of the existence of a winning strategy.

Undecidability of EWS

We consider the following central decision problem EWS of deciding the Existence of a Winning (uniform) Strategy for a coalition of players (EWS for short):

▶ Theorem 18. Let EWS be the following problem: Input: A matrix D, a coalition Γ and an LTL-formula φ.

Output: "Yes" if and only if there is a D-uniform joint strategy for Γ that is winning for φ.

EWS is undecidable.

This reslut is unsurprising, given the imperfect-information nature of our multi-player game.

Theorem 18 is proved by reducing the Tiling problem [START_REF] Berger | The undecidability of the domino problem[END_REF] to EWS. Recall that the Tiling problem takes in input a finite set of square tiles and two binary connectivity relations over the tiles, that specify which pairs of tiles may be adjacent (resp. horizontally and vertically). The output is the answer to the question whether there exists a tiling of the plane, that is a mapping from N 2 to the set of tiles such that any two of adjacent tiles respect the connectivity constraints. In a nutshell, our reduction involves four players τ 1 , τ 2 (tilers) and c 1 , c 2 (challengers): in a round, Challenger c 1 chooses a place (x, y) in N 2 and privately communicates it to his tiler companion τ 1 by playing ⊤ x ⊥⊤ y ⊥ ω . Tiler τ 1 then responds by choosing a tile t independently of the choice of Challenger c 2 and plays ⊤ t ⊥ ω , and symmetrically for Players τ 2 and c 2 . This way, the two tilers play independently. The two different Challengers are used to test the binary relations by choosing adjacent places. The following matrix encodes this situation.

D Tiling :=     c1 c2 τ1 τ2 c1 • -∞ -∞ -∞ c2 -∞ • -∞ -∞ τ1 +∞ -∞ • -∞ τ2 -∞ +∞ -∞ •     .
In the next section, we present a decidable sub-case.

Decidability of EWS for perfect-information Matrices

A close inspection of the proof of Theorem 18 reveals that not being able to circumvent the amount of information hidden to players is a matter. We introduce the subclass of perfect-information matrices where every player always has full information about the current configuration before proceeding, yielding a meta game that is turn-based with perfect information.

Definition and Properties

A meta game is perfect-information as long as two reachable configurations are not kindistinguishable, for every k. Actually, not being 0-indistinguishable is sufficient, since k-indistinguishability are nested (see Section 4.3). Furthermore, for the meta arena to be turn-based, we must guarantee that in each round, only one player can progress. This yields the following definition.

▶ Definition 19.

A matrix D is perfect-information if for every reachable configuration C : for every player a and reachable configuration

C ′ ̸ = C , we have C ̸ a ∼ 0 D C ′
and there is exactely one player a such that α C a ≥ 1. Remark that, by Definition 19, every move of a single player, from a reachable configuration that is not the initial one, is necessarily of length 1. Indeed, if a player could make a move of length strictly greater than 1, we could create another reachable configuration that would be 0-indistinguishable from the first one, a contradiction.

▶ Lemma 20. Let D be a perfect-information matrix, then α C

a ≤ 1 for any non-initial reachable configuration C and every Player a.

Proof. By contradiction, suppose that there is a non-initial reachable configuration C 1 with α C 1 a ≥ 2 for some Player a. Because D is progressing and perfect-information, there is a unique Player b that can progress in ∆ -1 (C 1 ). If b = a, we would not have α C 1 a ≥ 2 because players play greedily. Then, we have a ̸ = b.

We now exhibit a reachable configuration

C 2 ̸ = C 1 such that C 1 a ∼ 0 D C 2 .
Let u 1 be the joint move leading to C 1 , that is ∆(∆ -1 (C 1 ), u 1 ) = C 1 . As exactly one player moves, u 1 (c) = ε for every Player c ̸ = b. We define the joint move u 2 as follows: for every Player c ̸ = b, let u 2 (c) = ε and u 2 (b) = fliplast(u 1 (b)) where fliplast flips the last letter of the word (mapping ⊤ to ⊥, and ⊥ to ⊤).

For C 2 = ∆(∆ -1 (C 1 ), u 2 ), we have |C 1 (a)| = |C 2 (a)|, and C 1 (c) = C 2 (c) for P layer c ̸ = b. We have α C i a,b ≥ 2 for i ∈ {1, 2}. Then, by definition, |C i (b)| -(D[a, b] + |C i (a)|) ≥ 2, whence (D[a, b] + |C i (a)|) ≤ |C i (b)| -2. Now, let t ≤ |C 1 | + D[a, b]. By transitivity, t ≤ |C i (b)| -2. However, C 1 (b)[t] = C 2 (b)[t] for t ≤ |C 1 (b)| -2 since only the last letter of C 1 (b) differs from C 1 (b). Therefore, C 1 a ∼ 0 D C 2 which is a contradiction. ◀ ▶ Corollary 21.
Let D be a perfect-information matrix, and C a non-initial reachable configuration, there is Player a with α C a = 1 and for every other Player b, we have α C b = 0.

We can use this result to establish a characterization of perfect-information matrices. Let C be a reachable non-initial configuration and let Player a be the player that can progress in C . By Corollary 21, we have α

2 such that C 1 a ∼ 0 D C 2 .
We can assume without loss of generality that they are immediate successors of the same reachable configuration C . We compare the progress values of Player a with the one of the only player that can progress in C , and prove that the configurations C 1 and C 2 are equal.

A Parity Game to solve the Existence of a Winning Strategy

For perfect-information matrices, we establish a reduction from EWS to solving a parity game, thus attaining decidability (Theorem 30). Consider a perfect-information matrix D, a coalition Γ and a formula φ. We define the parity game G(D, Γ, φ) where the coalition Γ has a winning D-uniform strategy if, and only if, Player 0 has a winning strategy in G(D, Γ, φ) against Player 1.

The parity game G(D, Γ, φ) is built up from the deterministic parity automaton A φ for φ (see Section 3). Its plays simulate runs of automaton A φ on the sequence of growing configurations along a play in the meta arena. Positions in the parity games are pairs composed of states of A φ and buffers: a buffer β is a word vector (β a ) a∈P with at least one empty component. Formally, the set of buffers is:

{(β a ) a∈P ∈ ({⊤, ⊥} ⋆ ) P | β b = ε for some b ∈ P}.
The buffer of a configuration is the "pending part" of the configuration, namely its greatest suffix that is a buffer. ▶ Example 25. Consider the perfect-information matrix D 9 below where a reachable configuration C and its buffer are depicted.

0 1 2 3 4 D 9 =   a b c a • 2 3 b -3 • -1 c -4 0 •   C = a b c ⊤ ⊤ ⊤ ⊥ ⊥ ⊤ ⊥ ⊥ ⊤ ⊤ buffer
We say that a buffer is reachable if it is the buffer of some reachable configuration. We can show that in a reachable configuration, the single player that can progress only depends on the buffer β of this configuration, and we write p β this player.

We denote by B the set of reachable buffers, by B ∃ the set of buffers β in B where p β ∈ Γ, and we let B def = B\B ∃ . Although our matrix is perfect-information, we remark that, by Lemma 20, for the particular case of the empty buffer β 0 (of the initial configuration), Player p β 0 might be playing a long move. Moreover, it can be shown that the reachable buffers are finitely many1 and that their number is exponential in the values of the matrix (this is because the longest component of a reachable buffer is given by the biggest absolute value in the matrix).

We now informally describe the parity game with its two players Player 0 and Player 1. As said, a position in the parity arena is pair (q, β ) composed of a state q of the automaton and a buffer β . Position (q, β ) belongs to Player 0 whenever β ∈ B ∃ , otherwise β ∈ B ∀ and it belongs to Player 1.

In a given position (q, β ), only p β progresses by choosing a move u ∈ {⊤, ⊥}. We consider the word vector obtained by catenating u to p β 's component in buffer β , that we write β + p β u in the following.

If β + p β u is still a buffer we update the position to (q, β + p β u). Note that this is always the case for the initial buffer β 0 . Otherwise, the first letter of word vector β + p β u is all filled with labels on every component, and thus can be read by automaton A φ . We then update the position to the new current state of A φ and to the buffer obtained by removing the first letter of β + p β u (which is a buffer as β is not initial).

Formally, the parity game is the following.

▶ Definition 26. Given a perfect-information matrix D, a coalition of players Γ and a deterministic parity automaton A φ = (Q, q 0 , Σ, δ, par) with Σ = {⊤, ⊥} P , we define the parity game G(D, Γ, φ) = ⟨P 0 , P 1 , s 0 , →, par G ⟩ where:

P 0 = Q × B ∃
is the set of positions for Player 0, P 1 = Q × B ∀ is the set of positions for Player 1, s 0 = (q 0 , β 0 ) is the initial position, (q, β ) → (q ′ , β ′ ) when there is a legitimate move u for p β in the meta arena such that: 1. either β + p β u is a buffer and q = q ′ and β ′ = β + p β u. 2. or q ′ = δ(q, (β + p β u)[0]) and β ′ = (β + p β u) [1: ] and p β is the only player s.t. β p β = ε; par G (q, β ) = par(q), that is the priority of a position (q, β ) is the priority of the state q in the automaton A φ .

Note that the number of positions in the parity game is the product of the number of states in the automaton and the number of buffers, and that the game has the same priorities as the automaton.

▶ Proposition 27 (For a perfect-information matrix D). ⟨D, Γ, φ⟩ is a positive instance of EWS if, and only if, Player 0 has a winning strategy in G(D, Γ, φ).

Proposition 27 gives us an upper bound complexity of EWS by the following algorithm. 1. Compute the deterministic parity automaton A φ (accepting the models of φ); 2. Compute the parity game G(D, Γ, φ);

Solve G(D, Γ, φ).

In the following, the size of the matrix D is the quantity |D| = a̸ =b |D[a, b]|. Observe that we can build A φ by using the Vardi-Wolper construction [START_REF] Moshe | Automata-theoretic techniques for modal logics of programs[END_REF] with the Safra-like translation from Büchi to parity acceptance condition [START_REF] Piterman | From nondeterministic Büchi and Streett automata to deterministic parity automata[END_REF], so that parity game of Step 2 has O(22 |φ| × 2 2 |D| ) positions and O(2 |φ| ) priorities, hence a 2-Exptime decision procedure for EWS.

The next subsection, we show that this algorithm is essentially optimal by a reduction of the Church Synthesis problem.

Reduction from the Church Synthesis problem

For the lower bound, we reduce the Church Synthesis for LTL properties [START_REF] Finkbeiner | Synthesis of reactive systems[END_REF][START_REF] Pnueli | On the synthesis of reactive systems[END_REF]. Our Example 5 (page 4) illustrates the reduction. ▶ Definition 28. Given a coalition Γ, a Church matrix is a matrix D where for any two players a ̸ = b, we have:

D[a, b] = 0 if a / ∈ Γ and b ∈ Γ -1 otherwise
In essence, for Church matrices, players have the same knowledge about the current configuration, allowing them to foresee their allies moves.

Observe that Church matrices may not be perfect-information, since the moves of every player in a team (coalition or opponents) are concurrent. Nonetheless, we can "transform" any Church matrix D into a linear sized perfect-information Round Robin matrix D ′ (see Example 3 and Definition 29) such that ⟨D, Γ, φ⟩ is a positive instance of EWS if, and only if, ⟨D ′ , Γ, φ⟩ is a positive instance of EWS. ▶ Definition 29. A Round Robin matrix is a matrix D such that there exists a total order ≺ over P, where

D[a, b] = -1 if a ≺ b 0 otherwise
The total order ≺ describes the order in which players will play (the player that is minimal for ≺ plays first). Remark that D[a, b] + D[b, a] = -1 for any two players a ̸ = b then every Round Robin matrix is perfect-information (by Theorem 23). Given a Church matrix, we can choose order ≺ so that all players in the coalition play before their opponents.

By summing up, we polynomially reduce 2 a Church synthesis problem to a EWS problem for a Church matrix and that is in turn linearly reduced to a EWS problem for a Round Robin matrix. From this latter reductions, we can state the following. ▶ Theorem 30. EWS for perfect-information matrices is 2-Exptime-complete in the size of the LTL formula.

In the next section, we extend the class of perfect-information matrices to allow some matrices with infinite values, while keeping the decidability of EWS for the resulting superclass. In particular, QPTL matrices (see Example 4 on page 4) falls into this class.

Perfect-Information Matrices with Possibly Infinite Values

The proof of Proposition 27 can be extended to QPTL formulas instead of LTL formulas.

The following example illustrates a procedure for matrices with infinite values that yields a generalization of the perfect-information property (see Definition 32).

▶ Example 31. Consider the following matrices where the latter is perfect-information:

D 8 =   a b c a • +∞ +∞ b -∞ • -1 c -∞ 0 •   and D ′ 8 = b c b • -1 c 0 • According to D 8 ,
̸ = b: 1. D[a, b] ∈ Z implies D[a, b] + D[b, a] = -1; 2. D[a, b] ∈ {-∞, +∞} implies D[a, b] = -D[b, a]; 3. D[a, b] = +∞ implies D[a, c] ∈ {-∞, +∞}, for all c ̸ = a.
Observe that the procedure is in fact non-elementary in the number of players with +∞ dependencies. Moreover, since the validity problem for QPTL [START_REF] Prasad Sistla | The complementation problem for Büchi automata with applications to temporal logic[END_REF] reduces to EWS for arbitrary perfect-information matrices, we have the following.

▶ Theorem 33. EWS is non-elementary for arbitrary perfect-information matrices.

Conclusion

We presented the expressive framework of dependency matrices that can capture several game settings such as concurrent and turn-based games [START_REF] Alur | Alternating-time temporal logic[END_REF], (two-player) delay games [START_REF] Klein | What are strategies in delay games? borel determinacy for games with lookahead[END_REF][START_REF] Klein | How much lookahead is needed to win infinite games?[END_REF][START_REF] Thomas | Degrees of lookahead in regular infinite games[END_REF], logic QPTL [START_REF] Prasad Sistla | The complementation problem for Büchi automata with applications to temporal logic[END_REF], and Church Synthesis Problem [START_REF] Finkbeiner | Synthesis of reactive systems[END_REF].

We proved that the existence of a winning strategy for a coalition to achieve an LTL formula (EWS) is undecidable for arbitrary matrices.

We then exhibited the subclass of perfect-information bounded-value matrices for which the problem EWS is 2-Exptime-complete in the size of the formula.

Finally, we extended the class of perfect-information matrices with a narrow use of infinite dependencies allowing to re-use known techniques of automata projection for QPTL. For these matrices, EWS becomes non-elementary. Still our complexity analysis of EWS needs beeing refine regarding the matrix parameter: we do not know yet the lower bound complexity when the LTL formula is fixed.

A first track to continue this work concerns EWS for the whole class of boundedvalue matrices. We conjecture it is decidable, since, for a bounded-value matrix, each k-indistinguishable equivalence class of a reachable configurations has a bounded size.

F S T T C S 2 0 2 2

Given two vertices c i and c j of a non-negative cycle c = (c 0 , . . . , c |c| ) (with c 0 = c |c| ), we denote by w i the label r(c i , c i+1 ) and W i,j the circular sum of the labels between c i and c j :

If i < j, then W i,j = w i + • • • + w j-1 ; else, W i,j = W i,|c| + W 0,j . Remark that for every index i, W i,i is the sum of all labels of the cycle. So, for a non-negative cycle, W i,i ≥ 0. Furthermore, we denote by W ⋆ i the minimal sum W ⋆ i = min j (W i,j ).

▶ Lemma 34. Given a matrix D with a non-negative cycle c = (c 0 , . . . , c |c| ), for all player c i in the cycle, for all reachable configuration C , we have the following.

|C (c i )| ≤ max(0, -W ⋆ i )
Proof. We do the proof by induction on reachable configuration.

(base case) In the initial configuration C 0 , the property is obvious.

(inductive case) Consider a configuration C ′ = ∆(C , (u a ) a∈P ) for some joint move (u a ) a∈P and a reachable configuration

C such that |C (c i )| ≤ max(0, W ⋆ i ) for every c i ∈ c. Consider i ∈ 0, . . . , |c| . |C ′ (c i )| = |C (c i )| + α C ci = |C (c i )| + max(0, min a̸ =ci (α C ci,a )) ≤ |C (c i )| + max(0, α C ci,ci+1 ) ≤ |C (c i )| + max(0, |C (c i+1 )| -D[c i , c i+1 ] -|C (c i )|) ≤ max(|C (c i )|, |C (c i+1 )| -w i ) ≤ max(max(0, -W ⋆ i ), max(-w i , -W ⋆ i+1 -w i ))
The last inequality is obtained thanks to the inductive hypothesis. We now prove that -W ⋆ i ≥ max(-w i , -W ⋆ i+1 -w i ). Since w i = W i,i+1 , we have -W ⋆ i ≥ -w i . Let j 0 ∈ 0, . . . , |c| such that W ⋆ i+1 = W i+1,j0 . We now do a case study on j 0 . if

j 0 = i + 1, then, because c is non-negative, -W ⋆ i+1 -w i ≤ -w i . if j 0 ̸ = i + 1, then, -W ⋆ i+1 -w i = -W i,j0 ≤ -W ⋆ i Then we have |C ′ (c i )| ≤ max(0, -W ⋆ i ).
We have proven the property by induction. ◀

We now state a lemma to prove the other way around: that non-negative cycles are necessary for a matrix not to be progressing. ▶ Lemma 35. Given a bounded matrix D, if there is a player that is eventually blocked, then every player is eventually blocked.

(α C b,c )) ≤ |C (b)| + max(0, α C b,a ) ≤ |C (b)| + max(0, |C (a)| -D[b, a] -|C (b)|) ≤ max(|C (b)|, |C (a)| -D[b, a]) ≤ max(max(0, k -D[b, a]), k -D[b, a]) ≤ max(0, k -D[b, a])
We have proven the property by induction. ◀

Now, when all players are blocked, we use the next well known result of graph theory to find our non-negative cycle.

▶ Lemma 36. Given a directed graph G with no self loop, if every vertex is the source of an edge, then, there is a cycle in the graph. Now, we can give a proof for Proposition 12.

▶ Proposition 12. A matrix D is progressing if, and only if, its dependency graph G D has no non-negative-weighted cycle.

Proof. Given a matrix D with a non-negative cycle, then, by Lemma 34, we immediately have that every player in the cycle is eventually blocked.

In a second time, consider a matrix D that is not progressing. Then, by Lemma 35, for every player a, there is an integer k a such that for every reachable configuration C , we have |C (a)| ≤ k a . Consider a configuration C such that every player is blocked. Then, by immediate contradiction, for every player a, there is a player q a ̸ = a such that α C a,qa ≤ 0 (otherwise, there would be a player that can progress). The graph G = ⟨V, E⟩ with the vertices V = P are the players of the matrix and the edges are defined as E = {(a, q a ) | a ∈ P}. Since, G is a directed graph with no self loop, by Lemma 36, there is a cycle c = (c 0 , . . . , c |c| ) in the graph thus, for every i ∈ 0, . . . , |c| -1 , we have c i+1 = q ci and c |c| = c 0 . We have the following.

|c|-1 i=0 α C ci,ci+1 = |c|-1 i=0 |C (c i+1 )| -D[c i ; c i+1 ] -|C (c i )| = - |c|-1 i=0 D[c i ; c i+1 ] Since α C
ci,ci+1 ≤ 0 for every i ∈ 0, . . . , |c| , we have proven that c is a non-negative cycle. ◀

B Proofs of Section 6

We now address the proof of Theorem 23. The first direction states that a perfect-information matrix D satisfies that for every different Players In particular, thanks to Equation (3), we can take t = t 0 , and we have C 1 (b)(t 0 ) = C 2 (b)(t 0 ), in contradiction with Equation [START_REF] Alur | Alternating-time temporal logic[END_REF]. ◀

C Reduction from Church matrices to Round Robin matrices

We now prove the claim made in Section 6.3 that Church matrices can be reduced to Round Robin matrices. From a Church matrix D for a coalition Γ, we define a Round Robin matrix Rob(D) as follows. We take an arbitrary order ≺ on the players such that for every Player a ∈ Γ and every Player b / ∈ Γ, it holds a ≺ b. Rob(D) is the Round Robin matrix for this order.

▶ Lemma 39. Given an LTL formula φ and a Church matrix D, there is a winning joint D-uniform strategy iff there is a winning joint strategy Rob(D).

Proof. Suppose that there is a winning joint strategy F for Γ that is Rob(D)-uniform. Only the moves of players of the coalition can make F non-D-uniform. But, given the joint strategy for the whole coalition, we cannot reach two configurations that are equal on everything except a labeling of a player of the coalition because our strategies are deterministic. Thus, in practice, F is D-uniform.

Definition 1 .

 1 A dependency matrix (or simply a matrix) over a finite set P of at least two players is a matrix D = (D[a, b]) a̸ =b∈P , and whose values range over Z ∪ {-∞, +∞}. In a dependency matrix (D[a, b]) a̸ =b∈P over P, the value D[a, b] describes how Player a's decisions depends on Player b's: Player a's decision for choosing the valuation at time point t depends on the ones chosen by Player b at all time points in the interval [0, t + D[a, b]]. As such, whenever D[a, b] < 0, Player a's decision at time point t is independent of the decisions made by Player b up to some time point before t. In particular, if D[a, b] = -∞, Player a's decisions is independent of any of Player b's.

Figure 1

 1 shows the configuration C in which Player a played the word C (a) = ⊤⊤⊥⊤⊥, Player b played C (b) = ⊥⊥⊤, and Player c played C (c) = ⊥⊥⊤⊤.

FFigure 1

 1 Figure 1 A configuration C where Player a has chosen her labeling up to time point 4, Player b up to time point 2 and Player c up to 3.

  Player a needs to access the labeling of Player b up to time point t + D[a, b], included. Therefore, the value α C a,b := |C (b)| -(D[a, b] + |C (a)|) characterizes the length of a move available to Player a with regard to her dependency on Player b only. Thus, the overall progress value of Player a, written α C a , takes into account all quantities α C a,b for b ̸ = a in a conjunctive manner, leading to consider the most restrictive one. Formally:

Figure 2

 2 Figure 2 Player a wants to know the moves of Player b and reciprocally.

▶ Definition 11 . 2 31: 8 Dependency

 1128 Given a matrix D = (D[a, b]) a̸ =b∈P , the dependency graph of D is the weighted directed graph G D = (V, E, r) where: F S T T C S 2 0 2 Matrices for Multiplayer Strategic Dependencies V = P is the set of vertices, E = {(a, b)|a ̸ = b} is the set of edges, r(a, b) = D[a, b] is the weight of the edge (a, b).

▶

  Formally, we introduce an equivalence relation between configurations parameterized by a scope k: two configurations C 1 and C 2 are k-indistinguishable for Player a, denoted C 1 a ∼ k D C 2 , whenever |C 1 (a)| = |C 2 (a)|, and for every Player b ̸ = a and every t ≤ |C 1 (a)|+D[a, b]+k, we have: either both C 1 (b)(t) and C 2 (b)(t) are undefined (meaning k is greater than the progress of b in both configurations), or C 1 (b)(t) = C 2 (b)(t). We resort to relations a ∼ k D to formalize the notion of uniform strategies in our framework, where the parameter k is meant to range over [0, min(α C 1 a , α C 2 a )[. Definition 16. A strategy f for Player a is D-uniform whenever for any two configurations C 1 and C 2 , and any natural number k

Recall, by Definition 1 , 17 ▶ 17 .

 11717 that a value D[a, b] = -∞ indicates that Player a's decision are independent from Player b's. In particular, if the matrix line D[a, .] is all filled with value -∞, Player a fills the whole timeline in the first round. On the contrary, D[a, b] = +∞ forces Player a to wait until Player b has entirely filled the timeline.A typical example of a matrix with infinite values is provided by the matrix D 3 of Example 4, and is reminiscent of what is expressed in the setting of the logic QPTL: in this example, a play takes place as follows. First, Player a chooses an a-assignment of the timeline. Second, since Player a is done and Player b is independent from Player c, Player b has all the required information for choosing the b-assignment over the timeline. Third and finally, Player c can proceed for the c-assignment, and the play ends.For the cases that mix finite and infinite value, we consider first Example Example Consider matrix D 8 below. In a play, Player b and Player c's mutual dependencies enforce them to proceed in turn for choosing their respective labeling, while Player a cannot play until the other two have labeled the whole timeline.

C a = 1 ▷F S T T C S 2 0 2 2 31: 12 Dependency

 1212 and α C b = 0 for every Player b ̸ = a. We first make a claim: Claim 22. α C a,b = 1 and α C a,b ≤ 0 Matrices for Multiplayer Strategic Dependencies Using this claim, we obtain |C (b)|-(D[a, b]+|C (a)|) = 1 and |C (a)|-(D[b, a]+|C (b)|) ≤ 0. Then, D[a, b] + D[b, a] ≥ -1. Since the matrix is progressing, we have D[a, b] + D[b, a] ≤ -1 and then D[a, b] + D[b, a] = -1. In fact, we show that this necessary condition is a precise characterization of the perfect-information matrices. ▶ Theorem 23. A matrix D is perfect-information if and only if for all players a and b, with a ̸ = b we have D[a, b] + D[b, a] = -1. We now show the reciprocal, namely, if D satisfies D[a, b] + D[b, a] = -1, then D is perfect-information. The first step is to prove that, the associated meta arena is turn based. ▶ Lemma 24. For D with D[a, b] + D[b, a] = -1 whenever a ̸ = b, there is at most one Player a with α C a ≥ 1 in every configuration C . Proof. By contradiction, suppose α C a,b ≥ 1 and α C b,a ≥ 1. Then, α C a,b + α C b,a ≥ 2. Since α C a,b = |C (b)|-(D[a, b]+|C (a)|) and α C b,a = |C (a)|-(D[b, a]+|C (b)|), we obtain D[a, b]+D[b, a] ≤ -2 which contradicts the assumption on D. ◀ It is left to prove that any two different reachable configurations are not a ∼ 0 D -equivalent for any a. We here just give an intuition of the proof by contradiction. Suppose that there are two different reachable configurations C 1 and C

Proof.

  Consider a bounded matrix D where there is a player a and a natural number k ∈ Z such that for every reachable configuration C , we have |C (a)| ≤ k. We prove by induction on reachable configurations that for each Player b, we have |C (a)| ≤ max(0, k -D[b, a]). (base case) In the initial configuration C 0 , the property is obvious. (inductive case) Consider a configuration C ′ = ∆(C , (u a ) a∈P ) for some joint move (u a ) a∈P and a configuration C such that |C (a)| ≤ k -D[b, a] for every b. Then, for every Player b we have the following. F S T T C S 2 0 2 2 31:18 Dependency Matrices for Multiplayer Strategic Dependencies |C ′ (b)| = |C (b)| + α C b = |C (b)| + max(0, min c̸ =b

▷ 0 D C 2 . 0 D▶ 0 DD 0 D 0 D 0 D 0 D▶ 0 D 2 ) 3 )Finally, since C 1 a ∼ 0 D C 2 ,

 0200000002302 a and b, we have D[a, b] + D[b, a] = -1 and is presented in Section 6.1. We just need to prove Claim 22. Recall that C is a reachable non-initial configuration and Player a is the player that can progress in C . By Corollary 21, we have α C a = 1 and α C b = 0 for every player b ̸ = a. We consider a player b ̸ = a. Claim 22. α C a,b = 1 and α C a,b ≤ 0 Proof. First we prove that α C a,b ≤ 0. Remark that, in C , Player a has two legitimate moves: ⊤ and ⊥. Let C 1 = ∆(C , (⊤) a ) and C 1 = ∆(C , (⊥) a ). Note that C 1 and C 2 are reachable. Toward contradiction, assume that α C a,b > 0. We prove the contradiction C 1 b ∼ 0 D C 2 . We have α C a,b = |C (a)| -(D[b, a] + |C (b)|) > 0. Then |C (a)| > D[b, a] + |C (b)|. Therefore, for all t ≤ D[b, a] + |C (b)|, we have t < |C (a)|. And because C 1 (a)(t) = C (a)(t) = C 2 (a)(t), we conclude that C 1 b ∼ Then we prove that α C a,b = 1. By definition, α C a,b ≥ 1. Toward contradiction, suppose α C a,b > 1. Let C ′ be the configuration defined by C ′ (c) = C (c) for all c ̸ = b and C ′ (b) = fliplast(C (b)). We have that C ′ is reachable and, by the same kind of reasoning than previous point, we have C a ∼ C ′ , which is in contradiction with the assumption on D. ◁ Let us prove the other direction, namely that a matrix D is perfect-information if D[a, b] + D[b, a] = -1 for every pair of different Players a and b. Lemma 24 states that the meta game of such a matrix is turn based. Now, we need to prove that two different reachable configurations are not 0-indistinguishable. To do so, we first show two results on 0-indistinguishable relations. These results allow us to consider the "first time" at which two configurations diverge while being 0-indistinguishable. ▶ Lemma 37. Given a matrix D and two reachable configurations C and C ′ , with (C k ) k≤n and (C ′k ) k≤m such that C n = C and C ′m = C ′ . If n ≥ m then, for every Player a we have |C (a)| ≥ |C ′ (a)|. Proof. The proof is done by induction on n -m. (base case) If n = m, we do an induction on n. (base case) If n = m = 0, then C = C ′ = C 0 , the property is immediate. (induction) Suppose the property holds for some n, m ∈ N with n = m. Consider C and C ′ reachable. There are (C k ) k≤n+1 and (C ′k ) k≤m+1 with C n+1 = C and C ′m+1 = C ′ . By inductive hypothesis, we have |C n (a)| = |C ′m (a)| for every Player a. Then, α C n a = α C ′n a and so, |C (a)| = |C ′ (a)|. (induction) Suppose the property holds for some n, m ∈ N with n ≥ m. Consider C and C ′ reachable: there are (C k ) k≤n+1 and (C ′k ) k≤m with C n+1 = C and C ′m = C ′ . By inductive hypothesis, for every Player a |C n (a)| ≥ |C ′m (a)| and because |C n+1 (a)| ≥ |C n (a)|, we have |C n+1 (a)| ≥ |C ′m (a)|. We have proved the property by induction. ◀ Lemma 38. Given a dependency matrix D, and two reachable configurations C and C ′ that are non-initial, if C a ∼ C ′ , then, one of the following holds. 1. ∆ -1 (C ) ∆ -1 (C ′ ) Proof. Consider two reachable configurations C and C ′ such that C a ∼ C ′ . By definition, |C (a)| = |C ′ (a)|, and for every Player b ̸ = a, every t ≤ |C (a)| + D[a, b], we have C (b)(t) = C ′ (b)(t). Since C and C ′ are reachable, there are two sequences of successive configurations (C k ) k≤n and (C ′k ) k≤m such that C n = C and C ′m = C ′ . By symmetry we can assume n ≥ m. We do a case study.If n = m, then ∆ -1 (C ) and ∆ -1 (C ′ ) are also reachable and their sequences have the same length. By Lemma 37 for every player b, we have that|∆ -1 (C )(b)| = |∆ -1 (C ′ )(b)|. Immediately, |∆ -1 (C )(a)| = |∆ -1 (C ′ )(a)| and because C a ∼ C ′ , for every t ≤ |∆ -1 (C )(a)| + D[a, b] ≤ |C (a)| + D[a, b], we have ∆ -1 (C )(b)(t) = C (b)(t) = C ′ (b)(t) = ∆ -1 (C ′ )(b)(t). Hence, ∆ -1 (C ) a ∼ ∆ -1 (C ′ ) F S T T C S 2 0 2 231:20 Dependency Matrices for Multiplayer Strategic DependenciesIf n > m then ∆ -1 (C ) is reachable with a sequence of length n -1 ≥ m as ∆ -1 (C ) = C n-1then, by Lemma 37, for every player b, we have|∆ -1 (C )(b)| ≥ |C ′m (b)|. And, because C a ∼ C ′ , we have |C (a)| = |C ′ (a)|, then |∆ -1 (C )(a)| = |C ′ (a)|. Furthermore, for every t ≤ |∆ -1 (C )(a)| + D[a, b], if both ∆ -1 (C )(b)(t) and C ′ (b)(t) are defined, we have ∆ -1 (C )(b)(t) = C (b)(t) = C ′ (b)(t). Finally, we prove that C (b)(t) is defined if and only if C ′ (b)(t) is defined. By Lemma 37, we already have that |∆ -1 (C )(b)| ≥ |C ′m (b)|, and if ∆ -1 (C )(b)(t) is defined, so is C (b)(t),and by hypothesis, so is C ′m (b)(t). We have proved the property. ◀ We now prove the theorem. Theorem 23. A matrix D is perfect-information if and only if for all players a and b, with a ̸ = b we have D[a, b] + D[b, a] = -1. Proof. The first direction is presented in Section 6.1. For the other direction, consider D such that D[a, b] + D[b, a] = -1. By Lemma 24, there is only one player that can progress in any reachable configuration. Is left to prove that for any two reachable configurations C and C ′ with C ̸ = C ′ , for every player a, we have C ̸ a ∼ . The proof is done by contradiction. Suppose that there are two different reachable configurations C 1 and C 2 with C 1 a ∼ 0 D C 2 . Then, by Lemma 38, we can assume that ∆ -1 (C 1 ) = ∆ -1 (C 2 ) = C . Let b the player that can progress in C . Then, for all c ̸ = b, we have C (c) = C 1 (c) = C 2 (c) and, for all t < |C (b)|, we have C (b)(t) = C 1 (b)(t) = C 2 (b)(t). Because C 1 ̸ = C 2 ,then we necessarily have the following. C 1 (b)(t 0 ) ̸ = C 2 (b)(t 0 ) for some t 0 ∈ {|C (b)| -α C b , |C (b)| -1} (Since α C b,a ≥ α C b , we have |C (a)| -(D[b, a] + |C (b)|) ≥ α C b . As Player a does not progress in C , we obtain |C 1 (a)| -(D[b, a] + |C (b)|) ≥ α C b . By hypothesis D[b, a] = -1 -D[a, b], we have |C 1 (a)| + 1 + D[a, b] -|C (b)| ≥ α C b and because |∆ -1 (C 1 )(b)| + α C b = |C 1 (b)|, we have: |C 1 (a)| + D[a, b] ≥ |C 1 (b)| -1 (we have that C 1 (b)(t) = C 2 (b)(t) for every t ≤ |C 1 (a)| + D[a, b].

2 0 2 2 31:4 Dependency Matrices for Multiplayer Strategic Dependencies

▶ Example 4 (QPTL). In QPTL, dependencies stem from the order of the quantifiers: in the formula ∃a∀b∃cφ where φ is an LTL-formula, Player a plays first on the full timeline and independently of the others. Then b only depends on what Player a did. Finally, c depends on what both Players a and b did. All this is reflected by matrix D 3 .

  If Player a and Player b are in charge of the output, Player c and Player d are in charge of the input, the players dependencies are captured by matrix D

4 : output Players a and b only depend on the past values of the input players, and that input Players c and d see all values and have to respond on the spot.

  Player a depends on the whole labeling of Player b and Player c. Given an LTL formula φ and say coalition {a, b}, we can answer EWS on instance ⟨D 8 , {b}, φ⟩ as follows: we can first answer EWS for ⟨D ′ 8 , {b}, ∃a φ⟩ (since D ′ 8 is perfect-information). If no, then return no for ⟨D 8 , {b}, φ⟩. Otherwise, each outcome of the winning strategy for Player 0 in ⟨D ′ 8 , {b}, ∃a φ⟩ reflects a play ρ in ⟨D ′ 8 , {b}, ∃a φ⟩. From play ρ, exhibit a unique accepting run in A ∃aφ . By tracing back this run inside A φ , reconstruct Player a's response to the play ρ. The procedure employed in Example 31 applies to arbitrary matrices as long as they fulfill the Definition 32. ▶ Definition 32. An arbitrary matrix D is perfect-information if for any a

In their setting, the delay is defined with a delay function that gives at each round the number of moves the input Player has to make. However, Klein et al. mainly studied the fixed delay setting where the function is set to 1 after the first round.

also named trace in the model-checking setting.

Actually the set of reachable configurations is a regular language that can be recognized by a word automaton with buffers as states.

The size of the Church matrix is quadratic in the number of propositions of the Church synthesis problem

https://francoisschwarzentruber.github.io/fsttcs2022/ Software (Source Code): https://github.com/francoisschwarzentruber/fsttcs2022 archived

A second track regards our transformation of Church matrices into perfect-information Round Robin ones. We believe that our approach can generalize to a class of bounded-values matrices enlarging the one of Church matrices.

Conversely, consider two configurations C 1 and C 2 such that C 1 a ∼ Rob(D) C 2 for some a ∈ Γ. We denote by k the length of C 1 (a). Then for every b ∈ P, if a ≺ b, we have

Because we chose the order so that a ≺ b for every a ∈ Γ and b / ∈ Γ, we have that C 1 a ∼ D C 2 . Thus every strategy D-uniform is Rob(D)-uniform. ◀

D Proof of Theorem 33

▶ Theorem 33. EWS is non-elementary for arbitrary perfect-information matrices.

Proof. In this proof, we use the notation F ↾P\{a} to denote the function F restrained to the domain P\{a}. Given a dependency matrix D, we decompose the set of Players P as follows.

We reason by induction on the size of P ∞ . The base case is |P ∞ | = 0. In this case, we can apply Theorem 30.

Suppose that we can decide the EWS problem for matrices with |P ∞ | = n for some n ∈ N. We now prove that we can decide the problem for matrices with If (a ∈ Γ) we state Γ ′ = Γ\{a} and ψ ′ = ∃a. ψ. By inductive hypothesis, we can decide whether there is a joint strategy winning for the entry ⟨D ′ , Γ ′ , ψ ′ ⟩. Let us prove that ⟨D ′ , Γ ′ , ψ ′ ⟩ is a positive instance iff ⟨D, Γ, ψ⟩ is a positive instance. If there is a joint strategy F ′ for the coalition winning for the entry ⟨D ′ , Γ ′ , ψ ′ ⟩, then, for every play (C n 1 ) n , . . . , (C n k ) n in the meta game of D ′ , the assignment λ which is the limit of that play satisfy ⟨D ′ , Γ ′ , ψ ′ ⟩. Therefore, there is an infinite word u λ such that λ[a → u λ ] satisfies ψ ′ . Then we define the joint strategy F as follows. For every Player b ̸ = a, we set F b = F ′ b . For Player a, consider a configuration C such that α C a > 0. Because of the dependencies of Player a, it holds that |C (b)| = +∞ for every Player b ̸ = a. Let λ be the temporal assignment on P\{a} defined by C . We set F a (C ) = u λ . This joint strategy is winning. The converse follows the same idea: if there is F winning for the entry (D, Γ, ψ) then, the joint strategy F ′ = F ↾P\{a} is winning for the entry (D ′ , Γ ′ , ψ ′ ).

If (a /

∈ Γ) we state ψ ′ = ∀a. ψ. We then decide the instance ⟨D ′ , Γ, ψ ′ ⟩. Joint strategies for the coalition translate naturally between the two instances. If F ′ is winning for ⟨D ′ , Γ, ψ ′ ⟩, then every play in the outcome of F ′ satisfies ∀aψ. Then, by defining F (C ) = F ′ (C ↾P\a ) we define a wining strategy for ⟨D, Γ, ψ⟩. The converse is similar. ◀ F S T T C S 2 0 2 2


Xibin Lu

Jean-Marie Tarascon

Jiaqiang Huang

Perspective on commercializing smart sensing for batteries

Keywords: Batteries, Smart sensing, Fiber optic sensors, Sensor implanting, Smart batteries

The battery is an indispensable puzzle in the current roadmap towards a carbon-neutral world. With the soaring production, the battery itself is unexpectedly becoming a sustainability problem for society. Increasing attention is thus placed on the life cycle of batteries entailing the second life and recycling of batteries, relying on the monitoring of batteries' state and the classification of retired batteries by sensors. Battery sensors that decode the fundamental physical/chemical processes are thus poised to maximize the quality, reliability, lifetime, and safety of batteries and to minimize the environmental footprint. Fiber optic sensors stand out by virtue of their miniature size, insulating nature, electromagnetic immunity, and versatile sensitivities. In this Perspective, we discuss the promise and challenges of commercializing smart sensing for batteries and highlight how fiber optic sensors can synergize with paradigm shifts, including cell to pack and cell to chassis technologies.

Introduction

Batteries play a central role in reducing CO2 emissions and reaching the ultimate goal of carbon neutrality, by moderating the intermittent renewable energy and fueling the electric vehicles (EVs). Beyond these "macro-level" benefits, the sustainability of the battery itself cannot be absent if carbon neutrality is to succeed 1 . This, in turn, necessitates the life-cycle monitoring/tracking of batteries towards a circular economy 2 that entails the second life and recycling of batteries. To realize the life-cycle "battery passport" [START_REF]Proposal for a regulation of the European parliament and of the council concerning batteries and waste batteries, repealing Directive 2006/66/EC and[END_REF] , battery sensors, which decode the underlying physical/chemical processes into readable electrical/optical signals, become increasingly essential. In response, European Battery 2030+ roadmap [START_REF] Edström | Inventing the Sustainable Batteries of the Future[END_REF] initiated the integration of smart sensing into batteries in 2020 via three funding projects (INSTABAT and SENSIBAT for internal sensing, while SPARTACUS for external sensing) for monitoring paramount parameters of batteries under real-world operation.

The concept of battery sensor can trace back to 1887 by using a hydrometer for detecting the state of charge (SOC) of lead-acid batteries [START_REF] Bright | [END_REF] , that is, to "see" the remaining fuels in the tank. With the rapid expansion of battery applications and the market particularly of EVs 6 , the states of interest extend to states of health (SOH), state of power (SOP), and state of safety (SOS). To monitor these states, diverse sensors are being developed and applied in batteries, including electrochemical, electric, acoustic, and optical sensors 1 . Fiber optic sensors stand out among others thanks to their small diameter (<200 μm and thus the low invasiveness), electrical insulating nature, and immunity to electromagnetic (EM) interference. Besides, the fiber optic sensors are versatile to monitor multiple observables of batteries, including temperature 7 (T), strain 8 (ε), pressure 7 (P), refractive index 9 , and molecular fingerprints 1,10 .

The working mechanism and applications of battery sensors have been reviewed in detail previously 1 ; however, the challenges and solutions of commercializing smart sensing for batteries remain less touched. To close this gap, we firstly reiterate the importance of smart sensing for a sustainable future. To select the right sensor, we then compare different battery sensors and highlight the superiority of fiber optic sensors in real applications. Lastly, we show how the fiber sensors can be implanted into batteries of different formats in addition to their compatibility with emerging engineering designs.

Do we need smart sensing for cells?

Driven by the increasing EV penetration, the global market for lithium-ion batteries 6 reached 266 GWh in 2020 and expectedly 2,500 GWh in 2030 (Figure 1a). Whereas providing positive impacts in reducing fossil fuel burning and CO2 emission, the batteries themselves are becoming an inevitable sustainability problem [START_REF] Brudermüller | A Vision for a Sustainable Battery Value Chain in 2030[END_REF] through their life cycle from mining, production, application, and retirement. For instance, >40 GWh batteries 6 were retired in 2019 (Figure 1b) and more in the foreseeable future. To lower the life-cycle footprint of batteries, in addition to the exploitation of material eco-designs, a circular, responsible battery value chain 2 calls for "greener" application, repurposing, and retirement, which in turn depend on the reliable monitoring/sensing of batteries' states (SOC, SOH, SOP, SOS, etc.). However, the current battery diagnoses turn out to be insufficient, as witnessed by monthly reports of auto-ignitions of EVs, which subsequently lead to the high safety margins and thus the under-utilization of batteries. Besides, the difficulties in estimating the retired batteries' SOH and SOS also prevent the second life of batteries from reality. Thus, the need to increase battery sensing is clear. However, the pursuit of "sensors per cell" concept remains controversial.

Hints are provided by the trendy engineering designs of batteries with increasing capacity and dimension of the single cell, see Figure 1c,d. The cylindrical cells (mainly adopted by Tesla) have transited from 18650 to 21700 and recently to 46800, rendering higher energy and power densities 11 by reducing the dead volumes. However, the benefits come at a cost that the spatial heterogeneity of temperature and current distribution inside the cell is exacerbated, with the simulation showing the agglomerations close to the central void 11 , stressing the need for the sensing inside the cell. Besides, the enlarged cell size raises the inconsistency of cells inside a pack, pressing the necessity of sensing each cell. At the same time, the increased capacity/dimension from 18650 to 46800 (Figure 1c) makes every single cell a more expensive asset from both economical and environmental perspectives, justifying the life-cycle sensing of a single cell. The increase in cell capacity can also be seen in prismatic cells (Figure 1d, data from BYD, China), despite their flexibility in format dimensions. The increased capacity of a single cell is accompanied by the decreased cell number in the pack (Figure 1e), and the sensor number is thus reduced even under the "one sensor per cell" scheme. Fewer interrogation units can be further achieved via multiplexing the optical sensors 12 (Figure 1e, right axis), cutting the sensing cost as discussed in the next session.

In addition to complying with the larger battery design, the success of commercializing battery sensors potentially depends on the economic profitability by maximizing the quality, reliability, lifetime, and safety (QRLS) 1 of batteries. However, the extended battery lifespan may exceed the need for a 10-year use of electric vehicles, and revenues must be consolidated from other scenarios of energy storage such as vehicles to grid (V2G), building (V2B), and vehicle (V2V), where information from sensors is the basis for the energy management. Aside from EVs being the decentralized energy blocks, the repurposing of retired EV batteries into less demanding applications (e.g., grid, low-speed vehicles) further exploits the battery lifespan and again relies on the QRLS guaranteed by batteries sensors. Meanwhile, the battery sensors will benefit the classification of retired batteries into either repurposing or recycling by the life-long record, that is, "battery passport" [START_REF]Proposal for a regulation of the European parliament and of the council concerning batteries and waste batteries, repealing Directive 2006/66/EC and[END_REF] . Altogether, we argue that battery sensing will be one of the key puzzles towards increasingly economically and environmentally benign batteries (Figure 1f).

Financially, recent analyses [START_REF]Automotive Battery Sensor -Global Market Trajectory & Analytics[END_REF][START_REF]Global Automotive Battery Sensor Market: Industry Analysis and Forecast 2020 -2026: by Voltage, Communication Technology, Vehicle Type, Hybrid Vehicle and Region[END_REF] show that the global market of automotive battery sensor was about 3 billion US dollars in 2020 and was anticipated to reach nearly 6 billion US dollars by 2027. Note that this anticipation is simply based on the conventional electrical sensors, and we can expect a much stronger growth if the concepts of smart sensing and "sensor per cell" are realized. The evolution of cell number per pack (left axis) leading to reduced sensor/interrogation units (right axis). The shading indicates the uncertainties. f, Ambitions of battery sensors to reduce life cycle cost and green house gas (GHG) footprint of batteries. The data for 2020 refers to the literature [START_REF] Lander | [END_REF] , while the data for 2060 and the dashed curves are estimated to show the trend for meeting China's goals of carbon peak in 2030 and carbon neutrality in 2060.

Comparison of battery sensors

Diverse battery sensors are being explored to secure their position in the final commercialization. In this session, we briefly discuss the strengths of different sensors in detecting various physical/chemical phenomena in batteries (Figure 2). We then further compare the other critical merits for real applications, justifying the superiority of fiber optic sensors.

Electrochemical methods: Electrochemical methods lay the foundation for battery research/prototyping as well as the modern battery management system (BMS). They rely on Multiplexing the measurements of current and voltage, which diversify into coulomb counting, coulombic efficiency, open-circuit voltage, electrochemical impedance spectroscopy (EIS), and derivative curves (dQ/dV and dV/dQ). These methods are practically adopted for estimating the SOC and SOH of batteries, while being inferior in sensing other observables such as temperature and strain.

Electrical sensors (T, ε, P): Due to the incapability of electrochemical methods to sense temperature, other electrical sensors (such as thermistors 16 , thermocouples 17 , or resistance temperature detectors 18 ) appear as complements in real applications. In addition to temperature sensors, strain 19 and pressure 20 sensors have been explored to monitor the (ir-)reversible volume expansion of batteries.

Acoustics: Acoustic sensor relies on another type of electrical transducers/sensors, which convert electrical signals into mechanical waves or vice versa. Depending on the wave source, the acoustic battery sensing can be either passive 21 or active 22 , while 2D mapping 23 can be achieved via a translational platform or sensor arrays. Through the interactions (e.g., transmission, reflection) of the mechanical waves with the material, the mechanical events (e.g., cracking) or properties (e.g., modulus) of batteries can be "heard".

Fiber optics: Deviating from the above electrical sensors, fiber optic sensing exploits optical signals transmitting through optical fibers. The optical signal can be modulated through the various interactions (e.g., diffraction, absorption, and scattering) of light with matters, offering diverse sensing mechanisms.

Among them, fiber Bragg grating (FBG) stands out as a mature technology, being practically applied in other sectors (such as structural health monitoring in construction [START_REF] Udd | Fiber optic sensors: an introduction for engineers and scientists[END_REF] ). By inscribing periodic modifications on the fiber core, FBGs reflect light centering at a specific wavelength (λB = 2neffΛ, with neff and Λ being the effective refractive index of the grating and the grating period, respectively). This wavelength is sensitive to temperature, strain, and pressure variations of batteries, since these perturbations influence neff and Λ. The decoupling of the sensitivities depends on the delicate designs of implanting 7 , packaging, or sensor combinations 7 . Because these perturbations pertain to the impedance buildup, volume expansion, and side reactions, FBGs are proved to be useful in estimating the SOC [START_REF] Bae | [END_REF] and SOH 26 of batteries.

Unlike FBGs that confine the light inside the fiber core, tilted fiber Bragg grating (TFBG) frees parts of light from the core by tilting the Bragg grating. TFBGs utilize the evanescent wave penetrating into the environment, thus being additionally sensitive to the surrounding refractive index. By inserting TFBGs into the electrolyte and tracking its refractive index, we previously demonstrated 9 that TFBGs can monitor the electrolyte degradation. Besides, the turbidity of the electrolyte 9 was also detected via the optical scattering and absorptions of particles within the evanescent field. The multi-mode spectra of TFBG also offer extra ways to resolve the cross-sensitivities.

In spite of the valuable implications arising from refractive index and turbidity, the probed information is limited to particle level (0.1-10 μm) 1 , and we thus remain blind to details at the lower length scale. To overcome this limit, a more sophisticated approach to exploiting the evanescent wave lies in the fiber optic spectroscopies, including Raman 10 , infrared 1 , and those 27 using visible light. They are able to capture the fingerprints of chemical molecules (for example, via the resonant frequencies of vibrational modes in infrared spectroscopy 1 ) inside the batteries, rendering more fundamental insights into the evolutions of states.

In comparison to electrical sensors, fiber optic sensors also provide the possibility of high spatial resolutions by either multiplexing (that is, quasi-distributed) or distributed sensing technology (e.g., Rayleigh scattering sensing) 12,28 . Namely, the multiplexing of a few FBGs into a single fiber provides the capability of spatially sensing only a few discontinuous, pre-defined locations 12 , which is thus ascribed as "quasi-distributed" [START_REF] Udd | Fiber optic sensors: an introduction for engineers and scientists[END_REF] . Alternatively, we previously showed that fully distributed fiber optic sensing based on Rayleigh scattering could monitor the temperature (or strain) variations continuously along the fiber (i.e., every 0.65 mm) inside the batteries 12 . Despite the superior spatial resolution, this Rayleigh sensing technology relies on an even more expensive frequency-domain interrogator and gives a relatively low measurement repeatability 12 in comparison to the FBG technology.

Figure 2 (above the dashed line) summarizes the above discussion and qualitatively compares their sensing capabilities for battery applications. Aside from sensing capability, safety is the priority of batteries and the primary driving force for smart sensing. Turning to safety, two aspects need to be covered: (1) the additional safety risks from the sensors; (2) the added benefits from the sensors on improving the safety of batteries. As for (1), while the additional short circuits of batteries may arise from the electrical sensors, the application of tiny and insulating fiber optic sensors clearly suppress this possibility. Regarding (2), the improvements in batteries' safety depend again on the sensing capability of sensors and eventually on the way to exploit the sensing data, that is, the diagnostics/prognostics algorithms. As a pioneer exploration of FBG sensors 29 , Pinto et al. showed that FBGs exhibited rapid thermal responses to overcharging and external short circuits. Combining (1) and ( 2), we believe FBGs are a better candidate than electrical sensors, while electrochemical methods are relatively weak in detecting safety issues. Nevertheless, a fundamental study is still in need to thoroughly quantify the individual and intertwined responses of different observables (e.g., T, ε, P) to these phenomena (e.g., SOC and crack). Besides, to practically evaluate the effectiveness of smart sensing in diagnostics/prognostics, we should go for high-throughput experiments on commercial cells under diverse working conditions to acquire a large amount of data for statistical analysis as well as the training of diagnostic algorithms.

Towards commercialization, merits pertaining to the battery operation conditions should also be considered (Figure 2, below the dashed line). In high-voltage EV packs, the high voltage (up to 650 V) can shock the sensor and destroy the interrogation system if the sensor is electrically conductive. In this regard, optical fibers made of silica (or chalcogenide for infrared) are more suitable candidates owing to their insulator nature. Though appropriate insulations within the pack should be guaranteed anyway, we argue that the introduction of optical fiber will require less additional effort in insulation design. On the other hand, the optical fibers offer the possibility to sense the key locations (e.g., directly on the cell can or even within the electrode) without being limited by the insulation layer. Furthermore, the high-voltage and high-power batteries (together with convertors and motors) also induce strong electromagnetic fields, leading to the malfunction (or high noise) of electrical sensors without proper electromagnetic shielding. On the contrary, the optical fibers are electromagnetically immune, rendering better reliability.

The durability of sensors is another vital factor for commercialization; however, it has rarely been investigated. To have a preliminary idea of the durability of different sensors, we did a survey [30][31][32] on their applications in other fields, such as construction, see Figure 2. Surprisingly, it was predicted that fiber optical sensors could function for more than 20 years in civil composite applications 32 , while all the other sensor candidates also showed the potential for long-term durability (>10 years) 30,31 . In fact, we have recently shown that the TFBG sensors can function in 18650 cells for more than 1000 cycles 9 . However, we must confess that the experiments were done within one year at 25 o C and challenges are expected under real EV working conditions that combine vibration, high/low temperatures, and long duration (>10 years). Thus, we call for accelerated tests towards a careful investigation of the long-term durability of optical sensors under practical conditions.

The size of sensors is also critical for practical implementation. For example, it was reported 33 that the large-size implanted sensor not only influences the measurement accuracy but also pertains to some unwanted side effects (e.g., blocking the lithium transportation) on the batteries. We, therefore, compare the size of different sensors in Figure 2, showing that the fiber optic sensors are the finest (10 -3 to 10 0 mm) among others. Consequently, fiber optic sensors are favored in terms of sensor implantation.

• • • • • • SOH • • • • • • Thermal • • • • • • Strain • • • • • • Pressure • • • • • • Crack • • • • • • Molecules • • • • • • Safety • • • • • • Insulator • • • • • • EM interference • • • • • • Max. Durability (Year) >10 >10 >20 >20 R&D R&D
Sensor size (mm) 10 -1 to 10 2 10 -1 to 10 2 10 1 to 10 2 10 -3 to 10 0 10 -2 to 10 0 10 -1 to 10 0

Sensor cost (US$ unit -1 ) 0 10 0 to 10 2 10 0 to 10 2 10 0 to 10 1 10 1 to 10 2 R&D Interrogator cost (US$ unit -1 ) 0 to 10 4 10 0 to 10 2 10 3 to 10 4 10 2 to 10 4 10 3 to 10 4 10 4 to 10 5

Degree of appropriateness: Green, strong; Yellow, medium or to be explored; Red, weak As cost can be the primary barrier to implementing these sensing technologies, we also survey the sensor cost (US$ per unit sensor) and the interrogator cost (US$ per unit channel) via website/email/phone, see Figure 2.

Starting from the basic electrochemical methods, simply measuring the time-resolved voltage/current does not require additional sensors or equipment to nowadays BMS. These time-series data can be further utilized for derivative curves (dQ/dV or dV/dQ). However, the onboard voltage/current meters only offer relatively low accuracies 34 . Thus, the pursuit of high-precision coulombic efficiency (0.01%) measurement necessitates a customized charger costing ~4000 US$, as reported by Dahn et al. 34 . Similarly, the EIS also needs expensive potentiostats (10 3 to 10 4 US$ per unit channel) with a wide alternating current (AC) frequency range. Meanwhile, electrical T, ε, and P sensors appear as affordable add-ins (10 0 to 10 2 US$ per sensor and 10 to 10 2 US$ per interrogation channel) to the electrochemical methods. On the contrary, acoustic sensing turns out to be costly (10 0 to 10 2 US$ per sensor and 10 3 to 10 4 US$ per interrogation channel), due mainly to the high-frequency (at MHz scale) pulser and receiver 22 . Noteworthily, to achieve high accuracy, the cables of the above-mentioned electrical sensors should be delicately protected from electromagnetic interference, rendering the extra wiring design/cost compulsory.

Surprisingly, the price of FBG sensors is comparable to (10 0 to 10 1 US$ per sensor) the one of counterparts -electrical T, ε, and P sensors, thanks to the mature fabrication techniques and the pre-existing markets in other sectors. Optimistically, the FBG can be much cheaper if its mass production for battery application is realized 35 . Nevertheless, the TFBGs have a much smaller market, thus offering a higher cost of 10 1 to 10 2 US$ per sensor. Meanwhile, we cannot find commercial suppliers for chalcogenide 1 and photonic crystal fibers 10 for fiber optic spectroscopies.

The main obstacle to commercializing fiber optic sensors in batteries seems to be the expensive optical interrogator, that is, 10 2 to 10 4 , 10 3 to 10 4 , and 10 4 to 10 5 US$ per channel for FBG, TFBG, and fiber spectroscopies, respectively. However, we notice that the commercially available interrogators for FBGs are often overdesigned, exceeding the needs of battery applications. For example, the interrogators normally offer a wavelength range of ~100 nm, namely, ~10,000 o C for FBG's (with a temperature sensitivity of ~10 pm o C -1 ) 7 temperature measurement range, much surpassing the working temperature range of batteries. Thus, the downgrading of wavelength range (and/or other performance) appears to feasibly reduce the cost per channel for FBGs (Figure 3a). Note that wavelength range is just one cost-sensitive parameter of the interrogator among many others, including wavelength accuracy, wavelength repeatability, dynamic range, and acquisition frequency, etc. Some of these parameters, such as acquisition frequency, can also be downgraded for practical battery applications, since we may not need 1000 data points per second (one standard acquisition rate for interrogators) to overwhelm the data storage and processing. Alternatively, the wavelength division multiplexing (WDM, for example, by writing a few FBGs in one fiber or coupling a few single-FBG fibers via fiber couplers) or time division multiplexing (TDM, for example, by means of an optical switch to surveil each sensor one after the other) enables the sharing of one interrogator by hundreds of FBG sensors, possibly bringing the interrogation cost for each sensor possibly down to 10 0 US$ scale (Figure 3b).

Another short-term strategy for lowering the cost is to keep the optical interrogator offline with the charging station for in situ diagnosis only so that one interrogator can be shared by numerous EVs (Figure 3c). The ultimate realization of operando battery sensing will rely on the development of low-cost interrogators (Figure 3d). While the low-cost fiber charge-coupled detector (CCD) interrogator [START_REF] Askins | Instrumentation for interrogating many-element fiber Bragg grating arrays[END_REF] is an available option in the short term by compromising the resolution, the success of silicon photonic integration 37 will offer a compact, low-cost, and possibly high-resolution on-chip interrogator for the onboard sensing. In this direction for battery applications, PARC has already done some pioneering work by exploring the low-cost and compact interrogation readouts 35,[START_REF] Schuh | High-resolution, high-frequency wavelength shift detection of optical signals with low-cost, compact readouts[END_REF] . Besides, interrogators in the size of a memory stick are also being developed [START_REF]The Smallest Possible Spectrometer[END_REF] .

In short, all the sensors offer different sensing capabilities. We thus expect that two or three different sensors will combine together to provide an encompassing tracking of batteries' life cycle. Among them, the electrochemical method will remain as the foundation, while we modestly suggest that versatile fiber optic sensors that are immune to electrical shock and electromagnetic interference are the future complements, provided that the costs of sensor and interrogation system are reduced by the cross-disciplinary engineering/scientific innovations together with the mass production.

Implanting fiber optic sensors

If fiber optic sensors are selected from various battery sensors, the immediate question is how to exploit their added values by optimizing the positioning in batteries. The intuitive answer will be either the spatial mapping by a large number of sensing points or locating sensors at observables' (temperature, strain, etc.) maxima. The spatial mapping can be achieved by fully distributed (e.g., Rayleigh) 12 or quasi-distributed (e.g., FBG multiplexing) fiber optic sensing but at a relatively high cost. On the contrary, the key-point sensing, requiring much fewer sensor points and thus lower cost, seems closer to the practical applications. One controversy for key-point sensing is whether the fibers should be implanted into the cell, where the true maxima are located 7,11 . In current cell designs, the ingress of fiber inevitably brings about invasiveness (though small due to the diameter of the fiber, <200 μm) and the extra sealing, pertaining to additional cost and risk of leakage. To escape from the invasiveness, the positioning of sensors on the surface of the cells may be the first step for commercializing fiber optic sensing technologies into batteries. However, maximizing the benefits of fiber optic sensing should ultimately be realized by implanting the sensors into the cells. We thus discuss the implanting positions and the sealing methods in different cell formats in Figure 4.

In cylindrical cells, the central voids of jelly rolls, that are formed during the fabrication, are ideal accommodations for optical fibers (Figure 4a); see our previous papers 7,9,12 . Particularly, the central positions are the hot spots of the cylindrical cells, as evidenced by the experiment 7 /simulation 11 . Free from strain, the FBG sensors hosted in the central voids can unambiguously sense temperature 7,12 without cross-sensitivity issues. In conjunction with an additional FBG inscribed in microstructured optical fibers, hydraulic pressure resulting from the gas buildup can also be detected 7 . While using TFBGs in the central void, temperature, refractive index, and turbidity of the electrolyte can be decoupled by a single sensor 9 . To further sense the stress concentration, the fibers need to be implanted between jelly roll layers 35 or even embedded into the electrode 8,[START_REF] Bae | [END_REF] . However, the ways to decouple the temperature and strain of FBG sensors should be further explored.

In pouch/prismatic cells with flat jelly rolls or stacking layers, the fiber sensors can be placed at the cell center between the layers 35 (Figure 4b), which is possibly the hot spot of the cell [START_REF] Lin | [END_REF] . Similar to the cylindrical cells, the decoupling of temperature and strain can be complicated when implanting the sensors between layers. In the worst case, the coupled signal can still serve as a valuable input for battery management. Another interesting sensing position lies in ultrasonic or laser welded points between the tabs and positive/negative electrodes, where the interface/contact resistances may contribute to a hot pot 41 . On the other hand, a higher stress concentration is witnessed in the wound jelly roll structures than in the stacking ones 42 , particularly at the corner (Figure 4b). Consequently, implanting one fiber sensor inside the wound corner may offer critical implications for the cell's mechanical degradation. However, we should be aware of the possibility that the implanting of the fiber sensor may aggravate the stress concentration, and the impact of implanting needs to be assessed and minimized carefully. In addition, the single cell can consist of multiple jelly rolls (see Apple's patent [START_REF] Bhardwaj | Battery with multiple jelly rolls in a single pouch[END_REF] ). The sensors at the interface (Figure 4b) may monitor the interplay between jelly rolls.

After the implanting, the ports to inject the fibers should be closed by sealants (Figures 4c-e). In cylindrical cells (Figure 4c), epoxy sealants are adopted and show reliability under mild conditions (55 o C or gassing) in lab scale 7,9,12 . However, epoxy may fail under EV operation conditions combining vibration, high/low temperatures, and gassing inside the batteries. Further testing and screening of sealants are thus necessary for the long-term reliability of the battery sensing. The same sealant can be used for prismatic cells, while the electrolyte filling port may simultaneously serve as the sensor injection port (Figure 4d). This, in turn, calls for the integrated design of sensors and cells with at least the pre-formed fiber ingress ports. The sensor sealing in the pouch cell may be much readier, because the protruding fiber is similar to the tabs and can be readily sealed with the assistance of heat seal film (Figure 4e) as reported by PARC 35 . Note that the optical signals can be collected by reflection and transmission modes 44 , requiring one and two ports, respectively. One port and thus the reflection mode is indeed desired for fewer sealing points.

The emerging engineering designs, including cell to pack (CTP) and cell to chassis (CTC), may provide new opportunities for battery sensing. Note that the previous thermal sensors (e.g., thermistors) are generally placed at the module level, and the elimination of the module in CTP may push the battery sensors to the cell level. BYD's gravimetrical CTP (GCTP) technology is based on the "blade" (characteristic of its thin but long dimension) battery (Figure 4f, left). The unique geometry of "blade" batteries may induce temperature gradients, and the implanting multiplexed sensors along the longitudinal direction can be interesting. While in CTC, the batteries become bi-functional, serving as both energy storage and structural components (Figure 4f, right). Recall that fiber optic sensors have been widely applied in structural health monitoring [START_REF] Udd | Fiber optic sensors: an introduction for engineers and scientists[END_REF] in the construction sector, and thus bi-functioning of optical sensors for battery and structural sensing is readily feasible (Figure 4f, right). Aside from batteries, fiber optic sensors are increasingly explored for monitoring other components in EVs, such as tires [START_REF] Breglio | Proceedings of the World Congress on Engineering 2017[END_REF] . Thus, a conjoined, versatile optic platform in EVs can be envisaged. The monitoring of batteries at cell/system level by fiber optic sensors is exemplified in Figure 4. Thanks to the versatility of sensors, a multiscale operando monitoring of batteries is further envisioned (Figure 5). For example, at the electrode level, PARC has embedded the FBG sensors into the graphite electrodes of a pouch cell [START_REF] Bae | [END_REF] , while we have recently demonstrated the operando tracking of the stress evolution at the interfaces and electrodes of solid-state batteries 8 . Taking advantage of the evanescent field, we exploited the refractive index and turbidity of electrolyte 9 within the field (with a depth of 0.1-10 μm) at the particle level, and further investigated the chemical species (or functional groups) of electrolytes by the fiber infrared spectroscopy 1 at molecular level. Though promising, the simultaneous realization of multiscale monitoring is technically challenging, and we thus proposed the "lab-on-fiber"

Outlook

In this Perspective, we demonstrate the opportunity and challenges of commercializing smarting sensing into batteries for a more sustainable, carbon-neutral world. Significant work remains to integrate the fibers, reduce the cost, and maximize the benefits of fiber optic sensors. In the short term, a demo battery pack consisting of optical sensors is desired to explore the wiring of fibers, the communication with battery management systems, and to quantify the added values of the optical sensors. In the long term, the fruitfulness of battery sensors will rely on the various actors from cross-disciplinary fields throughout both academia and industry.

Figure 1 |

 1 Figure 1 | Sensors for cells. a, The anticipated global market of lithium-ion batteries 6 . b, The capacity of retired lithium-ion batteries 6 . c,d, The evolutions of capacity and dimension of cylindrical (c) and prismatic (d) cells with lines as a guide to the eyes. The data is retrieved from the media releases from Tesla and BYD. The formats of prismatic cells in (d) include 356×100×28, 420×109.5×39, 416×146×58, 960×90×13.5 mm 3 , from left to right. e,

Figure 2 |

 2 Figure 2 | Benchmark of various battery sensors with respect to merits that are key for commercialization in batteries. Although it is subjective and prone to overestimation or underestimation, some battery sensors are clearly best-suited to capture specific phenomena. Note that the data of cost is surveyed by website/email/phone with mainly Chinese suppliers.

Figure 3 |

 3 Figure 3 | Reducing the cost of interrogation. a, Downgrading the wavelength range of interrogator. b, Wavelength division multiplexing of multiple optical sensors in a single interrogation channel. c, Stationary interrogator for sharing the interrogation cost. d, Low-cost interrogators by fiber-CCD interrogator 36 and on-chip interrogator 37 .

Figure 4 |

 4 Figure 4 | Implanting fiber optic sensors. a,b, Sensor positions in cylindrical (a) and flat jelly rolls (b, taking a single cell with two jelly rolls as an example) for the pouch and prismatic cells. c-e, Sensor sealing in cylindrical (c), prismatic (d), and pouch (e) cells. f, Integrating optical sensor with new engineering designs, including cell to pack (CTP, left) and cell to chassis (CTC, right).

Figure 5 |

 5 Figure 5 | Monitoring of batteries by fiber optic sensor at different length scales.

Acknowledgement

This work was supported by the Hong Kong University of Science and Technology (Guangzhou) startup grant (G0101000062) and the Project of Hetao Shenzhen-Hong Kong Science and Technology Innovation Cooperation Zone (HZQB-KCZYB-2020083). We acknowledge BATTERY 2030+ funded by the European Union's Horizon 2020 research and innovation program under grant agreement No. 957213, and the funding from the International Balzan Prize Foundation via the 2020 Balzan Prize to Jean-Marie Tarascon. We are also indebted to Fan SHI (HKUST), Xiang ZHENG (CALB), Yabin ZHOU (LUNA), Fu LIU (CdF) for the fruitful discussion.

Declaration of interests

A patent related to the work has been filed.