Patricia Bouyer Lsv

A Note on Game Theory and Verification

We present some basics of game theory, focusing on matrix games. We then present the model of multiplayer stochastic concurrent games (with an underlying graph), which extends standard finite-state models used in verification in a multiplayer and concurrent setting; we explain why the basic theory cannot apply to that general model. We then focus on a very simple setting, and explain and give intuitions for the computation of Nash equilibria. We then give a number of undecidability results, giving limits to the approach. Finally we describe the suspect game construction, which (we believe) captures and explains well Nash equilibria and allow to compute them in many cases.

Introduction

Multiplayer concurrent games over graphs allow to model rich interactions between players. Those games are played as follows. In a state, each player chooses privately and independently an action, defining globally a move (one action per player); the next state of the game is then defined as the successor (on the graph) of the current state using that move; players continue playing from that new state, and form a(n infinite) play. Each player then gets a reward given by a payoff function (one function per player). In particular, objectives of the players may not be contradictory: those games are non-zero-sum games, contrary to two-player games used for controller or reactive synthesis [START_REF] Thomas | Infinite games and verification[END_REF][START_REF] Henzinger | Games in system design and verification[END_REF].

Using solution concepts borrowed from game theory, one can describe the interactions between the players, and in particular describe their rational behaviours. One of the most basic solution concepts is that of Nash equilibria [START_REF] Nash | Equilibrium points in n-person games[END_REF]. A Nash equilibrium is a strategy profile where no player can improve her payoff by unilaterally changing her strategy. The outcome of a Nash equilibrium can therefore be seen as a rational behaviour of the system. While very much studied by game theoretists (e.g. over matrix games), such a concept (and variants thereof) has been only rather recently studied over games on graphs. Probably the first works in that direction are [START_REF] Chatterjee | On Nash equilibria in stochastic games[END_REF][START_REF] Chatterjee | Games with secure equilibria[END_REF][START_REF] Ummels | Rational behaviour and strategy construction in infinite multiplayer games[END_REF][START_REF] Ummels | The complexity of Nash equilibria in infinite multiplayer games[END_REF].

Computing Nash equilibria requires to (i) find a good behaviour of the system; (ii) detect deviations from that behaviour, and identify deviating players (called deviators); (iii) punish them. Variants of Nash equilibria (like subgameperfect equilibria, robust equilibria, etc) require slightly different ingredients, but they are mostly of a similar vein.

In this note, we first recall some basics of game theory over matrix games. Those games are not sufficient in a verification context: indeed, explicit states are very useful when modelling systems or programs, but are missing in matrix games. However stability notions like Nash equilibria or other solution concepts borrowed from game theory, are very relevant. We thus present the model of concurrent multiplayer games (played on graphs), which extends in a natural way standard models used in verification with multiplayer interactions. We explain how Nash equilibria can be characterized and computed in such general games. The ambition of this note is not to be a full survey of existing results, but rather to give simple explanations and intuitions; it gives formal tools to characterize and compute them and should help understanding simple interactions like Nash equilibria in rich games played on graphs.

Related notes are [START_REF] Thomas | Infinite games and verification[END_REF], which discussed the use of two-player zero-sum games in verification, and [START_REF] Grädel | Solution concepts and algorithms for infinite multiplayer games[END_REF], which discussed solution concepts in multiplayer turnbased games on graphs.

Notations. If Σ is a finite alphabet, then Σ + (resp. Σ ω ) denotes the non-empty finite words (resp. infinite words) over Σ. If Γ is a finite set, then we note D(Γ ) the set of probability distributions over Γ . We write R for the set of real numbers.

Basics of game theory

In this section we present basic notions from game theory, which will be useful for our purpose. We refer the interested reader to the textbook [START_REF] Maschler | Game Theory[END_REF].

A matrix game (aka game in strategic form) is a tuple G = (P , Σ, (payoff A ) A∈P ) where P = {A 1 , . . . , A k } is a finite set of players, Σ is a finite set of actions, and for every A ∈ P , payoff A : Σ P → R is a payoff (or utility) function for player A. In a deterministic setting, such a game is played as followed: independently and simultaneously, each player selects an action, resulting in a move (an element of Σ P ), and each player gets the payoff specified in the game for that move. In a stochastic setting, each player selects a distribution over the actions, resulting in a distribution over the set of moves and an expected value for the payoff.

A pure strategy for player A ∈ P is the choice of an action σ A ∈ Σ, while a mixed strategy for player A is a distribution σ A ∈ D(Σ) over the set of possible actions. Obviously, a pure strategy is a specific case of a mixed strategy where only Dirac probability distributions can be used. We let σ = (σ A ) A∈P be a (pure or mixed) strategy profile (that is, for every A ∈ P , σ A is (pure or mixed) strategy for player A). The probability of a move m = (a A ) A∈P ∈ Σ P is written σ(m) and defined by:

σ(m) = A∈P σ A (a A )
Then, given a player B ∈ P , the payoff of player B is given by the expected value of payoff B under σ, that is:

E σ (payoff B ) = m∈Σ P σ(m) • payoff B (m)
Example 1 (The prisoner's dilemna). Two individuals have committed a crime and are apprehended. The prosecution lacks sufficient evidence to convict the two individuals on the principal charge, but they have enough to convict both on a lesser charge. The prosecutors offer each prisoner a bargain: without any communication between them, the two individuals are offered the opportunity to Betray the other by testifying that the other committed the crime and get (partly) immunity, or to stay Silent. The payoff of both players is summarized in the table below, where the higher is the payoff the shorter is the jail penalty:

A 2 S B A 1 S 2, 2 0, 3 B 3, 0 1, 1
In each cell of the

A 2 L R A 1 T 0, 0 2, 1 B 3, 2 1, 2
Note that in this game (and in several examples in the note), for more readability, we take w.l.o.g. different alphabets for the players.

Example 3 (Matching penny game). The game is a two-player game, where each player has two actions, a and b. This is a zero-sum game (that is, the sum of the two payoffs in each situation is 0): the first player wins (payoff +1) if the two chosen actions are matching, whereas the second player wins if the two actions are different. The payoffs are summarized below:

A 2 a b A 1 a +1, -1 -1, +1 b -1, +1 +1, -1
The study of multiplayer games is to understand the rational behaviours of the players, assumed to be selfish. For instance, if for a player A, one of her strategy σ A dominates another strategy σ A (in the sense that for all strategies of the other players, the payoff is larger using σ A than using σ A ), then there is no situation where player A should play σ A . This is for instance the case in the prisoner's dilemna (Example 1), where action B dominates action S. Hence, the only rational issue in this example is that both players play action B, yielding a payoff of 1 for each. One realizes however that it would be much better for them to both play S, but the threat that the other betrays (plays action B) makes that solution unsafe.

In the game of Example 2, action R (weakly) dominates action L for player A 2 (in the sense, it is better than or equally good), hence playing R for player A 2 is safe; knowing that, player A 1 will play action T; hence, a priori, the only rational issue of this game should be the profile (T, R) with payoff (2, 1). However, one also realizes that the profile (B, L) would be much better for both players, so only looking at dominating strategies might be too restrictive.

Finally, there might be no dominating strategies in a game, like in the matching penny game (Example 3), so other solution concepts have to be considered.

One of the most famous solution concepts for rationality is that of Nash equilibrium [START_REF] Nash | Equilibrium points in n-person games[END_REF]. Let σ be a strategy profile. If A ∈ P is a player, and σ A is a strategy for A (called a deviation), then σ[A/σ A ] is the strategy profile such that A plays according to σ A and each other player B ∈ P \ {A} plays according to σ B . Later, we write -A for the coalition of all the players except player A, that is, -A = P \ {A}.

A mixed (resp. pure) Nash equilibrium in game G is a mixed (resp. pure) strategy profile σ = (σ A ) A∈P such that for every A ∈ P , for every player-A mixed (resp. pure) strategy σ A ,

E σ [A/σ A ] (payoff A ) ≤ E σ (payoff A )
Note that even for mixed profiles, it is sufficient to look for pure deviations (if a mixed deviation improves the payoff, then so will do a pure deviation). Let σ be a strategy profile and σ A be a deviation for player A such that E σ [A/σ A ] (payoff A ) > E σ (payoff A ), then it is a profitable deviation for player A w.r.t. σ . If such a profitable deviation exists, then the profile is not a Nash equilibrium.

Coming back to the prisoner's dilemna (Example 1), the pair of pure dominating strategies (B, B) is a pure Nash equilibria, whereas the pair (S, S), which would yield a better payoff for both players, is not a Nash equilibrium.

In the matching penny game (Example 3), it is not difficult to check that none of the pure strategy profiles can be a Nash equilibrium since in each case, one of the players would benefit from switching to the other action. Also, one can argue that there is a unique Nash equilibrium, where each player plays each action uniformly at random, yielding an expected payoff of 0 for both.

Finally in Example 2, the two profiles (T, R) and (B, L) are the two Nash equilibria of the game. So there might be several Nash equilibria in a game, yielding possibly different payoffs.

A Nash equilibrium expresses a notion of stability. Indeed, it can be seen that a Nash equilibrium σ = (σ A ) A∈P is such that each strategy σ A is the bestresponse to the strategies (σ B ) B∈ -A of her adversaries. Formally, let S (resp. S A , S -A ) be the set of mixed strategy profiles (resp. strategies for player A, strategies for coalition -A ). For every σ ∈ S, let

BR(σ) = σ ∈ S | ∀A ∈ P , σ A ∈ argmax σ A ∈S A E σ[A/σ A ] (payoff A )
be the set of best-response strategy profiles for σ. Then, σ is a Nash equilibrium if and only if σ ∈ BR(σ).

We state now the famous Nash theorem [START_REF] Nash | Equilibrium points in n-person games[END_REF], which is one of the important milestones in the game theory domain.

Theorem 1 (Nash theorem). Every matrix game has a (Nash) equilibrium in mixed strategies.

The original proof of Nash uses Brouwer's fixed point theorem (see below). However it can also be seen that it is a consequence of Kakutani's fixed point theorem (see below), by taking BR as function f (since the set mixed strategy profiles can be seen as a convex subset of

[0, 1] |P |•|Σ| ).
Theorem 2 (Brouwer's fixed point theorem). Let X ⊆ R n be a convex, compact and nonempty set. Then every continuous function f : X → X has a fixed point.

Theorem 3 (Kakutani's fixed point theorem). Let X be a non-empty, compact and convex subset of R n . Let f : X → 2 X be a set-valued function on X with a closed graph and the property that f (x) is non-empty and convex for all x ∈ X. Then f has a fixed point.

As a final remark, let us define the minmax value of player A ∈ P as

v A = min (σ B ) B∈ -A ∈S -A max σ A ∈S A E σ (payoff A )
where σ = (σ B ) B∈P . This is the best player A can achieve, when she does not know how the other players will play. We will not discuss the minmax value, the maxmin value and the value of a game, but we notice that for every Nash equilibrium σ ∈ M P , E σ (payoff A ) ≥ v A (since otherwise the strategy giving the minmax value will be a profitable deviation).

Conclusion.

Game theory is a very rich field of research, of which we have only given few hints on the basic concepts, which will be relevant for the use in verification. We refer again to the textbook [START_REF] Maschler | Game Theory[END_REF] for an entry point to this research domain. Matrix games represent a "one-shot" interaction between the players. In system or program verification, players may represent components or controllers; it is usually useful to allow models with states for such systems, and to consider temporal behaviour of such systems. Hence the interaction is the result of a dynamic process, and not of a one-shot interaction like in matrix games. This is not specific to verification, and towards that goal, more complex interactions have been studied under the names of extensive-form games (games are then played on a tree), or repeated games (a given matrix games is a large number of times). There are many elegant results on these systems, but this note is not sufficient for this purpose.

Matrix games and extensions like repeated games are not adapted to study interaction between players in a verification context. Indeed, to represent systems or programs, it is very useful to have models with explicit states. We will therefore first present the model of games on graphs that we will consider, and then argue why those games cannot be solved using the standard well-understood theory that we have recalled. We will then give some results and ideas for the computation of Nash equilibria in such games.

Definition of the general model and of the problems of interest

We consider the model of concurrent multi-player games, based on the two-player model of [START_REF] Alur | Alternating-time temporal logic[END_REF], and extended with probabilities. The deterministic version of this model was used for instance in [START_REF] Bouyer | Pure Nash equilibria in concurrent games[END_REF].

Definition 1. A multiplayer stochastic concurrent game is a tuple G = (V, v init , P , Σ, δ, (payoff A ) A∈P )
where V is a finite set of vertices, v init ∈ V is the initial vertex, P is a finite set of players, Σ is a finite set of actions, δ : V × Σ P → Dist(V ) associates, with a given vertex and a given action tuple (called move) a distribution over the possible target vertices, and for every

A ∈ P , payoff A : V ω → R is a payoff function. We later write v m -→ v whenever δ(v, m)(v ) > 0.
As before, we assume an explicit order on P = {A 1 , . . . , A k }. Also, given a player A ∈ P , we write -A for the coalition P \ {A}. An element m = (m A ) A∈P ∈ Σ P is called a move, and we may write it as (m A1 , . . . , m A k ). If m ∈ Σ P and A ∈ P , we write m(A) for the A-component of m and m -A for all but the A components of m. In particular, we write m(-A) = m (-A) whenever m(B) = m (B) for every B ∈ -A . Also, if m ∈ Σ P , B ∈ P and a ∈ Σ, then m[B/a] denotes the move m such that m (-B) = m(-B) and

m(B) = a. A history π in G is a finite non-empty sequence v 0 v 1 . . . v h ∈ V + such that for every 1 ≤ i ≤ h, there is m i ∈ Σ P with v i-1 mi --→ v i .
We write last(π) for the last vertex of π (i.e., v h ). If i ≤ h, we also write π ≤i for the prefix v 0 v 1 . . . v i . We write Hist(v 0 ) for the set of histories in G that start at v 0 . Notice that histories do not record moves used along a history.

We extend above notions to infinite sequences in a straightforward way and to the notion of play. We write Plays(v 0 ) for the set of full plays that start at v 0 .

Let A ∈ P be a player. A randomized (or mixed) strategy1 for player A from v 0 is a mapping σ A :

Hist(v 0 ) → Dist(Σ). An outcome of σ A is a(n infinite) play ρ = v 0 v 1 . . . such that for every i ≥ 0, writing m i (A) = σ A (ρ ≤i ), v i mi --→ v i+1 .
We write out(σ A , v 0 ) for the set of outcomes of σ A from v 0 . A pure (or deterministic) strategy for player A is a mixed strategy σ A such that for every history h, σ A (h) is a Dirac probability measure (that is, it associates to some vertex v a probability 1, and to other vertices a probability 0).

A mixed (resp. pure) strategy profile is a tuple σ = (σ A ) A∈P , where, for every player A ∈ P , σ A is a mixed (resp. pure) strategy for player A. We write out(σ, v 0 ) for the set of plays from v 0 , which are outcomes of all strategies part of σ. Note that if σ is pure, then out(σ, v 0 ) has a single element, hence we may abusively speak of the outcome out(σ, v 0 ).

Note that strategies, as defined above, can only observe the sequence of visited states along the history, but they may not depend on the exact distributions chosen by the players along the history, nor on the actual sequence of actions played by the players. Notice that this model is more general than the model where actions are visible, which are sometimes considered in the literature-see for instance [START_REF] Ummels | The complexity of Nash equilibria in infinite multiplayer games[END_REF] and [START_REF] Bouyer | Nash equilibria in concurrent games with Büchi objectives[END_REF]Section 6] or [START_REF] Chatterjee | Partial-observation stochastic games: How to win when belief fails[END_REF] for discussions-and the results presented here are valid (though actually simpler) when considering visible actions.

When σ is a strategy profile and σ A a player-A strategy, we write σ[A/σ A ] for the strategy profile where A plays according to σ A , and each other player B plays according to σ B . The strategy σ A is a deviation of player A, or an A-deviation.

Once a strategy profile σ = (σ A ) A∈P is fixed, for every v 0 ∈ V it standardly induces a probability measure P σ v0 over the set of plays from v 0 in the game G, by defining probability of cylinders as described below, and by extending it in a unique way to the generated σ-algebra. For every history π = v 0 v 1 . . . v h ∈ Hist(v 0 ), we let Cyl (π) = {ρ ∈ Plays(v 0 ) | π is a prefix of ρ} and we define P σ v0 Cyl (v 0 ) = 1, and then inductively

P σ v0 Cyl (πv h+1 ) = P σ v0 Cyl (π) •        m∈Σ P v h m -→v h+1 σ(π)(m) • δ(v h , m)(v h+1 )        where σ(π)(m) = A∈P σ A (π)(m A )
is the probability that move m is selected by strategy profile σ.

Let f be a measurable function in the σ-algebra generated by the cylinders above. Then we define its expected value w.r.t. P σ v0 in a standard way, and denote it E σ v0 (f ). We will therefore assume that payoff functions payoff A (A ∈ P ) are all measurable!

The notion of Nash equilibrium that we have defined on matrix games extends naturally to games over graphs. Definition 2. A Nash equilibrium from v init is a strategy profile σ such that for every A ∈ P , for every player-A deviation σ A ,

E σ [A/σ A ] v init (payoff A ) ≤ E σ v init (payoff A ) Note that if σ is a pure profile, then E σ v init (payoff A ) = payoff A (out(σ, v init ))
. Also in this case, out(σ, v init ) is called the main outcome of equilibrium defined by σ.

As in matrix games, given a profile σ , a deviation σ A for player A such that

E σ [A/σ A ] v init (payoff A ) > E σ v init (payoff A
) is called a profitable deviation for player A.

Payoff functions. A property φ over V ω is said prefix-independent whenever for every ρ, ρ |= φ if and only if for every suffix ρ of ρ, ρ |= φ.

We say that a payoff function payoff : V ω → R is given by a Boolean property φ over V ω whenever payoff(ρ) = 1 if ρ |= φ, and payoff(ρ) = 0 if ρ |= φ. Usually, φ will be some specific types of properties, like reachability, safety. We then abusively say payoff is a reachability (resp. safety, . . . ) objective. In a stochastic game, the expected value of such a payoff function is the probability to satisfy the property φ.

A payoff function payoff over V ω is said terminal-reward if there is some designed subset V ⊆ V such that all vertices of V are sinks in the graph of the game, and a function w : V → R such that for every ρ ∈ V ω , payoff(ρ) = w( v) if ρ visits vertex v ∈ V (which is unique if it exists since it is a sink), and payoff(ρ) = 0 otherwise. A particular case is when the image of w is included in {0, 1}, in which case we speak of terminal-reachability.

Subclasses of games. We use the following subclasses of games. Game G is said:

turn-based whenever there is a function J : V → P such that for every v ∈ V , for every m, m ∈ Σ P , m(J(v)) = m (J(v)) implies δ(v, m) = δ(v, m ); deterministic whenever for every v ∈ V and m ∈ Σ P , δ(v, m) is a Dirac probability measure on some vertex.

The existence and the constrained existence problems. For verification purposes, even if the existence of a Nash equilibrium might be interesting (due to the link with a stability property), we will also be interested in the constrained existence problem, and in the computability of Nash equilibria when they exist.

The constrained existence problem asks, given a stochastic multiplayer concurrent game G = (V, v init , P , Σ, δ, (payoff A ) A∈P ) and a predicate P over R |P | , whether there exists a Nash equilibrium σ such that E σ v0 (payoff A )

A∈P ∈ P .
Of course, for computability matters, predicates should not be too complicated, but one might think of lower bounds on the expected payoffs, or constraints on the social welfare (that is, the sum of the payoffs of all the players), etc. The existence problem is just the same problem when the predicate is R P . We add "pure" to the name of the problem if we restrict to pure strategy profiles.

Example 4 (Hide-or-run game). We consider the hide-or-run game represented on Figure 1 (left). There are three vertices and two players A 1 and A 2 . The actions for player A 1 are shoot (the snowball) and wait while the actions for player A 2 are hide and run. Strings sh, wr, wh and sr represent all possible moves in the game. In vertex v 0 , if player A 1 plays action s and player A 2 plays action h, then the game proceeds to vertex v 1 . Actions from v 1 and v 2 are irrelevant hence omitted in the figure. Pairs of numbers close to each vertex represents a weight for each player. The payoff function for each player will be the mean-payoff along the play of all encountered weights. In this game, player A 1 wants to hit player A 2 with a (single) snowball. Player A 1 can therefore either shoot the ball or wait, while Player A 2 can hide (in which case she is not hit by the snowball) or run (in which case she is hit by the snowball if it is shot at the same time. Payoffs are assigned according to the satisfaction of the two players (payoff 2 when the player is satisfied and 0 otherwise). Note that the pair wh forever is only half-satisfactory for both players, hence a payoff of (1, 1).

One realizes that there is no Nash equilibrium in the hide-or-run game: indeed, if the probability of playing wh forever from v 0 (resp. of playing sr from v 0 ) is positive, then player A 2 can deviate and get a better payoff; conversely, if the probability of playing wr (resp. sh) from v 0 is positive, then player A 1 can deviate and get a better payoff.

The game of Figure 1 (on the right) is a slight modification of the previous game, with a terminal-reachability payoff: if the game ends up in the bottom-left vertex (formerly v 1 ), then the payoff is (0, 2), while it is (2, 0) if the game ends up in the bottom-right vertex of the game (formerly v 2 ). It is very similar to the first game, the only difference is that playing wh forever yields a payoff of (0, 0) instead of (1, 1) previously. This slight modification yields a pure Nash equilibrium in the game, which is to play sh from v 0 .

Why does the standard theory not apply?

While matrix games are obviously special cases of our general model, one may nevertheless wonder why the standard theorems would not apply in this general model. We first realize that Nash theorem (stated as Theorem 1) does not apply: there are indeed potentially infinitely many pure strategies.

As we mentioned earlier, the proof of Nash theorem can be seen as a direct application of Kakutani's fixed point theorem (recalled as Theorem 3), which is in a much more general setting than its application to Nash theorem. We explain how this theorem can apply in some cases, but why it does not apply in our precise setting. A stationary strategy σ is a mixed strategy such that for every h, h ∈ Hist(v 0 ), last(h) = last(h ) implies σ(h) = σ(h ). Such a strategy can therefore be viewed as an element R N for some integer N (one value for each triple (v, a, A i ) ∈ V × Σ × P ). The subspace X of R N of stationary strategies satisfies the hypotheses of the theorem. As we have already discussed in matrix games, a Nash equilibrium σ is such that each of its components is a best response to the other strategies. When restricted to stationary strategies, the best-response function can be defined as (we keep the same notations S and S A ):

BR(σ) = σ ∈ S | ∀A ∈ P , σ A ∈ argmax σ A ∈S A E σ[A/σ A ] v0 (payoff A )
Nevertheless, over game graphs, continuity of this best-response function is not ensured (hence the graph of BR is not closed). Let us consider for example game of Figure 2 (borrowed from [START_REF] Bouyer | Stochastic equilibria under imprecise deviations in terminal-reward concurrent games[END_REF]). It is assumed to be turn-based (vertex v i belongs to player A i ): from v i , player A i can easer continue or leave the game. A stationary strategy profile σ can be stored as a pair (σ

A1 (v 1 )(l), σ A2 (v 2 )(l)) ∈ [0, 1] 2 ,
where the first (resp. second) element is the probability that player A 1 (resp. A 2 ) leaves the game from v 1 (resp. v 2 ). If one player decides to leave the game with some positive probability, the other player has all incentive to purely continue the game, until eventually reaching the terminal state (with probability 1). Hence BR((x, y)) = {(0, 0)} for every x, y > 0. However, if one player purely continues the game, the only way to win some positive payoff 1 3 is to leave the game with positive probability. Hence BR((0, 0)) = {(x, y) | x, y > 0}. We conclude that the graph is not closed, so Theorem 3 cannot be applied to the classical BR function. We finally notice that any profile (x, 0) with x > 0, or (0, y) with y > 0, is a Nash equilibrium. Though this theorem does not apply in our general context, it can be used in others, for instance for stay-in-a-set games [START_REF] Secchi | Stay-in-a-set games[END_REF], for Nash equilibria with discounted payoffs or -Nash equilibria [START_REF] Chatterjee | On Nash equilibria in stochastic games[END_REF].

Discussion on a simple scenario

Let us focus on a simple scenario first. We fix for the rest of this subsection a game G = (V, v init , P , Σ, δ, (payoff A ) A∈P ) which satisfies the following (restricting) assumptions:

the game is turn-based and deterministic; for every A ∈ P , the payoff function payoff A is given by a Boolean prefixindependent objective φ A ;

We note ( †) the hypotheses of this simple scenario.

For every A ∈ P , we let G[A] be the two-player zero-sum game built on the same arena as G, where A plays against coalition -A (more precisely, all vertices which previously belang to some B ∈ P \ {A} now belongs to -A , and all vertices which previously belang to A still belongs to A); the payoff function for A is payoff A , while the payoff function for -A is -payoff A (here, in our simple setting, the objective of player A is φ A while the objective of -A is ¬φ A ). Let W -A (resp. W A ) be the set of winning states for coalition -A (resp. player A) in this game. Since this game is turn-based and the objectives are prefix-independent, the game will be determined, that is, either A has a winning strategy, or the coalition -A has a winning strategy (that is, for every vertex v ∈ V , either v ∈ W A or v ∈ W -A ). Furthermore, for large classes of objectives, the set W -A (or W A ) can be computed. We report here to the whole literature on the subject, see [START_REF] Grädel | Automata, Logics, and Infinite Games: A Guide to Current Research[END_REF] for an entry point.

One can then characterize pure Nash equilibria by the formula:

Φ NE = A∈P ¬φ A ⇒ GW -A
borrowing notations from the syntax of LTL [START_REF] Pnueli | The temporal logic of programs[END_REF]: that is, Φ NE holds along a play ρ whenever for every A ∈ P , either φ A holds along the outcome or A cannot enforce winning anywhere along the play (or equivalently, -A can enforce ¬φ A in G[A]). Note that the same formula can be used for reachability objectives but that a slightly different one has to be used for safety objectives. One can show:

Proposition 1. Assume setting ( †). Let ρ ∈ Plays(v init ). Then, ρ |= Φ NE if and only if there is a Nash equilibrium σ from v init such that out(σ, v init ) = ρ.
Proof (Sketch). Indeed, pick a play ρ ∈ Plays(v init ), and assume that ρ |= Φ NE . Consider a player A ∈ P . Such a player may have some interest in deviating only if her objective φ A is not already satisfied by ρ. In that case, she has a profitable deviation after some prefix π of ρ if she is able to ensure winning after π. In particular, if no winning state of A is visited along ρ, then ρ can be completed into a Nash equilibrium as follows:

all players play along ρ;

as soon as a player deviates from ρ, then the coalition -A = P \ {A} starts playing a counter-strategy to A. Such a strategy is sometimes called a threat or a trigger strategy.

Conversely assume there is a Nash equilibrium σ from v init such that out(σ, v init ) = ρ. Pick a player A ∈ P such that ρ |= φ A . Then, since σ is a Nash equilibrium, from every visited vertex v along ρ, A cannot enforce her objective φ A , which

means that v / ∈ W A , hence v ∈ W -A . Hence ρ |= Φ NE .
The situation is illustrated on Figure 3. Note that by determinacy, "Player A 1 should lose" can be replaced by "Coalition {A 2 , A 3 } prevents A 1 from winning". In this simple setting we can also prove the following existence result: Proposition 2. Assume setting ( †). There always exists a pure Nash equilibrium from v init . Proof (Sketch). In this simple setting, in two-player zero-sum games, there always exists strongly optimal strategies [START_REF] Gimbert | Solving simple stochastic tail games[END_REF], that is, one strategy for each of the two players, say σ and τ , such that each of the two strategies is optimal (for the corresponding player) after any compatible prefix. For every A ∈ P , we apply this result to each of the games G[A] from v init , and write σ A for the corresponding strongly optimal strategy for player A in G[A].

We argue why the main outcome ρ of σ = (σ A ) A∈P satisfies formula Φ NE . Assume that ρ |= φ A . Towards a contradiction assume that one of the visited vertices, say v after prefix π, along ρ, does not belong to W -A . By the strong determinacy result mentioned at the beginning of the proof, it implies that vertex v belongs to W A . Since σ A is strongly optimal, it is also optimal after prefix π: hence it is winning after prefix π. In particular, since φ A is prefix-independent, ρ should be winning as well. Contradiction: ρ |= Φ NE .

Algorithmics issues. By combining the proof of Propositions 1 and 2, one can compute a pure Nash equilibrium from strongly optimal and trigger strategies.

Another solution consists in computing for every A ∈ P the set W -A (or equivalently W A ), and to compute an infinite path in the game which satisfies formula Φ NE (which can be done for instance by enumerating the possible set of losing players, and then finding an adequate ultimately periodic play). Obviously, for specific winning conditions, more efficient algorithms can be designed, but this is not the aim of this note. We report e.g. to [START_REF] Ummels | Stochastic Multiplayer Games -Theory and Algorithms[END_REF][START_REF] Bouyer | Pure Nash equilibria in concurrent games[END_REF] for more algorithms.

Back to stochastic concurrent games

By a non-trivial extension of the discussion of Subsection 3.3 (see [START_REF] Ummels | The complexity of Nash equilibria in stochastic multiplayer games[END_REF]Section 3] for details), one can show the following existence result: Theorem 4. There exists a pure Nash equilibrium in any multiplayer stochastic turn-based game with prefix-independent winning objectives (which we can compute). This also holds in the same setting for any ω-regular objectives. [START_REF] Ummels | The complexity of Nash equilibria in stochastic multiplayer games[END_REF]Section 3] This result in particular applies to mean-payoff objectives, which are prefixindependent.

Why are we not fully happy with such a result?

one would like to go from turn-based to concurrent games; one would like more general payoff functions; one would like to solve the constrained existence problem.

It turns out that those extensions are very intricate, and that we can give a list of (related but incomparable) undecidability results.

Theorem 5. The following problems are all undecidable:

1. the constrained2 existence problem for stochastic multiplayer turn-based games with terminal-reachability objectives. This is true even if we restrict to pure strategy profiles. [36, Section 4] 2. the constrained existence problem for deterministic multiplayer turnbased games with terminal-reward payoffs. [35, Section 7] 3. the constrained existence problem for deterministic three-player concurrent games with terminal-reachability payoffs. 3 [5] 4. the existence problem for deterministic three-player concurrent games with terminal-reward payoffs.

[5] 5. the constrained existence problem for deterministic three-player concurrent games with safety objectives. 4 [5]

3.5 The suspect-game construction [START_REF] Bouyer | Pure Nash equilibria in concurrent games[END_REF] The setting we have chosen here assumes actions are invisible (since only visited vertices are visible along histories). Hence, a deviation from the main outcome can only be detected when the play goes out of the main outcome of the Nash equilibrium. However, even if a deviation occurs, there can be uncertainties for some of the players concerning the identity of the deviator. Consider for instance the game in Figure 4, with three players. Assume that the main outcome goes through v 0 aaa --→ v 1 .

-If the game proceeds to vertex v 2 instead of v 1 , it means that either player A 1 deviated alone (playing b instead of a), or both players A 1 and A 2 played b instead of a; the second case cannot occur since Nash equilibria only care of single-player deviations; hence only player A 1 can be the deviator, and all players will therefore know the identity of the deviator.

-If the game proceeds to vertex v 3 , then there are two possible suspects amongst the players: either A 2 or A 3 can be the deviator. In both cases, the two players A 2 and A 3 will know the identity of the deviator, while player A 1 will not know it.

This knowledge about the possible deviators is represented via a suspect function defined as follows:

-susp (v 0 , v 2 ), aaa = {A 1 } -susp (v 0 , v 3 ), aaa = {A 2 , A 3 }
with the meaning that, starting from v 0 , if the game proceeds to v 2 (resp. v 3 ), then only A 1 (resp. A 2 and A 3 ) are suspect for the deviation. More generally, we consider a game G = (V, v init , P , Σ, δ, (payoff A ) A∈P ), and we define the function susp : V 2 × Σ P → 2 P as follows:

susp (v 0 , v), m = {A ∈ P | ∃b ∈ Σ s.t. v 0 m[A/b] ----→ v}
Note that in the case no deviation occurred, that is if v 0 m -→ v, then the set of suspects is the set of all the players; this is because the set of suspect players becomes only relevant after a deviation has occurred.

The suspect game is now defined as the two-player 5 turn-based game S G = (S Eve , S Adam , s init , Γ, E, (payoff A ) A∈P ) where:

-S Eve = V × 2 P is the set of states belonging to Eve; -S Adam = S Eve × Σ P is the set of states belonging to Adam; s init = (v init , P ) is the initial state; -Γ = Σ P ∪ V is the new alphabet; the set of edges is

E = {(v, susp) m -→ ((v, susp), m) | v ∈ V, susp ⊆ P , m ∈ Σ P }∪ {((v, susp), m) v -→ (v , susp∩susp (v, v ), m) | ∃A ∈ P ∃b ∈ Σ s.t. v m[A/b] ----→ v }; -if ρ = (v 0 , susp 0 )(v 0 , susp 0 , m 1 )(v 1 , susp 1 ) . . ., for every A ∈ P , payoff A (ρ) = payoff A (v 0 v 1 . . .).
Given a play ρ = (v 0 , susp 0 )(v 0 , susp 0 , m 1 )(v 1 , susp 1 ) . . ., we define the set of suspect players for ρ as susp(ρ) = i≥0 susp i (this limit is well-defined).

The winning condition for Eve is rather non-standard, since it is a condition on the set of outcomes of Eve, not on each outcome of the strategy individually. A strategy ζ for Eve in S G is winning for some α ∈ R P if the unique outcome of ζ where Adam complies to Eve 6 has payoff α, and for every other outcome ρ of ζ, for every A ∈ susp(ρ), payoff A (ρ) ≤ α A .

Example 5. We consider again the small (part of) game depicted on Figure 4 (all missing moves in the figure lead to v 1 ). The corresponding part of the suspect game is given in Figure 5.

The role of Eve is to search for an equilibrium by suggesting moves to the players, and the role of Adam is to check whether there are possible profitable deviations. In particular, winning strategies of Eve in the suspect game will coincide with Nash equilibria in the original game: Proposition 3 (Correctness). Let α ∈ R P . There is a Nash equilibrium in G with payoff α from v init if and only if Eve has a winning strategy for α in S G from s init . Remark 1. Assume we start with a turn-based game. Then, since the arena of the game is known by the players, as soon as some deviation occurs, then all players will know which player is responsible for the deviation (since this is the player who controls the vertex at which the deviation occurred). In this case, the set of suspects will immediately be a singleton. The winning condition then ensures that, from a vertex controlled by player A i , if a deviation occurs, then Eve plays an optimal strategy for the coalition -A i = P \ {A i }. We somehow recover the intuitive explanation we gave in Subsection 3.3. Also, assume that actions are visible, then similarly, as soon as there is a deviation, the identity of the deviator is known by all the players. 5 We call the two players Eve and Adam. 6 That is, from (v, susp, m), Adam chooses to go to (v , susp) where v m -→ v . Algorithmics issues. Using the above construction, it is sufficient to solve the suspect game to compute Nash equilibria, since the equivalence of Proposition 3 is constructive. However, the winning condition is non-standard. In [START_REF] Bouyer | Pure Nash equilibria in concurrent games[END_REF], many algorithms are designed for specific payoff functions. Complexities obviously depend on the (discrete) payoff functions which are used.

As an illustration, let us look at Figure 6, where each player A has a Boolean objective φ A . We assume players A 1 and A 2 are losing along a play. Then if this play is the main outcome of a Nash equilibrium, it should be the case that from v, A 3 is able to punish both players (with the help of A 1 if A 2 is the deviator, and with the help of A 2 in case A 1 is the deviator); from v , it is known by everyone that A 1 is the deviator, hence the coalition of both A 2 and A 3 should be able to punish A 1 from there. Algorithmically, it is therefore sufficient to compute states (v, {A i }) which are winning for ¬φ Ai for the coalition -A i ) (or equivalently Adam); and then (in a bottom-up manner) states (v, {A i | i ∈ I}) which are winning for Adam for objective i∈I A i suspect at the limit ⇒ ¬φ Ai .

In [START_REF] Ummels | The complexity of Nash equilibria in limit-average games[END_REF]Section 6], an algorithm for mean-payoff functions is designed (in a setting where actions are visible), which consists in computing values of the various two-player mean-payoff games (A against -A ) in each vertex, and then to find a lasso satisfying a given constraint on the payoff.

Discussion

In this note, we have presented some basics of game theory over matrix games, and discussed how concepts from game theory can be studied in the context of models used in verification. We have discussed in particular a general construction that can be made to compute Nash equilibria in games on graphs, and which gives some general understanding of how interaction between players can be understood. This construction has been refined in several respects (for other solution concepts [START_REF] Brenguier | Robust equilibria in mean-payoff games[END_REF][START_REF] Condurache | The complexity of rational synthesis for concurrent games[END_REF], in some partial information contexts [START_REF] Bouyer | Games on graphs with a public signal monitoring[END_REF][START_REF] Bouyer | Nash equilibria in games over graphs equipped with a communication mechanism[END_REF]), and might be useful in some more contexts.

Even though there are some known existence results (we have mentioned some of them in Subsection 3.4), for simple payoff functions like terminal reachability payoffs. A related discussion can be found in [START_REF] Kristoffer | A stay-in-a-set game without a stationary equilibrium[END_REF].

In this note, we have not discussed temporal logics for multi-agent systems, even though this is a very rich domain of research (see [START_REF] Markey | Temporal logics for multi-agent systems (invited talk)[END_REF] for some pointers). We have also not discussed domination and admissibility (see [START_REF] Brenguier | Admissibility in games with imperfect information (invited talk)[END_REF] among others), nor subgame-perfect equilibria, which have nevertheless been much studied (among others, see [START_REF] Ummels | Stochastic Multiplayer Games -Theory and Algorithms[END_REF][START_REF] Brihaye | On subgame perfection in quantitative reachability games[END_REF][START_REF] Bruyère | On the existence of weak subgame perfect equilibria[END_REF][START_REF] Brihaye | Constrained existence problem for weak subgame perfect equilibria with ω-regular boolean objectives[END_REF]).

Fig. 1 .

 1 Fig.1. Hide-or-run game, on the left; and one of its variants, on the right (black squared states indicate payoffs of the two players if the game ends there).

Fig. 2 .

 2 Fig. 2. Turn-based game with terminal rewards (black squared states indicate payoffs of the two players if the game ends there) showing the non-applicability of Kakutani's theorem; the first player who leaves the loop with some positive probability loses.

Fig. 3 .

 3 Fig. 3. General shape of a Nash equilibrium in the simple setting (example with three players).

Fig. 4 .

 4 Fig. 4. Several suspect players.

Fig. 5 .

 5 Fig. 5. Illustration of the suspect game construction (states in light colors are Eve's states while states in dark colors are Adam's states).

Fig. 6 .

 6 Fig.6. Overview on the suspect-game construction.

This is the terminology used in the verification community, which might nevertheless be confusing with that used in the game theory community.

In the proof, we only impose that a player wins almost-surely.

This holds even with a constraint on the social welfare. This result has therefore to be compared with the result of[START_REF] Conitzer | New complexity results about Nash equilibria[END_REF], which states that the existence problem is NP-complete in two-player games.

This result has to be compared with the result of[START_REF] Secchi | Stay-in-a-set games[END_REF], which states that there always exists a Nash equilibrium in a safety game.

Acknowledgments. I would like to thank all my co-authors since I started working on multiplayer games played on graphs, that is, Nicolas Markey, Romain Brenguier [8], Daniel Stan [30], Michael Ummels and Nathan Thomasset.

Work supported by ERC project EQualIS between 2013 and 2019.


Patricia Bouyer Lsv
email: bouyer@lsv.fr

On the computation of Nash equilibria in games on graphs

Keywords: 2012 ACM Subject Classification Theory of computation; Theory of computation Multiplayer games, Nash equilibria Digital Object Identifier 10, 4230/LIPIcs, CVIT, 2016, 23

In this talk, I will show how one can characterize and compute Nash equilibria in multiplayer games played on graphs. I will present in particular a construction, called the suspect game construction, which allows to reduce the computation of Nash equilibria to the computation of winning strategies in a two-player zero-sum game.

Introduction

Multiplayer concurrent games over graphs allow to model rich interactions between players. Those games are played as follows. In a state, each player chooses privately and independently an action, defining globally a move (one action per player); the next state of the game is then defined as the successor (on the graph) of the current state using that move; players continue playing from that new state, and form a(n infinite) play. Each player then gets a reward given by a payoff function (one function per player). In particular, objectives of the players may not be contradictory: those games are non-zero-sum games, contrary to two-player games used for controller or reactive synthesis [10,7].

Using solution concepts borrowed from game theory, one can describe the interactions between the players, and in particular describe their rational behaviours. One of the most basic solution concepts is that of Nash equilibria [8]. A Nash equilibrium is a strategy profile where no player can improve her payoff by unilaterally changing her strategy. The outcome of a Nash equilibrium can therefore be seen as a rational behaviour of the system. While very much studied by game theoretists (e.g. over matrix games), such a concept (and variants thereof) has been only rather recently studied over games on graphs. Probably the first works in that direction are [5,4,11,12].

Computing Nash equilibria requires to (i) find a good behaviour of the system; (ii) detect deviations from that behaviour, and identify deviating players (called deviators); (iii) punish them. Variants of Nash equilibria (like subgame-perfect equilibria, robust equilibria, etc) require slightly different ingredients, but they are mostly of a similar vein.

In this talk, we will first recall some basics of game theory over matrix games. Those games are not sufficient in a verification context: indeed, explicit states are very useful when

23:2

On the computation of Nash equilibria in games on graphs modelling systems or programs, but are missing in matrix games. However stability notions like Nash equilibria or other solution concepts borrowed from game theory, are very relevant.

We will thus present the model of concurrent multiplayer games (played on graphs), which extends in a natural way standard models used in verification with multiplayer interactions. We will explain how Nash equilibria can be characterized and computed in such general games. We will also discuss some existence results for Nash equilibria.

A reference note for this talk is [1]. Related notes are [10], which discussed the use of two-player zero-sum games in verification, and [6], which discussed solution concepts in multiplayer turn-based games on graphs.

To give a taste of the approach, we informally discuss below a simple scenario. The general case with concurrent games and more general payoff functions will be handled by the suspect game abstraction, which somehow generalizes the simple scenario below. For readers not familiar at all with games, you can skip the discussion and wait until the talk.

Discussion on a simple scenario

We fix a turn-based and deterministic game G with set of players P , and we assume that the payoff function for each player A ∈ P is given by a Boolean prefix-independent objective φ A (that is, the player gets +1 is the play satisfies φ A , and 0 otherwise). Each player A plays using a (deterministic) strategy σ A , and once a strategy is fixed for every player, we have a strategy profile σ = (σ A ) A∈P . In such a game, the player objective is to make the generated play satisfy her formula. Hence, if the unique outcome of σ satisfies φ A , then player A is satisfied. Otherwise player A will try to be more satisfied by changing her strategy; the new strategy is then called a (single-player) deviation. The strategy profile σ will then be a (pure) Nash equilibrium if it is resistant to single-player deviations.

In our simple setting, it will be rather easy to characterize deviations that are profitable to player A: once a deviation by player A has occurred, we assume that all other players (which we note as a coalition -A ) play optimally in σ for the objective ¬φ A .1 That way, if the outcome of the strategy does only visit winning states for -A (which we denote W A ), then no deviation for player A can be profitable; conversely if the outcome visits a winning state for A (by determinacy, this is the negation of the previous case), then there will be a profitable deviation for player A. One can then characterize Nash equilibria as follows:

Proposition 1. Let ρ be an infinite path in G from the initial vertex v init . Then, ρ |= Φ NE if and only if there is a Nash equilibrium σ from v init such that the outcome of σ is ρ, where

Φ NE = A∈P ¬φ A ⇒ GW -A
The situation is illustrated on Figure 1. Note that by determinacy, "Player A 1 should lose" can be replaced by "Coalition {A 2 , A 3 } prevents A 1 from winning".

A solution to compute Nash equilibria is then to compute for every A ∈ P the set W -A (or equivalently W A ), and to compute an infinite path in the game which satisfies formula Φ NE (which can be done for instance by enumerating the possible set of losing players, and then finding an adequate ultimately periodic play). Obviously, for specific winning conditions, more efficient algorithms can be designed, see for instance [13,2].

Such a strategy is sometimes called a threat or a trigger strategy.

Acknowledgements I would like to thank all my co-authors since I started working on multiplayer games played on graphs, that is, Nicolas Markey, Romain Brenguier [3], Daniel Stan [9], Michael Ummels and Nathan Thomasset.

Work supported by ERC project EQualIS between 2013 and 2019.


Thomas Crespel
email: thomas.crespel@inria.fr

Patrick Reuter

Adrian Travis

Yves Gentet

Xavier Granier

Autostereoscopic transparent display using a wedge light guide and a holographic optical element: implementation and results

We present a novel transparent autostereoscopic display consisting of laser picoprojectors, a wedge light guide, and a holographic optical element. The holographic optical element is optically recorded, and we present the recording setup, our prototype, as well as the results. Such a display can superimpose 3D data on the real world without any wearable.

INTRODUCTION

Transparent displays, or see-through displays, allow a user to see the screen while still being able to see what is behind. They offer exciting possibilities for augmented reality as digital content may be superimposed on a real world object or scene. However, the digital content needs to be view-dependent in order to always align on the real objects to augment. Our goal is to provide a transparent display that can be used without tracking or any wearable, with autostereoscopic capabilities. Typical applications would be augmented showcases in museums or shops, head-up displays in vehicles, or any other augmented reality application that would preferably not require the user to wear any headset. This paper is structured as follows. In Section 2, we review related work on transparent 3D displays and wedge light guides. Section 3 details the general principle of our display. Section 4 focuses on describing the holographic optical element that composes our display. We describe the hardware and software implementation of our prototype in Section 5 and evaluate its performance in Section 6. Section 7 describes the perspective of improvement of our prototype, before we conclude in Section 8. This paper is an extended version of a two-page paper presented at the Digital Holography and 3D Imaging conference in May 2019 [START_REF] Crespel | Autostereoscopic transparent display using a wedge light guide and a holographic optical element[END_REF].

RELATED WORK A. Transparent and 3D displays

Transparent displays are possible notably thanks to OLED displays [START_REF] Gorrn | Towards see-through displays: Fully transparent thin-film transistors driving transparent organic light-emitting diodes[END_REF] or half-mirror and projector assemblies. However, such displays can generally not be used directly for augmented reality, as the augmentation has to be view-dependent in order to be aligned with the real world content. This problem can be partially solved by tracking the user's eyes positions relatively to the display [START_REF] Lee | Spacetop: Integrating 2d and spatial 3d interactions in a see-through desktop environment[END_REF][START_REF] Popescu | Simulated transparent display with augmented reality for remote collaboration[END_REF]. As the user's left and right eye have different positions themselves, a conflict between both eyes may arise. Head-mounted displays (HMDs) do not have the same alignement issues because the eye is fixed relatively to the screen. Indeed, the screen position and orientation must be tracked to update the digital content in real time. Exisiting HMDs can either be monoscopic [START_REF] Optinvent | [END_REF]6] or stereoscopic [7,[START_REF][END_REF].

A conceptually different approach is to simulate a seethrough effect from a video stream and to augment real content on an opaque regular display, like a phone or tablet. These approaches only provide a 2D projection of both the real and digital world.

Offering stereoscopic images to the user enhances 3D perception by exploiting binocular disparity. The left and right images can be separated towards the left and right eye by letting the user wear active or passive glasses, or the separation can be directly ensured by the display itself. In the latter case, the dis-plays are called autostereoscopic. Research on autostereoscopic displays is a broad area, and most of the existing approaches are based on parallax barriers or lenticular arrays [START_REF] Roberts | History of lenticular and related autostereoscopic methods[END_REF]10], random holes [START_REF] Nashel | Random hole display: A non-uniform barrier autostereoscopic display[END_REF] or compressive light-fields [START_REF] Wetzstein | Tensor Displays: Compressive Light Field Synthesis using Multilayer Displays with Directional Backlighting[END_REF]. If more than two views are presented, the display can also showcase other depth cues like motion parallax [START_REF] Howard | Depth perception[END_REF], enhancing even more 3D perception. Autostereoscopic displays often trade spatial resolution for angular resolution [START_REF] Jarvenpaa | Optical characterization of autostereoscopic 3-d displays[END_REF].

The ability to superimpose stereoscopic images over a realworld scene is an exciting perspective for augmented reality applications. The autostereoscopic displays presented above use conventional optics to separate the views, thus they are hardly adaptable to transparent displays. Takaki et al. [START_REF] Takaki | Flat-panel see-through three-dimensional display based on integral imaging[END_REF] adapted the lenticular method to create a see-through flat panel display based on integral imaging with several layers of lenticular arrays and a transparent display, but it suffers from diffraction effects by the pixel pitch and lenticular pitch, as well as low transmittance. The mask-hole method was also adapted to a transparent display [START_REF] Karnik | Mustard: A multi user see through AR display[END_REF], but the use of LCD panels inevitably blurs the real objects by diffraction. Hong et al. [START_REF] Hong | See-through multi-projection three-dimensional display using transparent anisotropic diffuser[END_REF] propose a multi-projection system with a transparent anisotropic diffuser, however, the diffuser is hard to manufacture, and multiprojection in free-space is often unwanted. Lee et al. [START_REF] Lee | Compact multiprojection 3d display system with light-guide projection[END_REF] proposed a compact, nontransparent, multiprojection system using a wedge light guide, a regular vertical diffuser, and Fresnel optics to create multiple viewing zones. Even though the purpose of this research was not to make a see-through display, we can argue that although the light guide is transparent, the Fresnel optics and diffuser distort the real world behind them, so it cannot be directly adapted to a see-through display.

An interesting element to perform view separation while maintaining a good transparency and no distortion is holography, and in particular holographic optical elements (HOEs). For an extensive survey on 3D displays based on holography, we refer the reader to He et al. [START_REF] He | Progress in virtual reality and augmented reality based on holographic display[END_REF]. Notably, some waveguide-based displays use HOEs, as for example the Hololens [7], where several HOEs are used to perform in-coupling, pupil expansion, and out-coupling in a waveguide [START_REF] Kress | 11-1: Invited paper: Towards the ultimate mixed reality experience: Hololens display architecture choices[END_REF]. The ability of HOEs to realize almost any optical function makes them suitable for multiprojection systems. Holografika [START_REF] Balogh | A scalable hardware and software system for the holographic display of interactive graphics applications[END_REF] designed a holographic screen for a full parallax opaque display using a dense projector arrangement. Olwal et al. [START_REF] Olwal | Astor: An autostereoscopic optical see-through augmented reality system[END_REF] designed the ASTOR display with two projectors in free-space and a reflective holographic combiner that scatters the light of each projector in separate viewing zones. Their display also involves free-space projection, and this may be unwanted for several reasons: the whole resulting system is bulky and not standalone as projectors must be positioned in accordance with the screen location, and the projection may be subject to occlusion issues. The fabrication of the involved HOEs is often eluded in the aforementioned literature, and our intention is to clearly describe also the recording process.

B. Wedge light guides

Our display involves a a wedge light guide to hold the projection distance, and we describe related work for such waveguides in the following.

Wedge optics have been widely used, and the most used case is wedge prisms to deflect or shape beams. Wedge light guides are specific wedge optics that were first developed for flat panel projection devices [START_REF] Travis | Flat panel display using projection within a wedge-shaped waveguide[END_REF] and later adapted to a flat panel timemultiplexed 3D display with a LED backlight and a LCD [START_REF] Lee | Flat-panel autostereoscopic 3d display[END_REF].

As depicted in Figure 1, a wedge light guide is roughly composed of two parts: an expansion part and a wedge part. If a Fig. 1. Principle of a wedge guide ray is shone into the entrance of the expansion part, it will be guided through total internal reflection towards the wedge part, where one interface is tilted relatively to the other. The rays will then undergo further total internal reflection bounces but the angle of reflection lowers at each bounce until the critical angle is reached, and the ray escapes the guide.

If a projector launches a fan of rays, then each ray will escape at a different position depending on the input angle: in the plane of the drawing, the grazier the angle, the further it will propagate. The image carried by the projector diverges in the plane of the guide in the expansion part, and the wedge part realizes the expansion of the image along the direction of propagation.

If a diffuser is located at the extraction surface, the projected image will be visible to a user like in free-space projection and without the need to couple out the beam from the guide.

If nothing blocks or redirects the rays at the exit surface, then they will simply continue their propagation. When the rays have just escaped the total internal reflection regime, they will leave the guide with an angle close to 90°with respect to the normal of the exit surface in the plane of the drawing, while they keep on diverging from a point source in a direction parallel to the plane. The shape of a beam created by a projector and escaping a wedge guide is then collimated in one direction and diverging in the other, and propagates with a grazing angle with respect to the wedge surface [START_REF] Crespel | Wedge cameras for minimally invasive archaeology[END_REF] . Readers must be aware that unlike the wedge guide described in [START_REF] Lee | Compact multiprojection 3d display system with light-guide projection[END_REF] and schematically drawn in Figure 1, these wedge guides do not have rigorous planar faces but have a thickness profile that is optimized to force rays to undergo the same number of reflections and leave the guide from the same side [START_REF] Travis | Flat-panel display using tapered waveguide[END_REF]. The advantage of a wedge guide compared to a regular slab is that there is no need for incoupling, pupil expansion nor out-coupling, as the guide itself ensures these functions.

Our main contribution in this paper compared to other work on wedge guides is to replace the regular diffuser that scatters the light from one projector uniformly by a holographic diffuser that scatters the light from several projectors to separate viewing zones.

OVERVIEW

The principle of our display, as depicted in Figure 2, is to couple beams from multiple laser beam steering picoprojectors into a transparent wedge guide and then to redirect each beam to separate viewing zones using a transparent HOE.

The viewing zones have a width W VZ and a height H VZ , and they are located at a distance D obs in front of the HOE. If W VZ is an integer fraction of the interpupillary distance d IPD , then a user located at D obs in front of the display has both eyes in separate viewing zones and perceives a stereoscopic image with naked eyes.

HOLOGRAPHIC OPTICAL ELEMENT

A. Role of the HOE

A transmission volume HOE is clamped to the wedge exit surface in order to create the viewing zones. Note that the HOE is

2).

Our approach is the following: we record the optical function for the central viewing zone only as we explain in Section B. In addition, as we detail in Section C, we use the large angular bandwidth of the hologram to reconstruct the other viewing zones.

B. Recording setup

The HOE is optically recorded, on the material Ultimate 04 (U04) from Ultimate Holography [START_REF]Ultimate Holography[END_REF], and so we need to create an interference pattern between a reference beam and an object beam. Let us first consider the recording for the central projector position (i = 0). Figure 3 illustrates the recording setup and the coordinate systems used for the following explanations.

The object beam is generated by a rectangular diffuser of size W VZ × H VZ and located at D obs in front of the hologram, and this corresponds to the desired properties of the viewing zone. To uniformly light the diffuser, we first spread the beam with a cylinder lens L2. Its focal length does not matter since the objective is simply to create a line on a first diffuser. This line is scattered toward a second diffuser that represent the recorded object, and each point of it is then scattered toward the full hologram.

Defined this way, it is clear that the reconstruction has to result in a real image of the object where rays converge, rather than a virtual image. Thus, the reference beam must be the complex conjugated of the incident beam, i.e. the counterpropagating wave.

The beam that is incident on the HOE is the beam that exits the wedge guide: it is collimated in the plane of Figure 1 and diverging in a plane parallel to the wedge (see Section 2 and [START_REF] Crespel | Wedge cameras for minimally invasive archaeology[END_REF]), so the reference beam must be collimated and converging. Moreover, it must be incident on the hologram with a grazing angle corresponding to the exit angle of the wedge guide (β ≈ 8 • ).

To create the reference beam, we first spread it by a spatial The reference beam is created by creating a convergent beam with a spherical mirror and collimate it in one direction with a cylinder lens.

filter toward a spherical mirror. As the mirror is in off-axis configuration, the beam is converged into a sagittal point S and tangential point T due to astigmatism. The center of the hologram is located at about 400m from S so that the converging angle α corresponds to the diverging angle from the wedge at the HOE location (α ≈ 15 • ). On the other hand, we add a diverging cylinder lens L1 of focal length -500mm so that the tangential image is located at its focal plane and the beam gets collimated in this direction. The lens L1 must be sufficiently high so that the converging beam covers entirely the HOE and in practice, we glued 8 lenses together to obtain a 200mm high lens.

We have recorded a monochromatic green HOE and a color HOE. The color HOE is obtained with wavelength multiplexing, and the laser beam shown in Figure 3 is composed of red, green, and blue lasers.

C. Reconstruction of the adjacent viewing zones

Our HOE is a volume hologram, therefore it has Bragg selectivity, and in particular angular selectivity. The typical efficiency curve [START_REF] Kogelnik | Coupled Wave Theory for Thick Hologram Gratings[END_REF] with respect to the deviation from the Bragg angle is shown in Figure 4. Note that the Bragg angle is different for each position of the hologram but every point exhibits this angular efficiency.

Rays that are incident on the HOE with the Bragg angle (the recording angle) create a viewing zone with maximum efficiency.

Rays whose angles belong to the angular bandwidth still reconstruct a viewing zone but with a lower efficiency and we use this range to reconstruct the other viewing zones. The dashed lines illustrate where the angle of incidence of each projector are located with respect to the Bragg angle and bandwidth. The position of the resulting viewing zone is shifted with respect to the input angular shift, so it is possible to arrange the projectors Rays that are incident on the hologram with an angle outside the angular bandwidth are not diffracted. This is the case with light that does not come from the inside of the wedge, thus the HOE appears transparent in a natural environment.

D. Alternative approach

It could have been possible to have a narrower angular bandwidth and to angular-multiplex as much gratings as projectors, but the recording setup would have been much more complicated, and the diffraction efficiency potentially lower. Here, we show that it is possible to record a hologram for a single projector and use the large bandwidth to reconstruct the other viewing zones, without angularly multiplexing each projector position. This also has the advantage of giving more freedom on the positioning of the projectors after the recording process.

PROTOTYPE OF THE DISPLAY A. Hardware design

We use an off-the-shelf wedge guide designed according to patent [START_REF] Travis | Flat-panel display using tapered waveguide[END_REF], with a size of 480mm x 250mm and a thickness varying from 10mm to 1mm. The HOE is located at the imaging area of the wedge guide. We use N proj = 5 Sony MP-CL1A laser picoprojectors [START_REF] Sony | [END_REF] that are connected to a laptop computer with an external graphical card. Each projector is separated by its neighbor(s) by 17mm, and they converge toward the HOE. The viewing zones are W VZ = 30mm wide and H VZ ≈ 100mm high and are located at D obs = 50cm. The prototype is built thanks to an aluminium frame and 3D printed elements.

B. Software Calibration

Our software generates N proj renderings of a 3D scene and casts them to N proj fullscreen windows on the projectors, which are connected as external monitors. The images must be aligned with each other on the plane of the HOE, and this is done by correcting both the wedge optical distortion and the positional relative projectors' offset.

To this end, we go through a calibration procedure that has to be done only once (provided that the prototype elements remain fixed between each other). The calibration procedure is illustrated in Figure 5 anddescribed below: 1. We replace the HOE with a regular diffuser (e.g. a piece of paper), so that the images projected by each projector are all visible from a single viewpoint.

2. A distortion-corrected camera images the diffuser, and the area to be calibrated has to be cropped.

3. A regular grid is drawn in camera space. 4. An algorithm projects a point in projector space and moves it until it matches a target corner in the camera grid. This is illustrated in Figure 5 where three points are projected and tracked by their color simultaneously.

5. We then extrapolate the calibrated points to a texture of the size of the projector resolution: for each pixel, we perform a bilinear interpolation in a quad formed by the closest calibrated points.

We call the resulting texture of this preprocess the mapping texture, and it stores for each projector pixel the corresponding coordinate of the target texture. When using our display, all the projected images are corrected in real time on the GPU: for each projector pixel, we look up the value of the mapping texture which provides the pixel coordinates to read in the input image.

We evaluate the required image transformation without any a priori knowledge on projector position or angle, or on the wedge guide properties. Our algorithm takes two minutes on average to calibrate one projector. Figure 5 shows the deformation of 5 checkerboard images that align on the imaging area.

RESULTS

In this section, we evaluate the performance of our display. We first focus on the practical reconstruction of the viewing zones with the monochromatic HOE in Section A. We then describe the color issues that we observed with the full-color HOE in Section B, before evaluating the display as a whole in Section C.

A. Reconstruction of the viewing zones

The five projectors are located at the entrance of the wedge guide and display fullscreen green-only images. The monochromatic HOE is located at the wedge part of the guide and the reconstruction of the viewing zones on a D obs distant screen can be seen in Figure 6(a). One can observe that they are well defined, and their size match the size of the recorded object. Note that the full-color HOE also shows the same behavior, except for color issues that are specifically addressed in Section B.

We insist on the fact that this rectangular diffuser is reconstructed with a projector that fully lights the HOE, and if only a portion of it is lit (e.g. one pixel), then the entire viewing zone will be reconstructed as well, with a much lower intensity. As predicted by the coupled-wave theory [START_REF] Kogelnik | Coupled Wave Theory for Thick Hologram Gratings[END_REF], the intensity lowers from the central positions with a sinc 2 modulation when the angle of incidence diverges from Bragg angle.

The outermost projectors have an efficiency ratio of 60% with respect to the central one. Hence, the number of projectors N proj can be more than 5 before extinction of the diffraction efficiency. We evaluate at N proj,max = 9 the maximum number of projectors with a minimum intensity ratio of 20% with respect to the central one. Uniformity in intensity can be achieved computationally by lowering the intensity of the brightest viewing zones so that they match the darkest one.

B. Color issues

The full-color HOE also reconstructs the viewing zones with the same behavior and angle dependency as explained in the previous section. In addition, each viewing zone display chromatic issues that are specifically discussed in this section.

Figure 7(a) shows a picture of a viewing zone created on a D obs distant screen by a fullscreen white image on the projector. Figures 7(b), 7(c), and 7(d), respectively, show the contributions of the red, green and blue wavelengths.

Figure 7(e) illustrates the wavelength-dependent contributions to the final result:

• The images R R , G G and B B are sharply imaged and superimposed at the screen position, as desired. An eye located in this area can thus perceive a full color image. The ideal white balance can be achieved either by software or by optimizing exposure times for each wavelength at the recording step.

• The red wavelength does reconstruct any other image. • The areas G R and B G are overlapping and appear blurred at the screen location. They are actually images that are reconstructed 15cm further than D obs (65cm away from the HOE). These images are undesired crosstalk images that are respectively created by the green wavelength diffraction in the red grating, and the blue wavelength diffraction in the green grating.

• The image B R is located 135cm in front of the HOE and corresponds to the order created by the blue wavelength diffraction in the red grating.

At the time of the recording, we did not measure the wavelength dependency of the diffraction efficiency. Finally, the red grating appears to be more efficient than the green one, which is itself more efficient than the blue. This explains why the areas G R and B G are brighter than G G and B B , respectively.

We measure the RGB area to be about 75mm high, and this is the effective viewing zone size where an eye can perceive a color image. In the current state of the prototype, if an eye is located too low in the eyebox, the user would see an image that does not contain red. We discuss in Section 7 how to avoid such color effects. Figure 8 shows five photographs of the display taken from each viewing zone, showing full color and transparency. The images are rendered with a slightly different perspective and corrected with the procedure described in Section B. As a consequence, binocular disparity and horizontal motion parallax are rendered and allow to have a good appreciation of the depth of the scene. We observed that a tolerance of about ±10cm around D obs is acceptable to view the entire images, and the measured field of view is 17°. Small vertical black lines are visible, and they are due to the cylinder lens that we made by gluing smaller lenses together: the interfaces have cast shadows on the hologram. They can be easily removed by using a single lens instead of glued lenses during the recording.

C. Display

FUTURE WORK A. Improvements on the HOE

The most required improvement of the HOE is the correction of chromatic aberrations described in Section 6, and several approaches are possible. We could use the same material and design a solution based on the observations. For example, recording another red viewing zone that overlaps with G R and B G would allow to see color images in this area. Simply extending the size of the viewing zone in this direction can also reduce the probability of being in the wrong location. Another way of improving color rendering would be to increase the thickness of the hologram to reduce spectral bandwidth and avoid color crosstalk. The problem with this approach is that the angular bandwidth would be reduced as well, and the maximum angle of incidence separating the outermost projectors would be lower. With constant projector pitch, this implies that N proj would be lower, and the field of view would also be smaller. With this approach, it could be interesting to have a significantly narrower bandwidth and multiplex the hologram for each projector position.

If color aberrations remain, a software white balance based on eye tracking should decrease perceived color shifting as long as red, green, and blue are in all viewing zones.

Depending on the application, it could be interesting to study how the image plane could be relocated behind the HOE plane, so that it is closer to the real objects and thus reduces the accomodation-vergence conflict for augmented reality applications. A possible solution might be to put an imaging lens between the diffuser and the hologram in the recording setup. In further research, we might study as well the recording of multiple imaging planes.

For now, the HOE has a size of 10x13cm, but for some applications it might be interesting to record a bigger HOE. The process could be a bit more complicated because of the larger optics that would be required to create the converging beam.

The other parameters of the HOE recording setup can also be changed according to the targeted application: D obs can be changed at will, and W VZ can be decreased to produce a denser horizontal parallax with denser image sources as well.

B. Improvements on the display

Apart from the HOE, several perspectives of improvement on the other parts of the display will be investigated.

First of all, eye tracking can improve the 3D depth cues by updating the displayed images with respect to the position of the user's eyes. Without tracking, the digital scene perspective does not change when moving horizontally in the W VZ range, and vertically in the H VZ range. Eye tracking could improve the motion parallax feeling and reduce the transition effects between views while still producing stereoscopic images.

Adding more projectors up to N proj,max would improve the field of view from 17°to 30°and offer more viewing zones. However, having a lot of projectors might not be a practical solution due to the cost of the system and the consumed power. It should be possible to have an opto-mechanical system to rasterize several virtual projector positions at high frequency and synchronize the rendering with it.

Finally, note that we used an off-the-shelf wedge guide that was not originally designed for this application, and it might be interesting to manufacture a dedicated wedge guide that is optimized for several projector positions. In particular, having a curved entrance instead of a rectangular one should improve the reconstruction quality by ensuring that the distance between the light source and the hologram is constant. Changing the size of the wedge guide with respect to the targeted application and HOE size should also be investigated. In particular, there is no physical limitation to design a phone-sized display.

CONCLUSION

We have demonstrated the feasibility of a compact, autostereoscopic transparent display with multiple projectors and a custom HOE. The HOE is wavelength-multiplexed for full-color efficiency, but only one angular grating is recorded and multiple viewing zones are reconstructed with several projector positions due to the high angular bandwidth. Although some chromatic issues are visible, they can be corrected and the proof-of-concept is demonstrated.

Our current prototype has N proj = 5 views but is theoretically able to generate up to N proj,max = 9 views.

The views are located 50cm in front of the display, they are 3cm wide and 10cm high. These values are fixed once the HOE is recorded; they result from our choices and can be changed in the recording step. Having narrower viewing zones would give a denser horizontal parallax but would also require to have as much more projectors. Eye tracking can improve horizontal motion parallax and add vertical motion parallax.

This display has great potential for augmented reality applications such as augmented exhibitions in museums or shops, head-up displays for vehicles or aeronautics, and industrial maintenance, among others.

Fig. 2 .

 2 Fig. 2. (left) Overview of the prototype: 5 projectors labeled -2..2 are coupled into a wedge light guide, and a HOE scatters the light towards independent viewing zones -2...2. (right) Photograph of our prototype from viewing zone 0

Fig. 3 .

 3 Fig. 3. Recording setup of the HOE. The object beam is created by a rectangular diffuser representing the viewing zone.The reference beam is created by creating a convergent beam with a spherical mirror and collimate it in one direction with a cylinder lens.

Fig. 4 .

 4 Fig. 4. Typical diffraction efficiency of a volume hologram depending on the deviation from the Bragg angle and the incidence angles of the 5 projectors of our display (in dashed lines)

Fig. 5 .

 5 Fig. 5. Calibration procedure and image transformation of 5 checkerboard patterns that align on the imaging area

Fig. 6 .

 6 Fig. 6. (a) Photograph of the 5 views projected on a screen at distance d obs from the HOE; (b) Normalized intensity profile along the horizontal direction

Fig. 7 .

 7 Fig. 7. Images of the viewing zones on a D obs distant screen, created by (a) Red, green and blue wavelengths; (b) Red only; (c) Green only; (d) Blue only; (e) Illustration of the wavelengthdependent contributions of each grating.

Fig. 8 .

 8 Fig. 8. Photographs of the display from each viewing zone. Parallax and transparency can be obsesrved.