Yackolley Amoussou-Guenou

Souheib Baarir

Maria Potop-Butucaru

Nathalie Sznajder

Léo Tible

Sébastien Tixeuil

On the encoding and solving of partial information games

In this paper we address partial information games restricted to memoryless strategies. Our contribution is threefold. First, we prove that for partial information games, deciding the existence of memoryless strategies is NP-complete, even for games with only reachability objectives. The second contribution of this paper is a SAT/SMT-based encoding of a partial information game altogether with the correctness proof of this encoding. Finally, we apply our methodology to automatically synthesize strategies for oblivious mobile robots. We first prove that synthesizing memoryless strategies is equivalent to providing a distributed protocol for the robots. Then, we use an SMT-solver to synthesize strategies for the gathering problem in a particular configuration (SP4), open case in distributed computing theory for more than a decade. Interestingly, our work is the first that combines two-player games theory and SMT-solvers in the context of mobile robots with promising results and therefore it is highly valuable for distributed computing theory where a broad class of open problems are still to be investigated.

Introduction

Two-player games are a widely used and very natural framework for reactive systems, i.e. that maintain an ongoing interaction with an unknown and/or uncontrollable environment. It is intimately linked to model-checking of µ-calculus [START_REF] Emerson | Tree automata, mu-calculus and determinacy[END_REF] and synthesis of reactive programs (see eg. [START_REF] Büchi | Solving sequential conditions by finite-state strategies[END_REF]). In classical two-player zero-sum games, two players play on a graph. One of the players tries to force the sequence of visited nodes to belong to a (generally ω-regular) subset of infinite paths, called the winning condition. Its opponent tries to prevent her to achieve her goal. When total information is assumed, each player has a perfect knowledge of the history of the play. In a more realistic model in regards to applications to automatic synthesis of programs for instance, the protagonist does not have access to all the information about the game. Indeed, in distributed systems, each component may have an internal state that is unknown by other components. This requires to consider games of partial information, in which only a partial information on the play is disclosed to the players. The main question to solve regarding games in our context is the existence of a winning strategy for the player modeling the system. This is now well understood. We know that total information parity games enjoy the memoryless determinacy property [START_REF] Emerson | Tree automata, mu-calculus and determinacy[END_REF] ensuring that in each game, one of the players has a winning strategy, and that a winning strategy exists if and only if there is a memoryless winning strategy, i.e. a strategy that depends only on the last visited node of the graph, and not on a history of the play. However, partial information games do not enjoy this property since the player may need memory to win the game. On the other hand, regarding tools implementations, the field of two-player games has not reached the maturity obtained in model-checkers area. For total information games, to the notable exception of pgsolver [24] that provides a platform of implementation for algorithms solving parity games, and Uppaal-TiGa [30] that solves in a very efficient way timed games (but restricted to reachability conditions), few implementations are available. SAT-implementations of restricted types of games have also been proposed [START_REF] Eén | Sat-based strategy extraction in reachability games[END_REF], as well as a reduction of parity games to SAT [START_REF] Heljanko | Solving parity games by a reduction to SAT[END_REF]. As for partial information games, even less attempts have been made. To our knowledge, only alpaga [1] solves partial information games, but the explicit input format does not allow to solve real-life instances.

Motivated by a problem on swarms of mobile robots, we propose here an attempt to solve partial information games, when restricted to memoryless strategies.

Formal methods for the study of networks of robots The study of networks of mobile oblivious robots was pioneered by Suzuki and Yamashita [START_REF] Suzuki | Distributed anonymous mobile robots: Formation of geometric patterns[END_REF]. In their seminal work, robots are considered as points evolving obliviously in a 2D space (that is, robots cannot remember their past actions). Moreover, robots have no common chirality nor direction, and cannot explicitly communicate with each other. Moreover, robots are anonymous and execute the same algorithm to achieve their goal. Nevertheless, they embed visual sensors that enable sensing other robots positions.

Recently, the original model was extended to robots that move in a discrete space, modeled as a graph whose nodes represent possible robot locations, and edges denote the possibility for a robot to move from one location to another. The main problems that have been considered in the literature in this context are: gathering [START_REF] Kranakis | The Mobile Agent Rendezvous Problem in the Ring[END_REF], where all robots must gather on the same location (not determined beforehand) and stop moving, perpetual exploration [START_REF] Blin | Exclusive perpetual ring exploration without chirality[END_REF][START_REF] Angelo | A unified approach for different tasks on rings in robot-based computing systems[END_REF] where, robots must visit infinitely often a ring, and exploration with stop [START_REF] Flocchini | Computing without communicating: Ring exploration by asynchronous oblivious robots[END_REF], in that case, robots must visit each node of the ring and eventually stops.

Designing correct algorithms for mobile robots evolving on graphs is notoriously difficult. The scarcity of information that is available to the robots yields many possible symmetries, and asynchrony of the robot actions triggers moves that may be due to obsolete observations. As a matter of fact, published protocols for mobile robots on graphs were recently found incorrect, as reported in model checking attempts to assess them [START_REF] Bérard | Formal verification of mobile robot protocols[END_REF][START_REF] Doan | Model checking of a mobile robots perpetual exploration algorithm[END_REF][START_REF] Doan | Model checking of robot gathering[END_REF].

In addition to finding bugs in the literature [START_REF] Bérard | Formal verification of mobile robot protocols[END_REF], Model-Checking was used to check formally the correctness of published algorithms [START_REF] Bérard | Formal verification of mobile robot protocols[END_REF][START_REF] Devismes | Optimal grid exploration by asynchronous oblivious robots[END_REF][START_REF] Rubin | Verification of asynchronous mobile-robots in partially-known environments[END_REF]. However, the current models do not help in designing algorithms, only in assessing whether a tentative solution satisfies some properties. An approach based on Formal Proof has been introduced with the Pactole framework [START_REF] Auger | Certified impossibility results for byzantine-tolerant mobile robots[END_REF][START_REF] Courtieu | Impossibility of gathering, a certification[END_REF][START_REF] Courtieu | Certified universal gathering in \R ˆ2 for oblivious mobile robots[END_REF][START_REF] Balabonski | Synchronous gathering without multiplicity detection: A certified algorithm[END_REF][START_REF] Balabonski | A foundational framework for certified impossibility results with mobile robots on graphs[END_REF] using the Coq Proof assistant. Pactole enabled the certification of both positive [START_REF] Courtieu | Certified universal gathering in \R ˆ2 for oblivious mobile robots[END_REF][START_REF] Balabonski | Synchronous gathering without multiplicity detection: A certified algorithm[END_REF] and negative results [START_REF] Auger | Certified impossibility results for byzantine-tolerant mobile robots[END_REF][START_REF] Courtieu | Impossibility of gathering, a certification[END_REF] for oblivious mobile robots. The framework is modular enough that it permits to handle discrete spaces [START_REF] Balabonski | A foundational framework for certified impossibility results with mobile robots on graphs[END_REF]. The methodology enabled by Pactole forces the algorithm designer to write the algorithm along with its correctness proof, but still does not help her in the design process (aside from providing a binary assessment for the correctness of the provided proof).

By contrast, Automatic synthesis is a tempting option for relieving the mobile robot protocol designer. Indeed, Automatic synthesis aims to automatically produce algorithms that are correct by design, or, when no protocol can be synthesized, it inherently gives an impossibility proof. Automatic program synthesis for the problem of perpetual exclusive exploration in a discrete ring is due to Bonnet et al. [START_REF] Bonnet | Discovering and assessing fine-grained metrics in robot networks protocols[END_REF] (the approach is however restricted to the class of protocols that are unambiguous, where a single robot may move at any time). The approach was refined by Millet et al. [START_REF] Millet | On the synthesis of mobile robots algorithms: the case of ring gathering[END_REF] for the problem of gathering in a discrete ring network using synchronous semantics (robots actions are synchronized).

Contributions

In the current paper, we propose a SAT-based encoding of two-player partial information games, when restricted to memoryless strategies. We also prove that this problem is NP-complete. Then we apply this result to automatic synthesis of mobile robot protocols. We significantly extend the work of Millet et. al. [START_REF] Millet | On the synthesis of mobile robots algorithms: the case of ring gathering[END_REF] since we define and prove correct a general framework for automatic synthesis of mobile robot protocols, for any target problem, using the most general asynchronous semantics (i.e. no synchronization is assumed about robots actions). Our framework makes use of the results presented in the first part, since we need to look for memoryless strategies in a partial information game. Then, we use the SMT-solver Z 3 to synthesize strategies for the gathering problem in the remaining open cases [START_REF] Bonnet | Asynchronous gathering in rings with 4 robots[END_REF]. 42 Preliminaries Words An alphabet Σ is a finite set of symbols. A word on Σ is a (finite or infinite) sequence of symbols of Σ. For a word u, we let |u| be its length, i.e., its number of symbols (if u is an infinite word, |u| = ω). We denote respectively by Σ * and Σ ω the set of finite and infinite words on Σ. Moreover, we denote by Σ + the set of finite non-empty words on Σ. For a word u ∈ Σ ω , we denote by by Inf(u) the set of symbols of Σ occurring infinitely often in u.

Mathematical notations

Logic We recall the definition of propositional logic formulae. Given a countable set of variables X, it is described by the following grammar:

φ := x | φ ∧ φ | φ ∨ φ | ¬φ.
As usual, we can use φ 1 -→ φ 2 as a shorthand for ¬φ 1 ∨ φ 2 , and φ 1 ←→ φ 2 as a shorthand for φ 1 -→ φ 2 ∧ φ 2 -→ φ 1 . A literal is either a variable or the negation of a variable. A clause is a disjunction of literals. A formula is said to be in conjunctive normal form (CNF) if it is a conjunction of clauses. A valuation ν of the variables of X is a function ν : X → {0, 1}. From a valuation ν one can define an interpretation ν * of a formula φ as follows.

-

for x ∈ X, ν * (x) = ν(x); -ν * (φ 1 ∨ φ 2 ) = max(ν * (φ 1 ), ν * (φ 2 )); -ν * (φ 1 ∧ φ 2 ) = ν * (φ 1 ) × ν * (φ 2 ); -ν * (¬φ 1 ) = 1 -ν * (φ 1 ).
Often we note ν for ν * .

Preliminaries on games

We recall here few notations on 2-player game with partial information. A game on an arena is played by moving a token along a labeled transition system (the arena). Following previous work [START_REF] Doyen | Games with Imperfect Information: Theory and Algorithms[END_REF], the game is presented as follows. When the token is positioned on a state s of the arena, the player called the protagonist can chose the label a of one of its outgoing transitions. Then the opponent moves the token on a state s ′ such that (s, a, s ′ ) is a transition of the arena. The game continues in a turn-based fashion for infinitely many rounds. The winner is determined according to the winning condition, which depends on the sequence of states visited. In a game with partial information, the protagonist is not able to precisely observe the play to make a decision on where to move the token next. This is formalized by the notion of observation, which is a partition of the states of the arena in observation sets. Hence, the decision of the player is made solely according to the sequence of observations visited, and not the precise sequence of vertices.

Arena with partial information A game arena with partial information A = (S, Σ, δ, s 0 , Obs) is a graph where S is a finite set of states, Σ is a finite alphabet labeling the edges, and δ ⊆ S × Σ × S is a finite set of labeled transitions, and s 0 is the initial state. The arena is total in the sense that, for any s ∈ S, a ∈ Σ, there exists s ′ ∈ S such that (s, a, s ′ ) ∈ δ. The set Obs is a partition of S in observations visible to the protagonist. For s ∈ S, we let o(s) ∈ Obs be the corresponding observation. We extend o to the sequence of states in the natural way. An arena can be finite or infinite. In this work, we only consider finite arenas.

Plays A play π on the arena A = (S, Σ, δ, s 0 , Obs) is an infinite sequence π = s 0 s 1 • • • ∈ S ω such that for all 0 ≤ i, there exists a i ∈ Σ such that (s i , a i , s i+1 ) ∈ δ. The history of a play π is a finite prefix of π, noted π[i] = s 0 s 1 . . . s i , for i ≥ 0.

Strategies, consistent plays A strategy for a player is a function that determines the action to take according to what has been played. Formally, a strategy σ for the protagonist is given by σ : S + → Σ. As we explained, in an arena with partial information, the protagonist does not have a full knowledge of the current play. This is formalized by the notion of observation-based strategy. A strategy σ is observation-based if, for all π, π ′ ∈ S + such that o(π) = o(π ′ ), σ(π) = σ(π ′ ). A strategy for the opponent is given by τ : S + × Σ → S. Given two strategies for the players, σ and τ , we say that a play

π = s 0 s 1 • • • ∈ S ω is (σ, τ )-compatible if for all i ≥ 0, τ (π[i], σ(π[i])) = s i+1 , where π[i] = s 0 • • • s i .
We say that it is σ-compatible if there exists a strategy τ for the opponent such that π is (σ, τ )-compatible.

When σ depends only of the last visited state, σ is said to be a memoryless strategy. In that case, we may define σ simply as σ : S → Σ. We highlight the fact that σ is a total function.

Winning condition, winning strategy A winning condition on an arena A = (S, Σ, δ, s 0 , Obs) is a set φ ⊆ S ω . An observation-based strategy σ is winning for the protagonist in the game G = (S, Σ, δ, s 0 , Obs, φ) if any σ-compatible play π ⊆ φ (such a play is called a winning play). Observe that we do not require the strategy of the opponent to be observation-based.

When the observation set is the finest partition possible, i.e., for all s, s ′ ∈ S, if o(s) = o(s ′ ), then s = s ′ , the game is of total information, and any strategy for the protagonist is observation-based.

We are interested in the following classical winning conditions:

Reachability Given a subset F ⊆ S of target states, the reachability winning condition is defined by

REACH(F ) = {π = s 0 s 1 • • • ∈ S ω | s i ∈ F for some i ≥ 0}.
The winning plays are then the plays where one target set has been reached.

Büchi Given a subset F ⊆ S of target states, the Büchi winning condition is given by BUCHI

(F ) = {π = s 0 s 1 • • • ∈ S ω | Inf(π) ∩ F = ∅}.
The winning plays are then those where at least one target state has been visited infinitely often.

co-Büchi Given a subset F ⊆ S of target states, the co-Büchi winning condition is given by coBUCHI Observe that Büchi and co-Büchi winning conditions are special cases of parity winning conditions, and that a reachability game can be transformed into a Büchi (or a co-Büchi) game, hence into a parity game. Hence to establish general results on games it is enough to consider only parity games.

(F ) = {π = s 0 s 1 • • • ∈ S ω | Inf(π) ∩ F = ∅}.
The following result is a well-known result, called the memoryless determinacy of parity games of total information. Theorem 1 ( [START_REF] Emerson | Tree automata, mu-calculus and determinacy[END_REF]). In any parity game of total information, either the protagonist or the opponent has a winning strategy. Moreover, any player has a winning strategy if and only if it has a memoryless winning strategy.

This important result shows that it is then sufficient to consider only memoryless strategies to solve parity games.

However this does not hold true anymore when we consider the more general case of partial information games. The following result is also well-known [START_REF] Doyen | Games with Imperfect Information: Theory and Algorithms[END_REF].

Theorem 2. There exist parity games of incomplete information where there exists a winning strategy for the protagonist, but no memoryless winning strategy.

Parity games of partial information are then more difficult to solve, since their resolution implies a modification of the arena using a subset construction, hence an exponential blow-up [START_REF] Reif | The complexity of two-player games of incomplete information[END_REF].

From now on we explore resolution of games of partial information when one is only interested in memoryless strategies.

3 Resolution of partial information games, with memoryless strategies

Complexity results

In this subsection, we establish NP-completeness of the problem. In fact, we show that even for the simple case of reachability games, the problem is already NPhard. The detailed proof of the following theorem can be find in the Appendix.

Theorem 3. Deciding the existence of a memoryless strategy for partial observation game with reachability objective is NP-complete.

Proof (Sketch). We show the lower bound by a reduction from 3-SAT. Let ϕ = 1≤i≤k c i be a 3-SAT formula in conjunctive normal form over a set X of variables. We define a reachability game G ϕ = (S, Σ, δ, s 0 , Obs, φ). The set of states of the arena will include a state for each clause, and a state for each variable and negation of variable. Formally,

S = {s 0 } ∪ {s ci | 1 ≤ i ≤ k} ∪ {s x , s ¬x | x ∈ X} ∪ {s ⊤ , s ⊥ }.
The game is supposed to go as follows. The opponent selects a clause that the protagonist must show valued to 1. To do so, the protagonist goes to a state s ℓ with ℓ a literal (x or ¬x) appearing in the selected clause, which is supposed to be true. According to its actual valuation, the game goes to the winning state s ⊤ or to the losing state s ⊥ . We assume that for all 1

≤ i ≤ k, c i = ℓ i,1 ∨ ℓ i,2 ∨ ℓ i,3 , with ℓ i,j ∈ {x, ¬x | x ∈ X}. We define Σ = {0, 1, 2, 3} and δ = {(s 0 , 0, s ci ) | 1 ≤ i ≤ k} ∪ {(s ci , j, s ℓi,j ) | 1 ≤ j ≤ 3} ∪ {(s x , 1, s ⊤ ), (s x , 0, s ⊥ ), (s ¬x , 0, s ⊤ ), (s ¬x , 1, s ⊤ ) | x ∈ X} ∪ {(s ⊤ , 0, s ⊤ ), (s ⊥ , 0, s ⊥ )}.
Observe that non-determinism, hence choice of the opponent, appears only in the transitions from the initial state s 0 . The opponent only choses the clause to prove to be true. The rest of the game is totally determined by the strategy of the protagonist. Finally, we define the observations. Each state has its own observation class, except for the literals: for all

x ∈ X, o(s x ) = o(s ¬x ) = {s x , s ¬x }. For all state s ∈ X \ {s x , s ¬x | x ∈ X}, o(s) = {s}. The objective of the game is φ = REACH({s ⊤ }).
Then the formula ϕ is satisfiable if and only if there is a memoryless observation-based strategy for the game G ϕ .

The upper bound follows from the fact that once a memoryless strategy has been guessed, one can check its correctness by inspecting the arena reduced to the only transitions chosen by the strategy in polynomial time (by checking absence of a loosing cycle).

The problem is then NP-complete.

⊓ ⊔

Since any reachability game can be reduced to a parity game, the following result can be obtained.

Corollary 4. Deciding the existence of a memoryless strategy for partial observation game with reachability objective is NP-complete.

Encoding a partial information game as a SAT problem

In this section, we show how to encode G = (S, Σ, δ, s 0 , Obs, φ) a partial information game in a propositional logic formula. Here, the winning condition φ can be either a reachability, a Büchi or a co-Büchi condition for a target set of states F ⊆ S. We give the proof for reachability games, but slight modifications of the constraint (4) allow to handle Büchi and co-Büchi conditions.

We encode the arena of the game by attributing a variable to each transition. Let X = { s 1 , a, s 2 | (s 1 , a, s 2 ) ∈ δ} be the corresponding set of variables. Valuation of a variable to 1 will mean that the corresponding transition is selected by the strategy. Now we need to express the different constraints that characterize a strategy. First, the strategy chooses a label of a transition, not the destination state. Moreover, the decision of a player is made only according to observation, and cannot depend specifically on one state.

s1,a,s2 , s ′ 1 ,a,s ′ 2 ∈X s.t. o(s1)=o(s ′ 1 ) ( s 1 , a, s 2 ←→ s ′ 1 , a, s ′ 2 ) (1)
Then, at each state, the strategy will choose a unique action:

s1,a,s2 ∈X s 1 , a, s 2 -→ s1,b,s ′ 2 ∈X , b∈Σ\{a} ¬ s 1 , b, s ′ 2 ∧ ¬ s 1 , a, s 2 -→ s1,b,s ′ 2 ∈X , b∈Σ\{a} s 1 , b, s ′ 2 (2)
A valuation of these variables satisfying these constraints would hence describe a memoryless observation-based strategy. Now we add constraints to check that this strategy is winning.

To do so, we need to check that any play compatible with this strategy is winning. We then add boolean variables that will encode prefixes of plays compatible with the strategy, i.e. paths in the graph of the arena, when restricted to edges selected by the strategy. In the following we refer to this graph as the restricted arena.

-P = { s, s ′ | (s, s ′ ) ∈ S 2 }.
A variable s, s ′ ∈ P encodes the existence of a path starting at s and ending with s ′ .

-W = { s, s ′ | (s, s ′ ) ∈ S 2 }.
A variable s, s ′ ∈ W encode the fact that all paths starting at s and ending with s ′ visit a state from F (different from s).

Thus, the constraints characterizing valid prefixes are: i) s1,a,s2 ∈X , s1,s2 ∈P ( s 1 , a, s 2 -→ s 1 , s 2 ). If the strategy allows a transition (s 1 , a, s 2 ) ∈ δ, then s 1 , s 2 is a path in the restricted arena.

ii)

s1,s2 ∈P, s2,a,s3 ∈X (( s 1 , s 2 ∧ s 2 , a, s 3 ) -→ s 1 , s 3 ). A prefix s 1 , s 2 is extended to s 1 , s 3 if the strategy allows the transition (s 2 , a, s 3 ) ∈ δ.

iii) s1,a,s2 ∈X ,s2 / ∈F ( s 1 , a, s 2 -→ ¬ s 1 , s 2 ). If the strategy allows a transition (s 1 , a, s 2 ) ∈ δ where s 2 is not a target state then there is a path from s 1 to s 2 that does not visit any state from F . iv)

s1,s2 ∈W,s2 / ∈F ( s 1 , s 2 -→ s3,b,s2 ∈X , s1,s3 ∈W,s3 =s2 (¬ s 3 , b, s 2 ∨ s 1 , s 3 )).
If all the paths from s 1 to s 2 visit a state from F (different from s 1 , while s 2 is not a target state, then it means that for every predecessor s 3 of s 2 , all paths from s 1 to s 3 already visit a state from F .

The formula resulting of the conjunction of the previous constraints is noted [START_REF] Balabonski | Synchronous gathering without multiplicity detection: A certified algorithm[END_REF].

It remains to show that the strategy is indeed winning, i.e., in the arena restricted to transitions allowed by the strategy, all the plays are winning. If this is not the case, then there exists a (infinite) play that never visits any set of F . Since the arena is finite, such a play necessarily contains a loop that does not visit a target state. The constraint expressing that the strategy is not winning is then: s 0 , s ∧¬ s 0 , s ∧ s, s ∧¬ s, s . So, to express that the strategy is winning, we just have to negate this formula and quantify over all variables of P and W. We obtain: s0,s , s,s ∈P, s0,s , s,s ∈W

(¬ s 0 , s ∨ s 0 , s ∨ ¬ s, s ∨ s, s ) (4)
The final formula encoding existence of a winning strategy is then the conjunction of all previous formulae:

ψ G = (1) ∧ (2) ∧ (3) ∧ (4) (5)
The detailed proof of the following theorem can be find in the Appendix.

Theorem 5. G = (S, Σ, δ, s 0 , Obs, REACH(F )) admits a memoryless winning strategy if and only if ψ G is satisfiable.

Proof (Sketch). Given a strategy σ on G, we define A σ = (S, Σ, δ σ , s 0 , Obs), where δ σ = {(s, a, s ′ ) ∈ δ | σ(s) = a} as the game arena restricted to the transitions allowed by the strategy σ.

Assume first that G admits a winning memoryless and observation-based strategy σ : S → Σ. Then ψ G is satisfied by the valuation ν σ : (X ∪ P ∪ W) → {0, 1}, defined as follows:

-for all s, a, s ′ ∈ X , ν σ ( s, a, s ′ ) = 1 if σ(s) = a. 0 otherwise.
for all s, s ′ ∈ P, ν σ ( s, s ′ ) = 1 if there is play of A σ with a prefix s . . . s ′ . 0 otherwise.

-for all s, s ′ ∈ W, ν σ ( s, s ′ ) =         
1 if there is play of A σ with a prefix s . . . s ′ and all prefixes starting at s and ending with s ′ visit a state from F different from s. 0 otherwise.

It is then straightforward to check that ν σ (ψ G ) = 1. Assume now that ψ G is satisfiable and let ν : X ∪ P ∪ W → {0, 1} such that ν(ψ G ) = 1. We build a strategy σ ν : S → Σ as follows. For s ∈ S, let a ∈ Σ and s ′ ∈ S such that ν( s, a, s

′ ) = 1 then σ ν (s) = a. Condition (2) ensures that σ ν is well-defined. Moreover, if s 1 , s ′ 1 ∈ S are such that o(s 1 ) = o(s ′ 1 ), then condition (1) ensures that, for all a ∈ Σ, ν( s 1 , a, s 2 ) = ν( s ′ 1 , a, s ′ 2 ). Hence σ ν (s 1 ) = σ ν (s ′ 1
) and σ ν is observation-based. To prove that σ ν is winning, we rely on the following observation: in a game G = (S, Σ, δ, s 0 , Obs, REACH(F )), if a strategy σ is not winning, then there exists a σ-compatible play s 0 • • • s • π ω , with π = s 1 • • • s k for some k ∈ N, and that play never visits a state from F . We can then prove that it is impossible to have such a play in A σ .

⊓ ⊔

4 Application: automatic synthesis of strategies for swarms of autonomous oblivious robots

In this section, we consider applying our methodology to formally study distributed algorithms that are designed for sets of mobile oblivious robots. Robots are mobile entities that evolve in a discrete space (here, a ring), When two robots are positioned on the same node, they form a tower. In this model, robots cannot remember their past actions (they are oblivious), have no common chirality nor direction, and cannot explicitly communicate with one another. However, they can sense their entire environment (using visual sensors). Moreover, robots are anonymous and execute the same deterministic algorithm to achieve their goal. Each robot evolves following an internal cycle: it takes a snapshot of the ring, computes its next move, and then executes the movement it has computed. Several semantics for swarms of robots have been studied. In the fully synchronous semantics (FSYNC), all the robots evolve at the same time, completing an internal cycle simultaneously. In the semi-synchronous semantics (SSYNC), in each round, only a non-empty subset of the robots fulfills a complete cycle. Finally, in the asynchronous semantics (ASYNC), each robot completes its internal cycle at its own pace. The later semantics are considered the harder to design robot algorithms, since a robot may move based on obsolete observations.

In this section, we extend the work done by Millet et al. [START_REF] Millet | On the synthesis of mobile robots algorithms: the case of ring gathering[END_REF], where automatic synthesis of protocols of gathering in FSYNC and SSYNC semantics was considered. In the current paper, we first provide a general framework for automatic synthesis of mobile robot protocols, for any target problem, using the most general ASYNC semantics. Then, we use our propositional logic-based encoding to effectively solve the problem.

Model for the robots

We partly use notations defined in [START_REF] Sangnier | Parameterized verification of algorithms for oblivious robots on a ring[END_REF]. We consider a fixed number of k > 0 robots evolving on a ring of fixed size n ≥ k. We denote by R the set of considered robots. Positions on the ring of size n are numbered {0, . . . , n -1}.

Configurations and robots views. A configuration is a vector c ∈ [0, n -1] k that gives the position of each robot on the ring at a given instance of time. We assume that positions are numbered in the clockwise direction. The set of all configurations is called C n,k , or simply C when n and k are clear from the context.

Decisions made by a robot are based on the snapshot it takes of the environment, called the view of that robot. We model it by the sequence of distances between neighboring robots on the ring, a distance of 0 means that the two consecutive robots share the same position on the ring. Formally, a view is then a tuple

V = d 1 , . . . , d k such that Σ n i=0 d i = n.
The set of all the views on a ring of size n with k robots is noted V. Notice that two robots sharing the same position should have the same view. This might be problematic with our definition since when two robots share the same node, their distance is equal to 0, and this 0 is not at the same position in the tuple according to the concerned robot in the tower. To ensure this, we assume that the first distance in the tuple is always strictly greater than 0 (which is always possible by putting the first 0's at the end instead). In Figure 1 is shown a configuration defined by c(r 1 ) = c(r 2 ) = 0, c(r 3 ) = 3, c(r 4 ) = 7 and c(r 5 ) = 8. When looking in the clockwise direction, the view of robots r 1 and r 2 is given by the tuple V = 3, 4, 1, 2, 0 , and the view of robot r 3 is given by V ′ = 4, 1, 2, 0, 3 . Formally, for a view V = d 1 , . . . , d k giving the view of a robot starting in one direction, we write its view in the opposite direction ← -V = d j , . . . , d 1 , d k , . . . , d j-1 , where 1 ≤ j ≤ k is the greatest index such that d j = 0. In our example, it means that ← -V = 2, 1, 4, 3, 0 and ← -

V ′ = 3, 0, 2, 1, 4 .
Given a configuration c ∈ C and a robot i ∈ R, the view of robot i when looking in the clockwise direction, is given by V

c [i →] = d i (i 1 ), d i (i 2 )-d i (i 1 ), . . . , n- d i (i k-1 ) , where, for all j = i, d i (j) ∈ [1, n] is such that (c(i) + d i (j)) mod n = c(j) and i 1 , . . . , i k are indexes pairwise distinct such that 0 < d i (i 1 ) ≤ d i (i 2 ) ≤ • • • ≤ d i (i k-1 ). When robot i looks in the opposite direction, its view accord- ing to the configuration c is V c [← i] = ← ----- V c [i →]. Hence, in the configuration c pictured in Figure 1, V c [r 1 →] = 3, 4, 1, 2, 0 and V c [← r 1 ] = 2, 1, 4, 3, 0 . Observe that in Figure 2, V c ′ [r 1 →] = V c ′ [← r 1 ] = 3, 1, 3 .
Robot r 1 is then said to be disoriented, since it has no way to distinguish one direction from the other. For a configuration c, we let Views(c) = i∈R {V c [i →], V c [← i]} be the set of views of all the robots in this configuration.

Since robots are anonymous, given a configuration c, the set of decisions taken by the robots based on their view in this configuration is invariant with respect to permutation of the robots or to any rotation of the ring. Since they have no chirality, a robot i ∈ R takes a decision solely based on V c [i →], V c [← i] , hence the same decision is reached for any configuration symmetric to c. Regarding decision taking, any two configurations that are obtained through symmetry or any rotation of the ring are equivalent. The notion of views captures handily this notion and we define the equivalence relation on configurations as follows. We now make some observations on the relations between configurations and views of the robots.

Let V ∈ V. We note

Config(V) = {c ∈ C | V ∈ Views(c)}. Lemma 7. Let V ∈ V, and c, c ′ ∈ Config(V). Then p ≡ p ′ .
We distinguish now some set of configurations that are useful in the remaining of the paper. Let C T = [c] where c(i) = 0 for all i ∈ R be the set of all the configurations where all the robots are gathered on the same position. For i ∈ R and j ∈ [0, n -1], let C j i = {c ∈ C | c(i) = j)} be the set of configurations where the robot i is on the position j of the ring, and we let C j = i∈R C j i be the set of configurations where there is one robot on position j of the ring.

The proof of Lemma 7 is immediate once we have made the following remark.

Remark 8. Let V = d 1 , . . . , d k ∈ V. We define rot(V ) = { d ′ 1 , . . . , d ′ k | ∃1 ≤ i ≤ k, such that for all 1 ≤ ℓ ≤ k -i + 1, d ′ ℓ = d i-ℓ+1 and for all k -i + 1 < ℓ ≤ k, d ′ ℓ = d i+ℓ-1-k
} the set of rotations of the tuple representing the view V. Then, it is easy to observe that for a configuration c ∈ Config(V),

Views(c) = { d 1 , . . . , d k ∈ V | d 1 , . . . , d k ∈ rot(V) ∪ rot( ← - V) with d 1 > 0}.
Protocols for the robots. We are interested in modeling distributed protocols that govern the movements of the robots in a ring in order to achieve some predefined goal. Such protocols control each robot according to its local view. Robots being anonymous imply that two robots having the same view of the ring execute the same order. Having no common chirality implies that the protocol does not discriminate between the clockwise and the anti-clockwise view, hence gives symmetric move orders to robots in symmetric positions, and cannot decide where to move when the robot is disoriented, i.e. when both views are identical. We denote by ∆ = {-1, 0, 1, ?} the set of possible decisions given by the protocol, where 0 means that the robot won't move, -1 means an anticlockwise movement, 1 a clockwise movement and ? means that the robot moves but is disoriented, hence it has no control on the exact direction to take.

We review here some basic notations. For a function f : A → B, we let dom(f ) = A its domain of definition, and for a subset C ⊆ A, we let f |C : C → B the restriction of f on C, defined by f |C (c) = f (c) for all c ∈ C. We can now define the notion of decision function. Definition 9. Let D : V → ∆ be a (partially defined) function. We say that D is a decision function if, for all V ∈ dom(D), (i)

← - V ∈ dom(V ), (ii) if V = ← - V, then D(V) ∈ {0, ?}, (iii) otherwise, D(V) ∈ {-1, 0, 1} and D(V) = (-1) • D( ← - V).
We denote by D the set of all decision functions.

A protocol P for k robots on a ring of size n is simply a total decision function.

Executions. Recall that each robot behaves according to an internal cycle, alternating between a phase where it looks at its environment and computes its next move, and a phase where it actually moves. We model here the asynchronous semantics, where other robots can execute an unbounded number of actions between the two aforementioned phases.

Hence, to define the transition relation between two configurations, we need to enrich the notion of configuration with that of internal state of each robot, which determines the next action of a robot. The set of all possible internal states for the robots is S = {-1, 0, 1, L}, where -1 represents a move in the anti-clockwise direction, 0 not moving, 1 represents a move in the clockwise direction, and L represents the fact that the robot is ready to take a snapshot of its environment.

Let s ∈ S k be the vector of internal states of the robots. An asynchronous configuration is an element (c, s) ∈ C × S k . We say that (c, s) → P (c ′ , s ′ ) if and only if there exists a robot i ∈ R such that:

-s ′ (j) = s(j) and c ′ (j) = c(j) for all j = i,

-if s(i) = L then c ′ (i) = c(i) and s ′ (i) ∈ {-1, 1} if P(V c [i →]) =?, and s ′ (i) = P(V c [i →]) otherwise. If s(i) = L then s ′ (i) = L and c ′ (i) = (c(i) + s(i)) mod n.
Observe that given two asynchronous configurations (c, s) and (c ′ , s ′ ), two protocols P and P ′ such that P |Views(c) = P ′ |Views(c) , then (c, s) → P (c ′ , s ′ ) if and only if (c, s) → P ′ (c ′ , s ′ ).

Protocols for robots are meant to work starting from any initial configuration, or at least from a subset of possible initial configurations. The only requirement is that internal states of robots are set to L at the beginning of the execution. Hence, an initial asynchronous P-run is a (finite or infinite) sequence ρ = (c 0 , s 0 )(c 1 , s 1 ) . . . such that: (1) s 0 (i) = L for all robot i ∈ R, and (2) for all 0

≤ k < |ρ|, (c k , s k ) → P (c k+1 , s k+1 ). For a robot i ∈ R, we let Act i (ρ) = |{0 ≤ k < |ρ| | s k (i) = L
and s k+1 (i) = L}| the number of times this robot has been moved during the execution. A P-run is fair if, for all i ∈ R, Act i (ρ) = ω.

For a P-run ρ, the projection of on the sequence of configurations is written π C (ρ).

We can now define the synthesis problem under consideration in this work, where we are given an objective for the robots, describing the set of desirable runs.

Definition 10 (Synthesis problem). Given an objective Ω ⊆ C ω , decide wether there exists an protocol P such that for all initial fair asynchronous P-run ρ, π C (ρ) ⊆ Ω.

Objectives. Classical objectives for the robots are gathering, perpetual exploration and exploration with stop. Formally, we call GATHER the synthesis problem where

Ω = {c 1 • • • c k • c ω k | for some k ≥ 1, c k ∈ C T }, we call EXPLORATION the synthesis problem where Ω = {π ∈ C ω | Inf(π) ∩ C j i = ∅ for all i ∈ R and j ∈ [0, n -1]} and EXPLORATION-STOP the synthesis prob- lem where Ω = {c 1 . . . c k • c ω k | c k ∈ C T , and for all j ∈ [0, n -1], there exists 1 ≤ ℓ ≤ k, c ℓ ∈ C j }.

Definition of the arena

We define now a partial information game G n,k = (S n,k , Σ n,k , δ n,k , s 0 , Obs n,k , φ) that captures the asynchronous model for a set R of k robots evolving on a ring of size n. The protocol of the robots gives, according to the last view of the robot, the next move to do, taken from the set ∆ = {-1, 0, 1, ?}. The states of the arena are the possible distinct asynchronous configurations, enriched with a vector of bits b ∈ {0, 1} k that keeps track of the various activated robots to ensure the fairness of the execution. We write B = {0, 1} k . Moreover, the initial configuration of the execution is chosen by the opponent. To ensure this, we add a special initial state, s ι , that can access any possible initial configuration.

Hence the set of states S n,k = (C × S k × B) ⊎ {ι}. Choosing a transition for the protocol means choosing a decision function for the possible views of the robots in a particular configuration c. The labeling of the transitions is hence taken from Σ n,k = D ⊎ {ε}, the set of all possible decision functions, along with a dummy label, ε, used only for the initial state. The protocol we look for is supposed to achieve the goal starting in any initial configuration. The transitions starting from the initial state of the arena (which is the special state ι) are all labelled by the same dummy action, and lead to any initial configuration. Formally, {(ι, ε, (c, s L , 0 )) | c ∈ C} ⊆ δ n,k with s L (i) = L for all i ∈ R, b 0 (i) = 0 for all i ∈ R. Now, in any configuration, the protagonist choses the decision function corresponding to the decisions of the robots in this particular configuration, and the opponent chooses the resulting configuration. The opponent then decides which robot moves (the role of the scheduler), and, whenever a robot is disoriented where it actually moves. Formally, let (c, s, b) ∈ S n,k be a state of the arena, and f : Views(c) → ∆ be a decision function. Let also f : V → ∆ be any protocol such that

f |Views(c) = f . Then, ((c, s, b), f, (c ′ , s ′ , b ′ )) ∈ δ n,k iff (c, s) → f (c ′ , s ′ ) and b ′ is defined as follows: let b ′′ ∈ B, such that b ′′ (i) = b(i) if s(i) = s ′ (i), i.e.
if the robot i has not been scheduled, and

b ′′ (i) = 1 if s(i) = L and s ′ (i) = L b(i) otherwise.
Then, b ′ is defined as follows. If b ′′ (i) = 1 for all i ∈ R, then b ′ (i) = 0 for all i ∈ R, otherwise b ′ = b ′′ . Hence, the bit b(i) is turned to 1 every time robot i has been scheduled to move. Once they all have been scheduled to move once, every bit is set to 1, and the entire vector is reset to 0. Finally we define the observation sets. Indeed, when the protocol is defined, it only takes into account the view of a robot, and it does not depend on the internal states of other robots, nor on the scheduling. Hence the strategy computed for the protagonist should only depend on the configuration. Moreover, as we have explained earlier, decisions of the robots are invariant to permutation of the robots, rotation of the ring or any symmetry transformation. The strategy then only depends on the equivalence class of the configuration. Given a set R of k robots evolving on a ring of size n, let φ ⊆ S ω n,k . Then, A n,k = (S n,k , Σ n,k , δ n,k , s 0 , Obs n,k ) is the corresponding arena with partial information and G n,k = (S n,k , Σ n,k , δ n,k , s 0 , Obs n,k , φ) is the two-player game with winning condition φ.

Proposition 11. For each synthesis problem GATHER, EXPLORATION and EXPLORATION-STOP, there exists a protocol for the robots if and only if there exists a memoryless winning strategy in a partial information game, with parity condition (more precisely a combination of reachability, Büchi and co-Büchi condition). Definition 12. Let A n,k be an arena as described above, and P a protocol for the robots. A play s 0 (c 0 , s 0 , b 0 )(c 1 , s 1 , b 1 ) . . . in A n,k is equivalent to the initial asynchronous run (c 0 , s 0 )(c 1 , s 1 ) . . . . Moreover, observe that for any initial run (c 0 , s 0 )(c 1 , s 1 ) . . . , there exists a unique play s 0 (c 0 , s 0 , b 0 )(c 1 , s 1 , b 1 ) . . . in G n,k that is equivalent, since the sequence of b i is entirely determined by the sequence of c i and s i . In the following, we have two lemmas which prove the equivalence. Lemma 13. Let σ : S n,k → Σ n,k be an observation-based memoryless strategy on G n,k . Then there exists a protocol P σ : V → ∆ such that any σ-compatible play is equivalent to an initial P-run, and any initial P-run is equivalent to a σ-compatible play.

Proof (Proof of Lemma 13). Let V ∈ V, and c ∈ Config(V), s ∈ S k and b ∈ B. We let P σ (V) = σ(c, s, b)(V). The protocol is then uniquely defined, because by Lemma 7, any c

′ ∈ Config(V) is in [c], and because σ is observation-based. Let s 0 (c 0 , s 0 , b 0 )(c 1 , s 1 , b 1 ) . . . be a σ-compatible play. Let i ≥ 0. Since it is a σ-compatible play, (c i , s i , b i ), P σ |Views(c i ) , (c i+1 , s i+1 , b i+1 )) ∈ δ, with σ(c i , s i , b i ) = P σ |Views(c i ) . Hence, (c i , s i ) → P σ (c i+1 , s i+1 ), and (c 0 , s 0 )(c 1 , s 1 ) • • • is an initial P σ -run.
Conversely, let (c 0 , s 0 )(c 1 , s 1 ) • • • be an initial P σ -run. Then the unique equivalent play s 0 (c 0 , s 0 , b 0 )(c 1 , s 1 , b 1 ) . . . is a σ-play. Indeed, let i ≥ 0, then σ(c i , s i , b i ) = P σ |Views(c i ) by construction, and since (c i , s i )

→ P σ (c i+1 , s i+1 ), ((c i , s i , b i ), P σ |Views(c i ) , (c i+1 , s i+1 , b i+1 )) ∈ δ. Hence s 0 (c 0 , s 0 , b 0 )(c 1 , s 1 , b 1 ) . . . is a σ-compatible play.
⊓ ⊔ Lemma 14. Let P : V → ∆ be a protocol for k robots on a ring of size n.

Then there exists an observation-based memoryless strategy σ : S n,k → Σ n,k such that any initial P-run is equivalent to a σ-compatible play of G n,k and any σ-compatible play is equivalent to an initial P-run.

Proof (Proof of Lemma 14). We build a memoryless strategy Let (c 0 , s 0 )(c 1 , s 1 ) . . . be an initial P-run and consider the unique equivalent play s 0 (c 0 , s 0 , b 0 )(c 1 , s 1 , b 1 ) . . . . Then, for all i ≥ 0, (c i ,

s i ) → P (c i+1 , s i+1 ) hence ((c i , s i , b i ), P Views(c i ) , (c i+1 , s i+1 , b i+1 )) ∈ δ and this is indeed a play in G n,k . Moreover, by definition of σ P it is a σ P -play. Conversely, let s 0 (c 0 , s 0 , b 0 )(c 1 , s 1 , b 1 ) . . . be a σ P -play. It is immediate that (c 0 , s 0 )(c 1 , s 1 ) . . . is an initial P-run. ⊓ ⊔
To conclude on the equivalence between solving the game for the robots and the synthesis problem defined in Section 4.1, it remains to state the following lemma. Proof (Proof of Proposition 11). In order to solve GATHER, we need to slightly modify the arena of G n,k . Indeed, if the objective of the gathering resembles a reachability objective, it is also required that once robots are gathered, they do not leave their positions anymore, while in a reachability game, the play is won as soon as the objective is attained no matter what happens afterwards. In order to circumvent this problem, we modify G n,k as follows. For all (c, s, b)

∈ S n,k such that c ∈ C T , for all (c ′ , s ′ , b ′ ) ∈ S n,k , ((c, s, b), f, (c ′ , s ′ , b ′ )) ∈ δ if and only if f (V) = 0 for all V ∈ Views(c).
The rest of the arena remains unchanged. We call this new game G ′ n,k . Hence, this modification restricts the possibilities to decision functions that detect that a configuration where all the robots are gathered is reached, and commands not to move anymore. This does not change anything for Lemma 13, and it is easy to see that Lemma 14 could be adapted to the special protocols that command not to move while all the robots are gathered. We then let T = {(c, s, b) | c ∈ C T and s(i) ∈ {L, 0} for all i ∈ R}. In the modified arena, any play π = s 0

• (c 0 , s 0 , b 0 )(c 1 , s 1 , b 1 ) • • • ∈ REACH(T ) is such that there exists k ≥ 0, such that for all ℓ ≥ k, (c ℓ , s ℓ , b ℓ ) ∈ T . In- deed, let k ≥ 0, such that (c k , s k , b k ) ∈ F . Since we consider the modified arena, ((c k , s k , b k ), f, (c k+1 , s k+1 , b k+1 )) ∈ δ implies that f (V) = 0 for all V ∈
Views(c k ). Hence, by definition, there exists i ∈ R such that s k (i) = s k+1 (i). If s k (i) = L then s k+1 = 0 by definition of f and c k+1 = c k ; if s k (i) = 0 then c k+1 = c k and s k+1 = L. Then, (c k+1 , s k+1 , b k+1 ) ∈ T . We also need to consider unfair executions that should not be considered as loosing if they fail to reach T . Let F = {(c, s, b) | b(i) = 0 for all i ∈ R}, the set of configurations where the vector b has been reset to 0.

There exists a protocol solving GATHER if and only if there exists a memoryless observation-based strategy for the protagonist in G ′ n,k (REACH(T ) ∪ coBUCHI(F )). Assume that there is a winning strategy σ in that game, and consider P the protocol as in Lemma 13. We show that P is winning for GATHER. We recall the objective of this problem,

Ω GATHER = {c 0 c 1 • • • c ω k | c k ∈ C T }.
Let ρ be a fair P-run and let π be its unique equivalent play. By Lemma 13, π is a σ-play. Since it is a winning strategy, π ∈ REACH(T ) ∪ coBUCHI(F ). By Lemma 15, since ρ is fair, Inf(π) ∩ {(c, s, b) | b(i) = 0 for all i ∈ R} = ∅ and π / ∈ coBUCHI(F ). Hence π ∈ REACH(T ) and π C (ρ) ∈ Ω GATHER . Reciprocally, assume that there is a protocol P solving GATHER and consider the memoryless observation-based strategy σ of Lemma 14. Let π be a σ-play and ρ be its equivalent run. By Lemma 14, ρ is a P-run. If ρ is fair, then π C (ρ) ∈ Ω GATHER and by construction π ∈ REACH(T ). Otherwise, by Lemma 15, Inf(π) ∩ {(c, s, b) | b(i) = 0 for all i ∈ R} = ∅ and π ∈ coBUCHI(F ).

⊓ ⊔

With the general parity condition, one can also use G n,k (with slight suitable modifications) in order to solve EXPLORATION and EXPLORATION-STOP.

This encoding is then a generalization of the work presented in [START_REF] Millet | On the synthesis of mobile robots algorithms: the case of ring gathering[END_REF], where the encoding allowed only for the gathering problem in synchronous or semisynchronous semantics.

This generalization is at the cost of an increasing of the size of the arena, as well as lifting the problem to parity games with partial information, hence making the problem more complex to solve, as we have seen earlier (NP-complete instead of linear time in the case of reachability games of total information studied in [START_REF] Millet | On the synthesis of mobile robots algorithms: the case of ring gathering[END_REF]). Results of Section 3.2 would allow us to solve this problem using a SAT-solver.

Conclusion

We studied the implementation of partial information zero-sum games with memoryless strategies. We proved that this problem is NP-complete. Moreover, we provided its SAT-based encoding using the recent advances in the state-of-the-art of SAT-solvers.

Furthermore, we used this framework to offer a solution to automatic synthesis of protocols for autonomous networks of mobile robots in the most generic settings (i.e. asynchronous). The arena obtained from our encoding suffers from an important exponential blow-up and the size of the generated formula is significantly large to be considered as input for a SAT-solver. To circumvent this problem, we used the Presburger subset formalism of first-order to encode the arena in a more abstract way. Indeed, the transition relation of the arena for the robots is encoded as a predicate in Presburger logic and we use uninterpreted functions of SMT to define predicates corresponding to the paths. Finally, the memoryless strategy is encoded as an uninterpreted function whose value is what the solver should find. It is worth noting that the theory we used is decidable, since all the variables range over finite domains. We used the SMT solver Z3 to experiment the synthesis problem GATHER, for 4 robots on a ring of size 5, 7 and 9. In each case, the solver answered that there was no protocol able to solve this problem, confirming handmade [START_REF] Stefano | About ungatherability of oblivious and asynchronous robots on anonymous rings[END_REF]. The files containing the formulae in the SMT-lib formalism are available on this webpage [19]. We currently work on covering, using our encoding, cases (e.g. rings of greater size) for the SP 4 [START_REF] Stefano | About ungatherability of oblivious and asynchronous robots on anonymous rings[END_REF] open problem.

For

  a, b ∈ Z such that a ≤ b, we denote by [a, b] the set {c ∈ Z | a ≤ c ≤ b}. We denote by mod the modulo function defined by a mod b = d, for a, b ∈ Z, where d ∈ [0, b -1] such that there exists j ∈ Z and a = b.j + d.

  The winning plays are then those where no target state has been visited infinitely often.Parity The parity winning condition requires the use of a coloring function d : S → [0, n] where [0, n] is a set of colors. The parity winning condition is given by Parity(d) = {π | min{d(s) | s ∈ inf(π)} is even}. The winning plays are then those where the minimal color occurring infinitely often is even.

Fig. 2 .Fig. 3 .

 23 Fig. 1. A configuration c with a tower

Definition 6 (

 6 Equivalence relation on configurations). Two configurations c and c ′ ∈ C are equivalent if and only if Views(c) = Views(c ′ ). We write then c ≡ c ′ . The equivalence class of c with respect to ≡ is simply written [c].

  Formally we let Obs n,k = {[c] | c ∈ C} and for any state (c, s, b) ∈ S n,k , o(c, s, b) = [c].

  σ P : S n,k → Σ n,k as follows. Let (c, s, b) ∈ S n,k , then σ P (c, s, b) = P |Views(c) . Consider (c ′ , s ′ , b ′ ) such that o(c, s, b) = o(c ′ , s ′ , b ′ ). Then c ≡ c ′ and by definition, Views(c) = Views(c ′ ). Hence σ P (c, s, b)=σ P (c ′ , s ′ , b ′ ) and the strategy is indeed observation-based.

Lemma 15 .

 15 Given ρ a run and π an equivalent play in the game, ρ is fair if and only if Inf(π) ∩ {(c, s, b) | b(i) = 0 for all i ∈ R} = ∅.

Note for the reviewers: due to space constraints, the complete proofs are given in as additional material in a separate file.

A Details of the proof of Theorem 3

Then the formula ϕ is satisfiable if and only if there is a memoryless observationbased strategy for the game G ϕ . Suppose that the formula ϕ is satisfiable and let ν : X → {0, 1} the valuation of the variables such that ν(ϕ) = 1. We define the memoryless observation-based strategy σ : S → {0, 1, 2, 3} as follows: σ(s 0 ) = 0, for all x ∈ X, σ(s x ) = σ(s ¬x ) = ν(x) and for all 1 ≤ i ≤ k, σ(s ci ) = j such that ν(ℓ i,j ) = 1 (such a literal always exists since ν(ϕ) = 1). The strategy is obviously memoryless and observation-based. Consider a σ-compatible play π = s 0 s 1 s 2 s 3 • • • . By construction, s 1 = s ci for some 1 ≤ i ≤ k, and let 1 ≤ j ≤ 3 such that σ(s ci ) = j. Then s 2 = s ℓi,j . By construction, ν(ℓ i,j ) = 1. If ℓ i,j = x then ν(x) = 1 and σ(s ℓi,j ) = 1, if ℓ i,j = ¬x, then ν(x) = 0 and σ(s ℓi,j ) = 0. In both cases, s 3 = s ⊤ by construction of the arena. Hence π is a winning play and σ is a winning strategy.

Conversely, let σ be a memoryless observation-based winning strategy for φ. We define a valuation of the variables ν(x) = σ(s x ) for all x ∈ X. Let 1 ≤ i ≤ k and let's show that ν(c i ) = 1. Let σ(s ci ) = j. Hence, and since σ is winning, s 0 s ci s ℓi,j s ω ⊤ is a σ-compatible play. By construction of the arena, it means that if

B Details of the proof of Theorem 5

Lemma 16. if σ is a winning strategy of G, then ν σ (ψ G ) = 1.

Proof. To prove lemma 16, we have to check that ν σ satisfies all terms of the equation 5 defining ψ G .

-

strategy is a total function) and thus there exists

ii) Let s 1 , s 2 , s 3 ∈ S, s 1 , s 2 ∈ P and s 2 , a, s 3 ∈ X . If ν σ ( s 1 , s 2 ∧ s 2 , a, s 3 ) = 1, then by definition of ν σ , there is a prefix of a play in A σ starting in s 1 and ending in s 2 , and (s 2 , a, s 3 ) ∈ δ σ . Therefore,

= 1 then all paths starting in s 1 and ending in s 2 in A σ visit a target state different from s 1 . Therefore, for each state s 3 ∈ S, if there is a path from s 1 to s 3 in A σ and (s 3 , b, s 2 ) ∈ δ σ then all the paths from s 1 to s 3 visit a state from F (different from s 1 ) -otherwise that would make a path from s 1 to s 2 without visiting a state from F . Hence, ν σ ( s 1 , s 3 ) = 1.

-Constraint (4): Let s ∈ S. We check each disjunct separately.

• If there is no play in A σ visiting s from s 0 , then ν σ ( s 0 , s ) = 0. It follows that ( 4) is satisfied. • If all prefixes of plays in A σ starting in s 0 and ending in s visit a target state, then ν σ ( s 0 , s ) = 1. It follows that ( 4) is satisfied. • If the first disjuncts are not satisfied, then there is a prefix of play in A σ from s 0 to s that visits no target states. Since σ is winning, we face two cases * either there is no cycle over s and then ν σ ( s, s ) = 0 with makes (4) true; * or, the cycle exists but then it visits a target state (otherwise this would be a play not winning), and then ν σ ( s, s ) = 1. Again, the formula (4) is satisfied. So, ν σ satisfies (4).

Since ν σ satisfies the constraints (1), ( 2), ( 3) and (4). Then ν σ (ψ G ) = 1. Lemma 17. If ν : X ∪ P ∪ W → {0, 1} is a valuation such that ν(ψ G ) = 1 then σ ν is a winning strategy for G.

Proof (Proof of lemma 17). Suppose that σ ν is not winning. then there exists a σ-compatible play s 0 s 1 • • • s i • π ω , with π = s i+1 • • • s ℓ for some ℓ ∈ N. and that play never visits a state from F . By induction on condition(??), we know that: ν( s 0 , s i ) = 1, ν( s 0 , s i ) = 0, ν( s i+1 , s i+1 ) = 1 and ν( s i+1 , s i+1 ) = 0. Indeed, there exists (s 0 , a 1 , s 1 ) ∈ δ and σ ν (s 0 ) = a 1 . By definition, ν( s 0 , a 1 , s 1 ) = 1 and then ν( s 0 , s 1 ) = 1 from (i). Also, because s 1 / ∈ F , ν( s 0 , s 1 ) = 0 from (iii). By induction, let k ∈ {0, • • • , i -1}, and suppose ν( s 0 , s k ) = 1 and ν( s 0 , s k ) = 0; there exists a k+1 ∈ Σ such that ν( s k , a k+1 , s k+1 ) = 1, and from (ii), we have ν( s 0 , s k+1 ) = 1. Besides, s k+1 / ∈ F and we have ν(¬ s k , a k+1 , s k+1 ∨ s 0 , s k ) = 0. Then, by (iv) ν( s 0 , s k+1 ) = 0. Therefore, ν( s 0 , s i ) = 0. In the same manner, we also obtain that ν( s i , s n ) = 0.

Finally, we observe thus that ν(¬ s 0 , s i ∨ s 0 , s i ∨ ¬ s i , s i ∨ s i , s i ) = 0, which is impossible because of ν(ψ G ) = 1.

⊓ ⊔


The impact of core precedences in a cyclic RCPSP with precedence delays

Zdenek Hanzalek, Claire