Keywords: Games, Imperfect Information, Opacity, Security

Problèmes d'opacité dans les jeux à information imparfaite

Résumé : Nous étudions en détail la classe des jeux à condition d'opacité, qui sont des jeux à deux joueurs à information imparfaite dans lesquels seul l'un des joueurs n'a pas information parfaite, et où la condition de gain dépend de l'information que celui-ci a au cours du jeu. Ces jeux sont liés à des aspects de sécurité des systèmes informatiques : une partie est opaque si le joueur à information imparfaite ne "sait" jamais avec certitude que la position courante est l'une des positions spéciales dites "secrètes". Nous étudions les problèmes de décision d'existence de stratégie gagnante pour chaque joueur, et nous les appellons opacity-violate problem et opacity-guarantee problem. Le fait de s'intéresser au joueur à information parfaite est nouveau en théorie des jeux à information imparfaite car lorsqu'on considère des conditions de gain classiques cela revient à considérer le jeu à information parfaite sous-jacent. Nous établissons que les deux problèmes sus-mentionnés sont EXPTIME-complets, montrant ainsi que notre condition de gain apporte un saut de complexité pour le joueur à information parfaite, et nous exhibons le problème opacity-verify qui, de manière intéréssante, généralise des approches considérées dans la littérature pour l'analyse d'opacité des systèmes à évènements discrets. Dans le cas des jeux en aveugle, ce problème se relie aux deux problèmes initiaux, de telle sorte que les jeux en aveugle à condition d'opacité sont déterminés et que les trois problèmes sont PSPACE-complets.

Mots-clés : Jeux, Information imparfaite, Opacité, Sécurité

Introduction

We described in [START_REF] Maubert | Games with Opacity Condition[END_REF] a class of two-player games with imperfect information that we called games with opacity condition. In these games, the players are Robert (for "robber") and Gerald (for "guardian"). Robert has imperfect information as opposed to Gerald who has perfect information. This asymmetric setting is very relevant for the verification of open systems and all the more for security aspects as it captures the intuitive picture of an attacker having only a partial information against a system. The game model we consider relies on the classical imperfect-information arenas, as defined in e.g. [START_REF] Reif | The complexity of two-player games of incomplete information[END_REF][START_REF] Berwanger | On the power of imperfect information[END_REF], but it is equipped with a subset of positions that denote confidential information and that we call secrets.

We focus on the opportunity for Robert to discover some secret, by introducing the property of opacity: a play is opaque if, at each step of the (infinite) play, the set of positions that are considered possible by Robert does not consist of secrets only. In games with opacity condition, the opacity property is the winning condition for Gerald. Informally, Robert tries to force the game to reach some point when he knows for sure that the current position is a secret, whereas Gerald tries to keep Robert under uncertainty. Note that this winning condition can be seen as a particular epistemic temporal logic statement [START_REF] Halpern | The complexity of reasoning about knowledge and time. 1. lower bounds[END_REF] on an imperfect information arena seen as an epistemic temporal model : this ETL formula is G¬K Robert secret. However, to our knowledge the complexity of deciding the existence of winning strategies for such winning conditions has never been studied in depth.

Our claim that games with opacity condition are natural and adequate models for practical applications is all the more sustained by very recent contributions of the literature [START_REF] Saboori | Opacity-enforcing supervisory strategies for secure discrete event systems[END_REF][START_REF] Dubreil | Opacity enforcing control synthesis[END_REF]. These results mainly arise from the analysis of discrete-event systems and their theory of control, and our games embed some problems studied in this domain, such as the verification of opacity. Our abstract setting provided by the game-theoretical paradigm enables us to focus on essential aspects of the topic, such as synthesizing strategies, and to circumvent the complexity of the problems.

Not surprisingly, games with opacity condition are not determined [START_REF] Maubert | Games with Opacity Condition[END_REF]. We therefore introduced two dual problems: the opacity-violate problem and the opacity-guarantee problem, that consist of deciding the existence of a winning strategy, respectively for Robert and for Gerald. The opacity-violate problem generalizes the strategy problem in reachability games with imperfect information [START_REF] Reif | The complexity of two-player games of incomplete information[END_REF], and so does the opacity-guarantee problem, but putting the emphasize on the player who has perfect information and has the complementary safety objective. The latter is, to our knowledge, never been done, for the following reason. In two-player games with imperfect information, when considering the existence of winning strategies for a player, one can equivalently consider that the opponent has perfect information (see [START_REF] Reif | The complexity of two-player games of incomplete information[END_REF]). Thus, when dealing with omega-regular winning conditions in arenas where the imperfect information is asymmetric, focusing on the player with perfect information would amount to solve the underlying perfect-information game. Our case is different : when considering Gerald's point of view, we could indeed equivalently consider that Robert plays with perfect information too, but we cannot give up the imperfectinformation setting because the definition of the winning condition itself relies on Robert's information along the play.

Additionally to the two aforementioned problems, we consider the opacityverify problem as an intermediate problem: the question here is to decide whether in a game with opacity condition, all strategies of Gerald are winning. The choice of considering this apparently weird problem is well motivated. Firstly, it is equivalent both to the opacity-guarantee problem and to the complementary of the opacity-violate problem for blindfold games; an immediate consequence is the determinacy of blindfold games with opacity conditon. And secondly, it enables us to embed opacity issues in discrete-event systems with a strong language-theoretic feature, addressed earlier in the literature [START_REF] Saboori | Opacity-enforcing supervisory strategies for secure discrete event systems[END_REF][START_REF] Dubreil | Opacity enforcing control synthesis[END_REF].

In this contribution, we consider the three problems of opacity-violate, opacityguarantee and opacity-verify, keeping in mind that our main attention turns to the opacity-guarantee problem. It is not hard to establish the EXPTIMEcompleteness of the opacity-violate problem, from a power-set construction inspired by [START_REF] Reif | The complexity of two-player games of incomplete information[END_REF] that amounts to solving a reachabilty perfect-information game, and from the fact that it generalizes imperfect-information games with reachability condition, known to be EXPTIME-complete [START_REF] Reif | The complexity of two-player games of incomplete information[END_REF]. Regarding the opacityguarantee problem, we rely on an earlier power-set construction to reduce this problem to a perfect-information game [START_REF] Maubert | Games with Opacity Condition[END_REF], yielding EXPTIME membership. The EXPTIME-hardness result for this problem, where the main player (Gerald) has perfect information, was unknown until now and relies on a reduction from the empty input string acceptance problem for linearly-bounded alternating Turing machines. As a corollary, the model checking problem for AETL [START_REF] Dima | Model-checking an alternating-time temporal logic with knowledge, imperfect information, perfect recall and communicating coalitions[END_REF] is EXPTIME-hard, hence EXPTIME-complete in the size of the arena. The key point is a pioneer encoding of configurations by information sets. Concerning the opacity-verify problem, we prove its PSPACE-completeness, which for the lower bound relies on a reduction similar to the one in [START_REF] De Wulf | Antichains: A new algorithm for checking universality of finite automata[END_REF] from the universality problem for nondeterministic automata [START_REF] Hopcroft | Automata theory, languages, and computation[END_REF]. Interestingly, the opacity-verify problem relates the two other problems for the particular case of blindfold games, in such a way that those games are determined. We also show that the blindfold setting embraces the language-theoretic approches for opacity analysis in discrete-event systems [START_REF] Saboori | Opacity-enforcing supervisory strategies for secure discrete event systems[END_REF][START_REF] Dubreil | Opacity enforcing control synthesis[END_REF].

The paper is organized as follows. In Section 2, we define games with opacity condition. In Section 3, we present the opacity-guarantee problem and the opacity-violate problem, and we establish their EXPTIME complexity. We first recall the power-set constructions from [START_REF] Maubert | Games with Opacity Condition[END_REF] yielding the upper bounds, then we show the matching lower bounds. In Section 4, we consider the opacity-verify problem for blindfold games. In this setting, we establish the determinacy and the PSPACE completeness of the three opacity problems. In Section 5, we retale the opacity-verify problem to the language opacity verification of [START_REF] Saboori | Opacity-enforcing supervisory strategies for secure discrete event systems[END_REF][START_REF] Dubreil | Opacity enforcing control synthesis[END_REF]. In Section 7, we discuss complexity aspects of problems regarding Gerald's winning strategies. We conclude in Section 8 by giving some ideas on our current and future work.

Games with opacity condition

A game with opacity condition over the alphabet Σ and the set of observations Γ is an imperfect information game structure A = (V, ∆, obs, act, v 0 , S) where V is a finite set of positions, ∆ : V × Σ → 2 V \∅ is a transition function, obs : V → Γ is an observation function, and act : Γ → 2 Σ \∅ assigns to each observation a INRIA non-empty set of available actions, so that available actions are identical for observationally equivalent positions. Finally, v 0 is the initial position, and the additional element S ⊆ V in the structure A is a finite set of secret positions.

In a game A = (V, ∆, obs, act, v 0 , S), the players are Gerald and Robert. A play is an infinite sequence of rounds, and in each round i ≥ 1, Robert chooses an action a i ∈ act(obs(v i-1 )), Gerald chooses the new position v i ∈ ∆(v i-1 , a i ), and Robert observes obs(v i ). A play in A is an infinite sequence ρ = v 0 a 1 v 1 . . . ∈ v 0 (ΣV ) ω that results from an interaction of Robert and Gerald in this game.

We now extend obs to plays by letting obs(v

0 a 1 v 1 a 2 v 2 . . .) := v 0 a 1 γ 1 a 2 γ 2 . . . with γ i = obs(v i ) for each i ≥ 1.
The imperfect information setting leads Robert to partially observe a play ρ as obs(ρ). Note that since the initial position is a part of the description of the arena, it is known by Robert.

For every natural number k ∈ N and play ρ, we denote by ρ k ∈ v 0 (ΣV ) k the k-th prefix of ρ, defined by ρ k := v 0 a 1 v 1 . . . a k v k , with the convention that ρ 0 = v 0 . We denote by ρ + an arbitrary prefix of ρ.

Since the information revealed to Robert is based on observations, a strategy of Robert in A is a mapping of the form α : v 0 (ΣΓ) * → Σ such that for any play prefix ρ k ending in observation γ, α(obs(ρ k )) ∈ act(γ). On the contrary Gerald has perfect information on how the play progresses, so a strategy of Gerald in A is a mapping of the form β : v 0 (ΣV ) * Σ → V such that for any play prefix ρ k ending in position v, for all a in act(obs(v)), β(ρ k a) ∈ ∆(v, a).

Given strategies α and β of Robert and of Gerald respectively, we say that a play ρ = v 0 a 1 v 1 . . . is induced by α if ∀k ≥ 1, a k = α(obs(ρ k-1 )), and ρ is induced by β if ∀k ≥ 1, v k = β(ρ k-1 a k ). We also note α β the only play induced by α and by β.

In the following, an observation γ might be interpreted as the set of positions it denotes, namely obs -1 (γ).

Let us fix a play ρ = v 0 a 1 v 1 a 2 v 2 . . .. Note that every k-th prefix of ρ characterizes a unique information set I(ρ k ) ⊆ V consisting of the set of positions that Robert considers possible in the game after k rounds. Formally, information sets can be defined inductively as follows.

Definition 1 For every play ρ = v 0 a 1 v 1 a 2 v 2 . . ., we let I(ρ 0 ) := {v 0 } and I(ρ k+1 ) := ∆(I(ρ k ), a k+1 ) ∩ obs(v k+1 ), for k ∈ N.

We now define the opacity property: Definition 2 For a given set of secret positions S ⊆ V , a play ρ satisfies the opacity property for S, or is S-opaque, if:

∀k ∈ N, I(ρ k ) S
Informally, the opacity condition means that Robert never knows with certainty that the current position is a secret, because there is always one of the positions he considers possible that is not a secret. In a game with opacity condition, the opacity property is the winning condition for Gerald, i.e S-opaque plays are winning for Gerald, and the other ones are winning for Robert.

Remark 1

The definition of the arena and of the opacity condition are slightly different from the ones in [START_REF] Maubert | Games with Opacity Condition[END_REF] : originally Robert's aim was to reach a singleton information set. We introduce here the set of secret positions and define the winning condition accordingly because it makes these games closer to the intuition behind opacity. Anyway the results established in [START_REF] Maubert | Games with Opacity Condition[END_REF] still hold in this setting, and adapting the proofs is straightforward.

3 Opacity-violate and opacity-guarantee problems

It is well known that perfect-information games are determined [START_REF] Martin | Borel determinacy[END_REF], and that imperfect-information games are not determined in general. We recall that a game is determined if each position is winning for one of the two players.

We proved the following result in [START_REF] Maubert | Games with Opacity Condition[END_REF]:

Theorem 1 Games with opacity condition are not determined in general.

This result leads to introduce two dual problems. We remind that α (resp. β) stands for a strategy of Robert (resp. Gerald). We first consider Robert's point of view.

Definition 3 Given a game with opacity condition A = (V, ∆, obs, act, v 0 , S), the opacity-violate problem is to decide whether the following property holds: ∃α, ∀β, α β is not S-opaque

We now consider Gerald's dual point of view.

Definition 4 Given a game with opacity condition A = (V, ∆, obs, act, v 0 , S), the opacity-guarantee problem is to decide whether the following property holds: ∃β, ∀α, α β is S-opaque Remark 2 It is important to comment on Definition 4 regarding the universal quantification over Robert's strategies. As defined, this quantification ranges over observation based strategies only. The opacity-guarantee problem would however be equivalent if this quantification ranged over the wider set of perfect information strategies, as already argumented by Reif in [START_REF] Reif | The complexity of two-player games of incomplete information[END_REF] : along a play, Robert's possible behaviors are not restricted by observation-based strategies.

In the rest of this section we prove the following result:

Theorem 2 The opacity-violate and opacity-guarantee problems are EXPTIMEcomplete.

In the following, we adopt the classic convention that the size of a game is the size of its arena, i.e. the number of positions.

Power-set constructions for upper bounds

We recall the power-set constructions of [START_REF] Maubert | Games with Opacity Condition[END_REF] that lead to equivalently solve perfect information games.

We first address the opacity-violate problem. Since we consider the point of view of the player with imperfect information, this problem is close to problems usually studied in games with imperfect information. This is why we can easily INRIA rely on previous work on the topic to study its complexity. We remind the construction from [START_REF] Maubert | Games with Opacity Condition[END_REF], which is strongly inspired from the one described by Reif in [START_REF] Reif | The complexity of two-player games of incomplete information[END_REF] :

Let A = (V, ∆, obs, act, v 0 , S) be a game with opacity condition. We define a reachability perfect-information game A, where the players are Roberta and SuperGeraldine1 . A position of A is either I where I is a reachable information set in A -it is a position of Roberta -, or (I, a) where I is a reachable information set in A and a ∈ act(I)2 -it is a position of SuperGeraldine.

The game is played as follows. It starts in the initial position I 0 := {v 0 } of Roberta. In a position I, Roberta chooses a ∈ act(I) and moves to position (I, a). Next, let O be the set of reachable observations from I by a. SuperGeraldine chooses a next information set ∆(I, a) ∩ γ, where γ ranges over O. In A, a play I 0 (I 0 , a 1 )I 1 (I 1 , a 2 ) . . . is winning for Roberta if it reaches a position of the form I with I ⊆ S, otherwise it is winning for SuperGeraldine.

Theorem 3 [START_REF] Maubert | Games with Opacity Condition[END_REF] Robert has a winning strategy in A, if and only if, Roberta has a winning strategy in the perfect-information game A.

Due to nondeterminacy (Theorem 1), the opacity-guarantee problem has to be studied on its own. We remind the power-set construction for the opacityguarantee problem described in [START_REF] Maubert | Games with Opacity Condition[END_REF], that leads to a safety perfect-information game A. In this game, unlike in A, we maintain an extra information on how Gerald is playing in A. The players in A are SuperRoberta3 and Geraldine. A position in A is either of the form (I, v) where I is a reachable information set in A, and v ∈ I -it is a position of SuperRoberta -, or of the form (I, v, a) where I is a reachable information set in A, v ∈ I, and a ∈ act(I) -it is a position of Geraldine. The initial position is ({v 0 }, v 0 ). In position (I, v), SuperRoberta chooses a ∈ act(I), and moves to (I, v, a). In position (I, v, a), Geraldine chooses v ′ ∈ ∆(v, a) and moves to (I ′ , v ′ ) where I ′ = ∆(I, a) ∩ obs(v ′ ). In A, a play (I 0 , v 0 )(I 0 , v 0 , a 1 )(I 1 , v 1 ) . . . is winning for SuperRoberta if it reaches a position (I, v) with I ⊆ S, otherwise it is winning for Geraldine.

Theorem 4 [START_REF] Maubert | Games with Opacity Condition[END_REF] Gerald has a winning strategy in A, if and only if, Geraldine has a winning strategy in the perfect-information game A.

It is well known that perfect-information reachability games and perfectinformation safety games are solvable in PTIME. Since the constructions of A and A involve a single exponential blow-up, it follows from Theorems 3 and 4 that the opacity-violate and opacity-guarantee problems are in EXPTIME.

Matching lower bounds

We prove here that the opacity-violate and the opacity-guarantee problems are EXPTIME-hard.

First, EXPTIME-hardness of the opacity-violate problem is proved by a reduction from reachability imperfect-information games of [START_REF] Reif | The complexity of two-player games of incomplete information[END_REF]. Recall that a reachability imperfect-information game is a game of imperfect information A = (V, F, ∆, obs, act, v 0 ) over Σ and Γ with a distinguished set of target observations F ⊆ Γ that Robert aims at reaching.

Theorem 5 [START_REF] Reif | The complexity of two-player games of incomplete information[END_REF] Solving reachability imperfect-information games is EXPTIMEcomplete.

The reduction is straightforward. Let A = (V, F, ∆, obs, act, v 0 ) be a reachability imperfect-information game over Σ and Γ. We define the game with opacity condition A ′ := (V, ∆, obs, act, v 0 , S) over Σ and Γ, where S = γ∈F γ. It is easy to see that solving the reachability imperfect-information game A is equivalent to solving the opacity-violate problem in the game A ′ : a winning strategy for Robert to reach F in A is also a winning strategy for Robert in A ′ , and vice versa (remember that the information set is always a subset of the current observation).

We now show that the opacity-guarantee problem is EXPTIME-hard by a polynomial-time reduction from the acceptance problem of the empty input string for linearly-bounded alternating Turing Machines (TM) with a binary branching degree, which is EXPTIME-complete [START_REF] Chandra | Alternation[END_REF]. The key idea is to encode TM configurations by the information sets.

In the rest of this section, we fix such a TM machine

M = (B, Q = Q ∀ ∪ Q ∃ ∪ {q acc , q rej }, q 0 , δ), where B is the input alphabet, Q ∃ (resp. Q ∀ ) is the set of existential (resp. universal) states, q 0 ∈ Q is the initial state, q acc / ∈ Q ∀ ∪ Q ∃ is the (terminal) accepting state, q rej / ∈ Q ∀ ∪ Q ∃ is the (terminal) rejecting state, and δ : (Q ∀ ∪ Q ∃ ) × B → (Q × B × {+1, -1}) × (Q × B × {+1, -1})
is the transition function. In each non-terminal step (i.e., the current state is in Q ∀ ∪ Q ∃ ), M overwrites the tape cell being scanned, and the tape head moves one position to the left (-1) or right (+1). Let n be the size of M and [n] = {1, . . . , n}. We assume that n > 1.

Since M is linearly bounded, we can assume that M uses exactly n tape cells when started on the empty input string ε. Hence, a configuration (of

M over ε) is a word C = w 1 (q, b) w 2 ∈ B * • (Q × B) • B * of
length exactly n denoting that the tape content is w 1 b w 2 , the current state is q, and the tape head is at position |w 1 | + 1. The initial configuration C init is given by (q 0 , ) n-1 , where is the blank symbol. Moreover, without loss of generality, we assume that when started on C init , no matter what are the universal and existential choices, M always halts by reaching a terminal configuration C, i.e. such that the associated state, written q(C), is in {q acc , q rej } (this assumption is standard, see [START_REF] Chandra | Alternation[END_REF]). For a non-terminal configuration C = w 1 (q, b) w 2 (i.e. such that q ∈ Q ∃ ∪ Q ∀ ), we denote by succ L (C) (resp. succ R (C)) the successor of C obtained by choosing the left (resp. the right) triple in δ(q, b). An accepting computation tree of M over ε is a finite tree T whose nodes are labeled by configurations and such that the root is labeled by C init , the leaves are labeled by accepting configurations C, i.e. q(C) = q acc , each internal node x is labeled by a non-terminal configuration C, and: (1) if C is existential (i.e., q(C) ∈ Q ∃ ), then x has exactly one child whose label is one of the two successors of C, and (2) if C is universal (i.e., q(C) ∈ Q ∀ ), then x has exactly two children corresponding to the two successors succ L (C) and succ R (C) of C. We construct a game with opacity condition A M such that Gerald has a winning strategy in A M if, and only if, there is an accepting computation tree of M over ε (Theorem 6). Hence, EXPTIME-hardness of the opacity-guarantee problem follows.

In the game A M , the tape content can be retrieved from the current information set (of size n), and the remaining information about the current configuration is available in each position of the information set. A step of the machine is simulated by two rounds of the game: in the first round, depending on whether the current state is universal or existential, Robert simulates the universal choice of the next configuration or Gerald simulates the existential choice, and the second round simulates the updating of the configuration of the machine.

Here, we describe the construction of the game A M = (V, ∆, obs, act, v 0 , S).

1. V = {v 0 , saf e L , saf e R , saf e choice }∪ ([n]×B)×([n]×Q×B)×{L, R, choice} . 2. obs : V → Γ = {γ 0 , γ choice , γ L , γ R } is defined by obs(v) =        γ 0 if v = v 0 γ L if v ∈ {saf e L } ∪ ([n] × B) × ([n] × Q × B) × {L} γ R if v ∈ {saf e R } ∪ ([n] × B) × ([n] × Q × B) × {R} γ choice otherwise. 3. act : Γ → Σ = {∀ L , ∀ R , ∃} ∪ B is defined by act(γ) =    Σ if γ = γ 0 {∀ L , ∀ R , ∃} if γ = γ choice B otherwise. 4. S = ([n] × B) × ([n] × {q rej } × B) × {choice}.
We delay the formal definition of ∆ : V × Σ → 2 V \∅ after informally describing the running of the game. A configuration C is encoded by an information set I f (C) of the form

{((1, b 1 ), (i, q(C), b i ), f ), . . . , ((n, b n ), (i, q(C), b i ), f )}
where f ∈ {L, R, choice}, i is the position of the tape cell of C being scanned, and for each 1

≤ j ≤ n, b j is the content of the j-th cell. For each f ∈ {L, R, choice}, I f (C) is called the f -code of C
, and during a play, the current information set is of the form I f (C) for some reachable configuration C of the machine, unless Robert happened to have made some deviating move which does not simulate the dynamics of M. We capture this deviation by making Robert lose: technically, the play enters one of the safe positions saf e L , saf e R , or saf e choice that do not belong to the set S of secrets; then, once a safe position is reached, only other safe positions can be reached, yielding Gerald to win, whatever Robert does in the future. Note that for each f ∈ {L, R}, I f (C) does not violate the opacity condition for S, and I choice (C) violates the opacity condition for S if, and only if, C is rejecting (i.e. q(C) = q rej ). For all q ∈ Q ∃ ∪ Q ∀ and b ∈ B, we denote by δ L (q, b) (resp. δ R (q, b)) the left (resp. right) triple in δ(q, b). The behavior of A M is as follows:

First round: From the initial position v 0 , whatever Robert and Gerald choose, the information set at the end of the first round is I choice (C init ), the choice-code of the initial configuration.

The current information set is I choice (C) for some terminal configuration C: If C is rejecting, then I choice (C) ⊆ S and Gerald loses. Otherwise, I choice (C) ⊆ S and independently of the move of Robert, the play reaches a safe position saf e dir for some dir ∈ {L, R} and Gerald wins.

As we shall see, there remain only two cases, which in turn simulate a complete step of M.

The current information set is I choice (C) for some non-terminal configuration C:

Let v = ((k, b k ), (i, q(C), b i ), choice)
be the current position (corresponding to some position in I choice (C)). From obs(v), Robert can only choose actions in {∃, ∀ L , ∀ R }. There are again two cases.

C is existential (note that this information is contained in the position v). Moves ∀ L and ∀ R of Robert are deviating and the play reaches one of the safe positions saf e L or saf e R , thus Gerald wins. If instead Robert's move is ∃, the following move dir ∈ {L, R} of Gerald aims at simulating the existential choice of M in the configuration configuration C. The reached position is then

v ′ = ((k, b k ), (i, q(C), b i ), dir).
C is universal. The move ∃ of Robert is deviating and the following move of Gerald can lead only to saf e L or saf e R , which makes him win. Instead Robert's move ∀ dir ∈ {∀ L , ∀ R } simulates the universal choice of M in the configuration C. Next, Gerald's move is unique and leads to the position v ′ = ((k, b k ), (i, q(C), b i ), dir).

Whatever the type of the configuration C was, by letting the observation classes split positions with different values of dir (see the definition of obs above), the information set after the move of Gerald becomes I dir (C), unless Robert's move was deviating.

The current information set is I dir (C) with dir ∈ {L, R}, for some nonterminal configuration C:

Let the current position be v = ((k, b k ), (i, q(C), b i ), dir) ∈ I dir (C), and let δ dir (q(C), b i ) = (q dir , b dir , θ dir ).
The value j = i + θ dir represents the position of the cell being scanned in the next configuration succ dir (C); note that the value j is easily computable from the current position v.

In order however to complete the step of the machine and to reach the information set I choice (succ dir (C)), the value of b j must be provided by the game. Therefore, we let b j be the only non-deviating move of Robert from position v ∈ I dir (C), among the possible moves in B.

From position v = ((k, b k ), (i, q(C), b i ), dir), the above behavior is implemented as follows. Let b be the action chosen by Robert. If k / ∈ {i, j}, tape cell k is unchanged by the step of the machine, hence the only possible move of Gerald leads to ((k, b k ), (j, q dir , b), choice). If k = i, tape cell i is overwritten, hence the move of Gerald is unique and leads to INRIA ((i, b dir ), (j, q dir , b), choice). Finally, if k = j, there are two cases. If b = b j , then Gerald can only move to ((j, b j ), (j, q dir , b j ), choice) which updates the data for the next configuration succ dir (C), otherwise the move b ( = b j ) of Robert is deviating (and the play reaches a safe position).

We can now formally define the moves in A M , by letting ∆ : V × Σ → 2 V \∅ be:

Case v = v 0 : ∆(v, a) = {((h, ), (1, q 0 , ), choice) | h ∈ [n]} Case v = saf e choice : ∆(v, a) = {saf e dir | dir ∈ {L, R}} Case v = saf e dir ,
where dir ∈ {L, R}:

∆(v, a) = {saf e choice } Case v = ((h, b), (i, q, b ′ ), choice): ∆(v, a) =        {((h, b), (i, q, b ′ ), dir) | dir ∈ {L, R}} if a = ∃ and q ∈ Q ∃ {((h, b), (i, q, b ′ ), L)} if a = ∀ L and q ∈ Q ∀ {((h, b), (i, q, b ′ ), R)} if a = ∀ R and q ∈ Q ∀ {saf e dir | dir ∈ {L, R}} otherwise Case v = ((h, b), (i, q, b ′ ), dir)
, where dir ∈ {L, R}, q / ∈ {q rej , q acc }, and

δ dir (q, b ′ ) = (q dir , b dir , θ dir ): ∆(v, a) =        {((h, b), (i + θ dir , q dir , a), choice)} if a ∈ B and h / ∈ {i, i + θ dir } {((h, b dir ), (i + θ dir , q dir , a), choice)} if a ∈ B and h = i {((h, b), (i + θ dir , q dir , b), choice)} if a = b and h = i + θ dir {saf e choice } otherwise Case v = ((h, b), (i, q, b ′ ), dir)
, where dir ∈ {L, R} and q ∈ {q rej , q acc }:

∆(v, a) = {((h, b), (i, q, b ′ ), choice)}
This achieves the construction of the game A M which satisfies the following:

Theorem 6 There is an accepting computation tree of M over ε if, and only if, there is a winning strategy of Gerald in the game A M .

The rest of this section is dedicated to the proof of Theorem 6. First, we need additional definitions. For each v ∈ V , we denote by A v M the game (V, ∆, obs, act, v, S), i.e. the game defined exactly as A M with the unique difference that the initial position is v. A play of A M starting from v is a play of A v M . Similarly, a strategy of Gerald from position v, is a strategy of Gerald in the game A v M . Given a play ρ = v ′ 0 a 1 v ′ 1 . . . from v ′ 0 = v and a set I 0 ⊆ V such that v ∈ I 0 , for each k ≥ 0, the information set I(ρ k , I 0 ) of the prefix ρ k of ρ w.r.t. I 0 is inductively defined as I(ρ k ) with the unique difference that initially we set I(ρ 0 , I 0 ) = I 0 . In particular, if

I 0 = {v}, then I(ρ k , I 0 ) = I(ρ k ) RR n°1978
for each k ≥ 0. Let β be a strategy of Gerald from position v. An outcome of

β is a play ρ = v ′ 0 a 1 v ′ 1 . . . starting from position v such that for each k > 0, v ′ k = β(ρ k-1 a k ). Given I 0 ⊆ V such that v ∈ I 0 ,
we say that β is winning for Gerald w.r.t. I 0 if, and only if, for each outcome ρ of β and k ≥ 0, I(ρ k , I 0 ) ⊆ S. Note that for I 0 = {v}, the above notion corresponds to the notion of winning strategy of Gerald in the game A v M . The full computation tree of M (over ε) T f ull is the tree whose nodes are labeled by configurations such that: (1) the root is labeled by C init , (2) each leaf node is labeled by a terminal configuration, and (3) each internal node x is labeled by a non-terminal configuration C and has two children labeled by succ L (C) and succ R (C), respectively. By our assumptions, T f ull is finite. For a configuration C, we say that C is reachable if there is some node in T f ull which is labeled by C. Note that for all nodes x and x ′ of T f ull , if x and x ′ are labeled by the same configuration, then the subtrees rooted at x and x ′ are isomorphic. Thus, if C is a reachable configuration, we denote by height(C) the height of any subtree of T f ull rooted at a node labeled by C. Furthermore, if C is a reachable configuration, we say that C leads to acceptance if, and only if, the following is inductively satisfied: or (1) C is accepting, or (2) C is an existential configuration and succ dir (C) leads to acceptance for some dir ∈ {L, R}, or (3) C is an universal configuration and succ dir (C) leads to acceptance for each dir ∈ {L, R}. Evidently, there is an accepting computation tree of M over ε if, and only if, C init leads to acceptance. Now, we prove some preliminary results.

Claim 1: Let v ∈ V and v saf e be a safe position in {saf e L , saf e R , saf e choice } such that obs(v) = obs(v saf e ) (note that v and v saf e can coincide). Then, for each I 0 ⊆ V such that v, v saf e ∈ I 0 and play ρ starting from v, the following holds: for each k ≥ 0, I(ρ k , I 0 ) ⊆ S.

Proof of Claim 1:

Let ρ = v ′ 0 a 1 v ′ 1 . . . with v ′ 0 = v.
Since each safe position in {saf e L , saf e R , saf e choice } is not in the secret S, it suffices to show that for each k ≥ 0, I(ρ k , I 0 ) contains a safe position v k,saf e and obs(v k,saf e ) = obs(v ′ k ). This is proved by induction on k ≥ 0. The base case (k = 0) is obvious. Now, assume that I(ρ k , I 0 ) contains some safe position v k,saf e such that obs(v k,saf e ) = obs(v ′ k ). There are three cases: • obs(v k,saf e ) = saf e L : hence, obs(v k,saf e ) = obs(v ′ k ) = γ L . By definition of the transition function, obs(v ′ k+1 ) = γ choice , and ∆(saf e L , a k+1 ) = {saf e choice }. Since obs(v ′ k+1 ) = obs(saf e choice ) and saf e choice ∈ ∆(I(ρ k , I 0 ), a k+1 ), the result follows.

• obs(v k,saf e ) = saf e R : this case is similar to the previous one.

• obs(v k,saf e ) = saf e choice : hence, obs(v k,saf e ) = obs(v ′ k ) = γ choice . By definition of the transition function, obs(v ′ k+1 ) = γ dir for some dir ∈ {L, R}. Moreover, ∆(saf e choice , a k+1 ) = {saf e L , saf e R }. Since obs(v ′ k+1 ) = obs(saf e dir ) and saf e dir ∈ ∆(I(ρ k , I 0 ), a k+1 ), the result follows.

Claim 2: Let C be a reachable configuration which leads to acceptance. Then, for each v ∈ I choice (C), there is a winning strategy of Gerald from position v w.r.t. I choice (C).

Proof of Claim 2:

The proof is by induction on height(C).

INRIA

Base case: height(C) = 0, hence C is a terminal configuration. Since C leads to acceptance, C is accepting. Let v ∈ I choice (C). We show that each play from v satisfies the opacity condition for S, hence the result follows. Let ρ = v ′ 0 a 1 v ′ 1 . . . be a play from v. By definition of the transition function, v ′ 1 ∈ {saf e R , saf e L }. By Claim 1, it follows that for each k > 0, I(ρ k ) ⊆ S. Since v ′ 0 = v / ∈ S, the result follows. Induction step: height(C) > 0, hence C is a non-terminal configuration. There are two cases:

• C is universal: since C leads to acceptance, succ dir (C) leads to acceptance for each dir ∈ {L, R}. Since height(succ dir (C)) < height(C) for each dir ∈ {L, R}, by the induction hypothesis, it follows that for each v ∈ I choice (succ dir (C)), there is a winning strategy β v dir of Gerald from position v w.r.t. I choice (succ dir (C)). Let v ∈ I choice (C). We define a strategy β v : v(ΣV ) * Σ → V of Gerald from position v as follows. For all k ≥ 0, a ∈ Σ, and w ∈ (ΣV ) k , β v (vwa) is defined as follows:

k ≤ 1: let v ′ be the last position in w and v ′′ be an arbitrary position in ∆(v ′ , a). We set

β v (vwa) = v ′′ . -k > 1: hence, vwa can be written in the form va 1 v 1 a 2 v 2 w ′ a. If v 2 ∈ I choice (succ dir (C)) for some dir ∈ {L, R}, we set β v (vwa) = β v2 dir (v 2 w ′ a).
Otherwise, let v ′ be the last position in w and v ′′ be an arbitrary position in ∆(v ′ , a). We set β v (vwa) = v ′′ . Now, we show that β v is a winning strategy for Gerald from position v w.r.t. I choice (C). Let ρ = v ′ 0 a 1 v ′ 1 . . . be an outcome of β v (hence, v ′ 0 = v). We need to show that ρ is winning for Gerald w.r.t. I choice (C), i.e. for each k ≥ 0, I(ρ k , I choice (C)) ⊆ S. By definition of the transition function, either v ′ 1 ∈ {saf e L , saf e R } or there is dir ∈ {L, R} such that v ′ 1 is the position in I dir (C) associated with v. In the first case, since I choice (C) ⊆ S, by Claim 1, we deduce that I(ρ k , I choice (C)) ⊆ S for each k ≥ 0. Thus, in this case, the result holds. Now, assume that v ′ 1 is the position in I dir (C) associated with v. By definition of the transition function, a 1 = ∀ dir , and we easily deduce that I(ρ 1 , I choice (C)) = I dir (C). Moreover, ∆(v ′ 1 , a 2 ) is a singleton and there are two cases: either I(ρ 2 , I choice (C)) contains the safe position saf e choice or I(ρ 2 , I choice (C)) = I choice (succ dir (C)). In the first case, since I(ρ k , I choice (C)) ⊆ S for each k = 0, 1, the result directly follows from Claim 1. In the second case, v ′ 2 ∈ I choice (succ dir (C)), and by definition of

β v , the suffix v ′ 2 a 2 v ′ 3 . . . of ρ is an outcome of strategy β v ′ 2 dir
. Since this suffix is winning for Gerald w.r.t. I choice (succ dir (C)), the result follows.

• C is existential: since C leads to acceptance, there is dir ∈ {L, R} such that succ dir (C) leads to acceptance. Since height(succ dir (C)) < height(C), by the induction hypothesis, we have that for each v ∈ I choice (succ dir (C)), there is a winning strategy β v dir of Gerald from position v w.r.t. I choice (succ dir (C)). Let v ∈ I choice (C). We define a strategy β v : v(ΣV ) * Σ → V of Gerald from position v as follows. For all k ≥ 0, a ∈ Σ, and w ∈ (ΣV ) k , β v (vwa) is defined as follows: k = 1: let w = a 1 v 1 and v 2 be an arbitrary position in ∆(v 1 , a). We set β v (vwa) = v 2 .

-k = 0: since C is
k > 1: hence, vwa can be written in the form va

1 v 1 a 2 v 2 w ′ a. If v 2 ∈ I choice (succ dir (C)), we set β v (vwa) = β v2 dir (v 2 w ′ a).
Otherwise, let v ′ be the last position in w and v ′′ be an arbitrary position in ∆(v ′ , a). We set β v (vwa) = v ′′ . Now, we show that β v is a winning strategy for Gerald from position v w.r.t.

I choice (C). Let ρ = v ′ 0 a 1 v ′ 1 . . . be an outcome of β v (hence, v ′ 0 = v).
We need to show that ρ is winning for Gerald w.r.t. I choice (C). By definitions of the transition function and strategy

β v , either v ′ 1 ∈ {saf e L , saf e R } or v ′
1 is the position in I dir (C) associated with v. In the first case, since I choice (C) ⊆ S, by Claim 1, we deduce that I(ρ k , I choice (C)) ⊆ S for each k ≥ 0. Thus, in this case, the result holds. Now, assume that v ′ 1 is the position in I dir (C) associated with v. By definition of the transition function, a 1 = ∃, and we easily deduce that I(ρ Proof of Theorem 6: First, assume that there is an accepting computation tree of M over ε. Hence, C init leads to acceptance. By Claim 2, for each position v ∈ I choice (C init ), there is a winning strategy β v of Gerald from position v w.r.t. I choice (C init ). Moreover, by the definition of the transition function, each play (from the initial position) has the form ρ = v 0 a 0 v . . . such that v ∈ I choice (C init ) and I(ρ 1 ) = I choice (C init ). Let β be the strategy of Gerald defined as follows:

1 , I choice (C)) = I dir (C). Moreover, ∆(v ′ 1 , a 2 )
• for each a ∈ Σ, β(v 0 a) is an arbitrary position in ∆(v 0 , a);

• for each a 1 v 1 w ∈ (ΣV ) * and a ∈ Σ, if v 1 / ∈ I choice (C init ), then β(v 0 a 1 v 1 wa) is some arbitrary position in ∆(v ′ , a)
, where v ′ is the last position in a 1 v 1 w; otherwise, we set β(v 0 a 1 v 1 wa) = β v1 (v 1 wa).

Evidently, β is a winning strategy of Gerald. Now, assume that there is a winning strategy β of Gerald. Let v be an arbitrary position in I choice (C init ) and let β v be the strategy of Gerald from position v defined as follows: for each a ∈ Σ and w ∈ (ΣV ) * , β v (vwa) = β(v 0 a 0 vwa). Since β is winning for Gerald, by definition of the transition function, it follows that β v is a winning strategy of Gerald from position v w.r.t. I choice (C init ). By Claim 3, it follows that C init leads to acceptance. Hence, there is an accepting computation tree of M over ε, which concludes.

Blindfold games with opacity condition

We recall that a game with imperfect information is blindfold if all positions have the same observation.

Lemma 7 Let A = (V, ∆, obs, act, v 0 ) be a blindfold game with imperfect information over Σ and Γ = {γ}. For every play prefix

ρ n = v 0 a 1 v 1 . . . a n v n , I(ρ n ) = ∆({v 0 }, a 1 . . . a n ).
The proof is trivial, by applying the definition of the information set. In blindfold games Robert cannot base the choice of his actions on anything because he sees nothing of what Gerald does. So a strategy for Robert is just an infinite sequence of actions. More formally: Lemma 8 Let A = (V, ∆, obs, act, v 0 ) be a blindfold game with imperfect information over Σ and Γ = {γ}, let α be a strategy for Robert, then there exists a 1 a 2 a 3 . . . ∈ Σ ω such that for all strategies β and β ′ for Gerald, obs(α β) = obs(α β ′ ) = v 0 a 1 γa 2 γ . . .

In the rest of this section we prove the following two theorems: Theorem 9 Blindfold games with opacity condition are determined.

Theorem 10 For blindfold games with opacity condition, the opacity-guarantee problem and the opacity-violate problem are PSPACE-complete.

Both theorems are proved by considering a third problem: the opacity-verify problem which addresses the strong ability for Gerald to win the game. We define this problem and establish its PSPACE-completeness in the general setting of games with opacity condition and also in the particular case of blindfold games (Theorem 11). We finally compare it to the opacity-violate and opacityguarantee problems for blindfold games (Theorem 14).

Definition 5 Given a game with opacity condition A = (V, ∆, obs, act, v 0 , S), the opacity-verify problem is to decide whether the following property holds:

∀β, ∀α, α β is S-opaque (1)
If Property (1) holds, any strategy β of Gerald is a winning-strategy. Otherwise, there exists a play in the game that is not S-opaque.

Theorem 11

The opacity-verify problem is PSPACE-complete, even for blindfold games.

For the PSPACE membership, we design an algorithm that decides whether there exists a losing play for Gerald, which is clearly equivalent to deciding whether there exists a strategy of Gerald that is not winning. The algorithm runs in NPSPACE, hence in PSPACE [START_REF] Savitch | Relationships between nondeterministic and deterministic tape complexities[END_REF], by nondeterministically choosing the moves for Robert and Gerald, and by updating the current information set of Robert at each round. Since information sets are subsets of the set of positions, if there are n positions, we need O(n) space to run this algorithm. The PSPACE-hardness of the opacity-verify problem results from a reduction from the universality problem for a complete nondeterministic finite automaton (NFA), known to be PSPACE-complete [START_REF] Stockmeyer | Word problems requiring exponential time (Preliminary Report)[END_REF]. This reduction was initially inspired by [START_REF] Dubreil | Monitoring and Supervisory Control for Opacity Properties[END_REF] but is in fact a variant of the one in [START_REF] De Wulf | Antichains: A new algorithm for checking universality of finite automata[END_REF].

We recall that a NFA

A = (Q, Σ, ∆, Q 0 , Q f ) is a nondeterministic finite automaton with states Q, alphabet Σ, transition relation ∆ : Q × Σ → 2 Q
and sets of (respectively) initial and accepting states Q 0 and Q f . A NFA A is complete if for every state q and letter a, ∆(q, a) = ∅. The language L(A) ⊆ Σ * of A is the set of words w ∈ Σ * such that ∆(Q 0 , w) ∩ Q f = ∅. The universality problem is to decide whether A accepts all possible finite words, i.e L(A) = Σ * . Given a complete NFA A = (Q, Σ, ∆, Q 0 , Q f ), define the blindfold game with opacity condition A A = (Q ∪ {q 0 }, ∆ ′ , obs, act, q 0 , S) over Σ and Γ = {γ}, with q 0 / ∈ Q, as follows:

S = Q\(Q f ∪ {q 0 }) INRIA act(γ) = Σ ∀q ∈ Q ∪ {q 0 }, obs(q) = γ ∀a ∈ Σ, ∆ ′ (q, a) = Q 0 if q = q 0 ∆(q, a) otherwise
Since, firstly, q 0 is not reachable after the first move, secondly, ∆ ′ (q, a) = ∆(q, a) for q = q 0 and finally, ∆ ′ (q 0 , a) = Q 0 for all a, we obtain from lemma 7 the following corollary :

Corollary 12 For each play prefix in A A of the form ρ n = q 0 a 1 q 1 . . . a n q n with n ≥ 1, I(ρ n ) = ∆(Q 0 , a 2 . . . a n )
One may note that the aim of the initial position q 0 is to initialise Robert's information set to Q 0 at the end of the first round.

Proposition 13

The NFA A is universal if, and only if, in A A , every strategy of Gerald is winning.

Proof We start with the right-left implication. Assume that every strategy is winning for Gerald. Take one strategy β, and take a word w ∈ Σ * . Consider a play ρ in wich Robert's first moves form the sequence of actions aw, for some a in Σ, and Gerald follows strategy β. This is possible because the underlying automaton is complete. Being ρ induced by the winning strategy β, it is S-opaque, hence in particular I(ρ 1+|w| ) S. By Corollary 12 we obtain : ∆(Q 0 , w) S, which implies that there exists a position q in ∆(Q 0 , w) that is in Q f , hence A accepts w. A is universal.

For the other implication, suppose that A is universal. Let β be a strategy of Gerald, and let ρ be a play induced by β. We prove that ρ is S-opaque. Let n ∈ N. If n = 0, I(ρ n ) = {q 0 } S. If n > 0, there exists w in Σ * such that I(ρ n ) = ∆(Q 0 , w) (Corollary 12). Since A is universal it accepts w, hence ∆(Q 0 , w) ∩ Q f = ∅. So I(ρ n ) S, and this finishes the proof.

Theorem 14 In a blindfold game with opacity condition, the opacity-verify problem, the opacity-guarantee problem and the complementary of the opacityviolate problem are equivalent.

Proof Let A = (V, ∆, obs, act, v 0 , S) be a blindfold game with opacity condition. It is clear that in general, ∀β, ∀α, α β is S-opaque ⇒ ∃β, ∀α, α β is S-opaque

We prove the converse in the case of blindfold games. Suppose that there exists a winning strategy β for Gerald. We prove that any strategy β ′ is also winning.

Let α be a strategy for Robert. Since A is blindfold, by Lemma 8 we have that obs(α β) = obs(α β ′ ), so for every n ∈ N, I(α β ′ n ) = I(α β n ) S.

So we have that the opacity-verify problem is equivalent to the opacityguarantee problem in blindfold games. We now show that the opacity-verify problem is also equivalent to the complementary of the opacity-violate problem (decide whether ∀α, ∃β s.t. α β is S-opaque holds).

Once again one implication is trivial : ∀β, ∀α, α β is S-opaque ⇒ ∀α, ∃β, α β is S-opaque Now the other way. Suppose that for any strategy α there is a strategy β for Gerald such that α loses. Now take any couple of strategies (α, β ′ ). We know that there exists a strategy β such that α β is S-opaque. But we also know (Lemma 8) that obs(α β) = obs(α β ′ ) because the game is blindfold, so once again for every n ∈ N, I(α β ′n ) = I(α β n ) S.

The idea behind this theorem is that in blindfold games with opacity condition, the outcome of a play does not rely on Gerald's behaviour but only on what Robert plays. Indeed, since he observes nothing of what Gerald does, Robert's information set, and so the winning condition, are only determined by the series of actions he chooses. Thus, these games via a power-set construction can be seen as (reachability) one-player games: each position is a reachable information set I, at each step the unique player (Robert) chooses an action a ∈ act(I), where I is the current position, and moves to position ∆(I, a). Therefore, in blindfold games with opacity condition, whether Robert has a winning strategy (i.e a winning sequence of actions), or Gerald wins whatever he does.

The determinacy of blindfold games with opacity condition (Theorem 9) is an immediate corollary of the above Theorem 14. Also Theorem 10 results from Theorems 14 and 11.

Related work

Opacity has mostly been studied in the framework of discrete-event systems and their theory of control ( [START_REF] Saboori | Opacity-enforcing supervisory strategies for secure discrete event systems[END_REF][START_REF] Dubreil | Opacity enforcing control synthesis[END_REF]). It is both interesting and important to know to what extent the classical problems in this field can be embedded into our games. We first describe the discrete-event system setting, next we define the notion of opacity in this framework. We finally propose a translation from the verification of opacity in this setting to the opacity-verify problem in games with opacity condition.

First we recall that a a deterministic finite automaton (DFA) is a NFA A = (Q, Σ, δ, q 0 , Q f ) but with a unique initial state q 0 and in which the transition relation δ : Q × Σ → 2 Q satisfies |δ(q, a)| ≤ 1 for all states q and input symbols a.

The problem of opacity is defined in [START_REF] Dubreil | Opacity enforcing control synthesis[END_REF] with regards to a LTS G (labelled transition system, i.e a DFA without accepting states) and a confidential predicate φ over execution traces of G, representable by a regular language L φ ⊆ Σ * where Σ is the set of events of the transition system. For convenience, we equivalently state it on a DFA A φ G representing the transition system together with the secret predicate. The automaton A φ G is simply the synchronized product of G with some complete DFA accepting L φ . We denote by T (A) ⊆ Σ * the set of execution traces of an automaton A, and by L(A) the language accepted by A, so we have that T (A φ G ) = T (G) and L(A φ G ) = T (G) ∩ L φ . From now on, for a DFA A, a state q and w ∈ T (A), δ(q, w) shall denote the only state it contains.

We consider a subset of events Σ a ⊆ Σ which denotes the observation capabilities of a potential attacker of the system, and we let P Σa be the projection function from Σ * to Σ * a . Two words w and w ′ are observationally equivalent if INRIA P Σa (w) = P Σa (w ′ ). We denote by [w] a = P -1 Σa (P Σa (w)) the set of words in Σ * that are observationally equivalent to the word w with regard to Σ a .

Definition 6 L φ is opaque w.r.t. T (G) and Σ a if ∀w ∈ T (G), [w] a ∩ T (G) L φ
This means that L φ is opaque w.r.t. T (G) and Σ a if, and only if, whenever an execution trace of G verifies the confidential predicate φ there exists another possible execution trace observationally equivalent that does not verify φ.

We take an instance of the opacity verification problem, A φ G = (Q, Σ, δ, q G 0 , Q f ), and we describe the construction of the game with opacity condition A φ G such that the following holds.

Theorem 15 Verifying that L φ is opaque w.r.t T (G) and Σ a is equivalent to deciding the opacity-verify problem in A φ G .

The construction starts from A φ G where transitions labelled by events in Σ\Σ a are turned into ǫ-transitions. Then we remove those ǫ-transitions as described in [START_REF] Hopcroft | Automata theory, languages, and computation[END_REF] by taking the ǫ-closure of the transition function, and we obtain the ǫ-free nondeterministic finite automaton

A ǫ = (Q, Σ a , ∆ ǫ , Q ǫ 0 , Q f ).
In this automaton, transitions are all labelled by observable events. One should think of the nondeterminism in this automaton as the uncertainty the attacker has concerning the behaviour of the system. More precisely, she does not know when an observable event is triggered whether the system takes "invisible" transitions or not, may it be before, after, or both before and after the observable one.

We need the following lemma, which is a mere consequence of the construction :

Lemma 16 ∀w ∈ Σ * a , ∆ ǫ (Q ǫ 0 , w) = {δ(q G 0 , w ′ ) | w ′ ∈ [w] a ∩ T (G)}
We can now define the game A φ G = (V, ∆, obs, act, v 0 , S) over Σ

′ = { √ } and Γ = {γ x | x ∈ Σ a } ∪ {γ ǫ }: • V = Q × Σ a ∪ Q ǫ 0 × {ǫ} ∪ {v init }. • ∆(v, √ ) = {(q ′ , y) | y ∈ Σ a , q ′ ∈ ∆ ǫ (q, y)} if v = (q, x) {(q, ǫ) | q ∈ Q ǫ 0 } if v = v init • ∀(q, x) ∈ V, obs((q, x)) = γ x , and obs(v init ) = γ ǫ • ∀v ∈ V, act(v) = { √ } • S = {(q f , x) | q f ∈ Q f , x ∈ Σ a ∪ {ǫ}} and v 0 = v init
Remark 3 Without loss of generality we can assume that in every state q of A ǫ there exists an event y in Σ a such that ∆ ǫ (q, y) is not empty. So in every position (q, x) in V , ∆((q, x), √ ) is not empty, and the game can always continue.

Strategies for Gerald

In this section we consider some aspects of strategies for Gerald. We first recall the notion of memory of a strategy. A play ρ = v 0 a 1 v 1 . . . is consistent with B if there is a sequence of memory states m 1 m 2 . . . such that m i ⇒ vi,ai+1 vi+1 m i+1 for i = 0, 1, 2, . . .. A strategy β has finite memory of size k if it is realized by a strategy automaton B with |M | = k, in the following sense: for every play ρ = v 0 a 1 v 1 . . . induced by β, ρ is consistent with B. In that case, for all i, m i ⇒ vi,ai+1 β(ρ i ai+1) m i+1 .

Theorem 18 Deciding whether a given finite-memory strategy β is winning for Gerald is PSPACE-complete in the size of the game and the size of the memory.

Proof We first give an algorithm that takes as input a game A and a strategy automaton realyzing strategy β, runs in NPSPACE, hence PSPACE [START_REF] Savitch | Relationships between nondeterministic and deterministic tape complexities[END_REF], and accepts if β is not winning in A. This algorithm simply nondeterministically chooses actions for Robert while moves for Gerald are obtained by running the strategy automaton, and at each round the new information set is computed and it is checked whether it is contained in S or not. Clearly one only needs to store in memory the current position in the game, the current state of the strategy automaton and the current information set, hence only O(n) cells are needed if n is the number of positions in the game. So the problem of deciding whether a strategy of Gerald is winning in a game is in coPSPACE = PSPACE in the size of the game and the memory of the strategy. Now for PSPACE-hardness we provide a straightforward reduction of the opacity-guarantee problem in blindfold games. Let A be a blindfold game with opacity condition, as an instance of the opacity-guarantee problem. We construct in linear time a strategy automaton B that realizes a memoryless strategy β of Gerald, and obtain an instance of the problem of deciding whether a finitstate strategy is winning. If β is winning then there exists a winning strategy for Gerald; conversely if there exists one, because of the equivalence of the opacityguarantee and the opacity-verify problem for blindfold games, all strategies for Gerald are winning, hence β is winning. The opacity-guarantee problem being PSPACE-complete in the blindfold setting we obtain the PSPACE-hardness.

Discussion on complexity

Solving safety games with perfect-information is in PTIME, and solving parity games with perfect information is known to be in N P ∩ co-N P [START_REF] Jurdzinski | Deciding the winner in parity games is in UP [intersection] co-UP[END_REF]. However we have seen that deciding whether Gerald, who has perfect-information, has a winning strategy in a game with opacity condition, is EXPTIME-complete, even if we let Robert play with perfect-information (in the sense that his strategies are based on actual prefixes of plays instead of their observation). So the gap between deciding the existence of a winning strategy for a player in perfectinformation games and for Gerald in a game with opacity condition does not come from the fact that Robert has imperfect information, but rather from the nature of the winning condition itself, which is based on the notion of information set, and forces Gerald to keep track of what Robert's information set along the game is.

Similarly, verifying that a finite-state strategy is winning in a safety perfectinformation game can be done in PTIME, whereas Theorem 18 shows that in games with opacity condition, deciding whether a finite-state (and even memoryless) strategy of Gerald is winning is PSPACE-complete in the size of the arena and the memory of the strategy. The idea is that one has to check that the strategy is winning not in all positions, but in all information sets. Concerning the size of the memory needed for Gerald's strategies, we know that an exponential memory is sufficient because if there is a winning strategy there is a memoryless one in the powerset construction. The lower bound for the needed memory is still an open problem.

Finally, note that Theorem 2 gives an EXPTIME lower bound for the model checking of AETL with perfect recall as defined in [START_REF] Dima | Model-checking an alternating-time temporal logic with knowledge, imperfect information, perfect recall and communicating coalitions[END_REF], since solving the opacityviolate problem is equivalent to deciding whether the formula Robert F K Robert S holds in the game arena, where F is the eventuality operator of AETL.

Conclusion and perspectives

Following [START_REF] Maubert | Games with Opacity Condition[END_REF], we have extended the study of games with opacity condition. The opacity condition is an atypical winning condition in imperfect information arenas aiming at capturing security aspects of computer systems. Since games with opacity condition are not determined in general, two dual problems need being considered: the opacity-violate problem and the opacity-guarantee problem, focusing on the player who has imperfect information and on the player who has perfect information respectively. The latter problem is usually equivalent to solving the underlying perfect information game, which explains why it has never been considered; but the fact that our winning condition is based on information sets makes the problem relevant. For both problems, simple power-set constructions apply to convert such games into perfect information ones, that can be solved in polynomial time, hence their upper bound is EXPTIME. On the contrary, the matching EXPTIME lower bound for the opacity-guarantee problem, where the main player has perfect information, was unknown until now and relies on an elegant reduction from the empty input string acceptance problem for linearly-bounded alternating Turing machines. The key point is to encode configurations by information sets. The reduction and its correctness proof are very technical, but we could provide an intuitive informal description.

Finally, we focused on the particular case of blindfold games which offers specific results such as determinacy (Theorem 9) and PSPACE-complete complexities (Theorem 10). The main tool to obtain these results is the opacityverify problem which addresses the question whether any strategy of Gerald is winning. The fact that blindfold games with opacity condition can be seen as INRIA one-player games makes this problem relevant and explains why it is equivalent to the opacity-guarantee problem and to the complement of the opacity-violate problem in the blindfold setting, as we established. We also proved that it is PSPACE-complete, by providing a PSPACE algorithm and a reduction from the nondeterministic finite automata universality problem. The opacity-verify problem is all the more interesting to consider that it naturally demonstrates how the paradigm of opacity condition embraces opacity issues investigated in the recent literature of Control Theory [START_REF] Saboori | Opacity-enforcing supervisory strategies for secure discrete event systems[END_REF][START_REF] Dubreil | Opacity enforcing control synthesis[END_REF].

Games with opacity condition open a novel field in the theoretical aspects of games with imperfect information by putting the emphasis on the player who has perfect information. From this point of view, plethora of questions need being addressed, among which their connection with language-theoretic issues (the synchronizing/directing word problem [START_REF] Černý | Poznámka k. homogénnym experimentom s konecnými automatmi[END_REF][START_REF] Pin | On two combinatorial problems arising from automata theory[END_REF][START_REF] Černý | On directable automata[END_REF], controller synthesis to enforce the opacity of a language [START_REF] Dubreil | Opacity enforcing control synthesis[END_REF]), their logical foundations, and their algorithmic aspects.

  existential, by definition of the transition function if a = ∃, then ∆(v, a) = {v L , v R }, where v L (resp. v R ) is the position in I L (C) (resp. I R (C)) associated with v. In this case, we set β v (va) = v dir . If instead a = ∃, then ∆(v, a) = {saf e L , saf e R }, and we set β v (va) to an arbitrary position in {saf e L , saf e R }.

Claim 3 :

 3 is a singleton and there are two cases: either I(ρ 2 , I choice (C)) contains the safe position saf e choice or I(ρ 2 , I choice (C)) = I choice (succ dir (C)). In the first case, since I(ρ k , I choice (C)) ⊆ S for each k = 0, 1, the result directly follows from Claim 1. In the second case, v ′ 2 ∈ I choice (succ dir (C)), and by definition ofβ v , the suffix v ′ 2 a 2 v ′ 3 . . . of ρ is an outcome of strategy β v ′ 2 dir. Since this suffix is winning for Gerald w.r.t. I choice (succ dir (C)), the result follows. Let C be a reachable configuration and v ∈ I choice (C). If there is a winning strategy of Gerald from position v w.r.t. I choice (C), then C leads to acceptance.Proof of Claim 3: Let β be a winning strategy of Gerald from position v w.r.t. I choice (C). We show by induction on height(C) that C leads to acceptance. Base case: height(C) = 0, hence C is a terminal configuration. By hypothesis I choice (C) ⊆ S. By definition of S, we deduce that C is accepting, and the result follows. Induction step: height(C) > 0, hence C is a non-terminal configuration. Then, there is i ∈ [n] such that v is associated with the i-th cell of C. For each dir ∈ {L, R}, we denote by v dir (resp. v succ dir ) the position in I dir (C) (resp. I choice (succ dir (C))) associated with the i-th cell of C (resp. succ dir (C)). Moreover, let b dir be the content of the cell being scanned in succ dir (C). We distinguish two cases:• C is universal: we show that for each dir ∈ {L, R}, there is a winning strategy β dir of Gerald from position v succ dir w.r.t. I choice (succ dir (C)). Hence, by the induction hypothesis, the result follows. By definition of the transition function, for each dir ∈ {L, R}, there is an outcome ρ dir of β having the form ρ dir = v ∀ dir v dir b dir v succ dir . . . such that I(ρ 2 dir , I choice (C)) = I choice (succ dir (C)). Then, for each w ∈ (ΣV ) * and a ∈ Σ, we setβ dir (v succ dir w a) = INRIA β(v ∀ dir v dir b dir v succ dir w a).Evidently, β dir is a winning strategy of Gerald from position v succ dir w.r.t. I choice (succ dir (C)), and the result holds.• C is existential: we show that there exists dir ∈ {L, R} such that there is a winning strategy β dir of Gerald from position v succ dir w.r.t. I choice (succ dir (C)). Hence, by the induction hypothesis, the result follows. By definition of the transition function, there exists dir ∈ {L, R} and an outcome ρ dir of β having the form ρ dir = v ∃ v dir b dir v succ dir . . . such that I(ρ 2 dir , I choice (C)) = I choice (succ dir (C)). Then, for each w ∈ (ΣV ) * and a ∈ Σ, we set β dir (v succ dir w a) = β(v ∃ v dir b dir v succ dir w a). Evidently, β dir is a winning strategy of Gerald from position v succ dir w.r.t. I choice (succ dir (C)), and the result holds. Now, we prove Theorem 6.

Definition 7

 7 Let A = (V, ∆, obs, act, v 0 , S) be a game with opacity condition over Σ and Γ. A strategy automaton for Gerald is an I/O automaton B = (M, V × Σ, V, m 0 , ⇒) where M is a set of memory states, V × Σ and V are the input alphabet and output alphabet respectively, m 0 is the initial state, and⇒⊆ M × (V × Σ) × V × M is the transition relation that updates the current memory. If m ⇒ v,av ′ m ′ , then B being in state m and reading input (v, a), outputs v ′ and moves to state m ′ .

RR n°1978

We use the superlative "Super" here because in general the winning strategies of SuperGeraldine do not reflect any winning strategy of Gerald in A. She has "more power" than Gerald.

2 act(I) makes sense because an information set is always a subset of a single

observation.[START_REF] Černý | On directable automata[END_REF] we use the superlative "Super" as, contrary to what Roberta could do in the game A, SuperRoberta can take advantage of the extra information.RR n°1978

In this game, Robert is passive. He only observes Gerald, who simulates the system G. If the game is in position (q, x), it represents that we are in state q in the system G, and that the last visible event was x (if x = ǫ, no observable event happened yet). Robert observes γ x , i.e the only information he gains during a play is the sequence of visible events.When Gerald plays, he chooses a visible event y and a state reachable from q through y in A ǫ , which can be seen as choosing as many invisible transitions in G as he wishes, plus one visible amongst them, y. We shall note α √ the only possible strategy for Robert, which is to always play √ . v init is the initial position, that can never be reached after the first move. It is used to initialize Robert's information set to Q ǫ 0 × {ǫ} (these are the only reachable positions from v init , and they have the same observation, γ ǫ ). This represents the set of states in G that are reachable before any observable transition is taken.

We start the proof of Theorem 15 by establishing this central lemma.

Proof The latter fact is obvious, from the definition of observations.

Considering the former fact, we prove it by induction on n.

, so we clearly have :

We move on to the proof of Theorem 15. Suppose that every strategy β is winning for Gerald. We prove that L φ is opaque w.r.t T (G) and Σ a . Take a word w in T (G). There exists a prefix of a play ρ n+1 = v init √ (q 0 , ǫ) √ (q 1 , x 1 ) . . . √ (q n , x n ) such that x 1 . . . x n = P Σa (w). So there exists a strategy β such that α √ β n+1 = ρ n+1 . With lemma 17 and 16 we have that {q

Now suppose that L φ is opaque w.r.t T (G) and take β a strategy for Gerald in A φ G , we prove that β is winning. Let ρ β = α √ β be the only possible play induced by β. Take a prefix ρ n+1 β = v init √ (q 0 , ǫ) √ (q 1 , x 1 ) . . . √ (q n , x n ) of this play. By Lemma 17 and 16 again, {q |

Since an information set is never empty, there exists w in [x 1 . . . x n ] a ∩ T (G), and because L φ is opaque w.r.t T (G), [x 1 . . . x n ] a ∩ T (G) L φ . So there exists w ′ in [x 1 . . . x n ] a ∩T (G) such that δ(q G 0 , w ′ ) = q / ∈ Q f , hence (q, x n ) / ∈ S and I(ρ n β ) S. β is winning.

INRIA