Arthur Queffelec

Ocan Sankur

François Schwarzentruber

Planning for Connected Agents in a Partially Known Environment

Keywords: multi-agent path finding, multi-agent planning, connectivity, imperfect knowledge, decentralized planning

The Connected Multi-Agent Path Finding (CMAPF) problem asks for a plan to move a group of agents in a graph while respecting a connectivity constraint. We study a generalization of CMAPF in which the graph is not entirely known in advance, but is discovered by the agents during their mission. We present a framework introducing this notion and study the problem of searching for a strategy to reach a configuration in this setting. We prove the problem to be PSPACE-complete when requiring all agents to be connected at all times, and NEXPTIME-complete in the decentralized case, regardless of whether we consider a bound on the length of the execution.

Introduction

The coordination of mobile agents is at the heart of many real world problems such as traffic control [START_REF] Dresner | A Multiagent Approach to Autonomous Intersection Management[END_REF], robotics [START_REF] Erdem | A General Formal Framework for Pathfinding Problems with Multiple Agents[END_REF][START_REF] Yu | Planning Optimal Paths for Multiple Robots on Graphs[END_REF], aviation [START_REF] Pallottino | Decentralized Cooperative Policy for Conflict Resolution in Multivehicle Systems[END_REF] and more [START_REF] Silver | Cooperative Pathfinding[END_REF][START_REF] Yu | Optimal Multirobot Path Planning on Graphs: Complete Algorithms and Effective Heuristics[END_REF]. Some of these problems have multiple aspects which make them complex: (1) Some systems are multi-agent, that is, the behaviors of agents influence others' and these influences must be taken into consideration when computing missions; this can be due for instance, to collisions [START_REF] Ma | AI Buzzwords Explained: Multi-Agent Path Finding (MAPF)[END_REF], sensor interferences [START_REF] Goldberg | Interference as a Tool for Designing and Evaluating Multi-Robot Controllers[END_REF][START_REF] Schneider-Fontán | Territorial multi-robot task division[END_REF] etc.; (2) Some missions must ensure connectivity, that is, ensure periodic or constant connection to a station/agent to share acquired information [START_REF] Amigoni | Multirobot Exploration of Communication-Restricted Environments: A Survey[END_REF]; [START_REF] Yu | Planning Optimal Paths for Multiple Robots on Graphs[END_REF] The environment may be only partially known, and the agents may discover it during the mission [START_REF] Rao | Robot navigation in unknown terrains: Introductory survey of non-heuristic algorithms[END_REF][START_REF] Thrun | Robotic Mapping: A Survey[END_REF]. Several works have considered problems containing these three aspects. For instance, several algorithmic approaches have been investigated to solve the coordination of multirobot exploration [START_REF] Burgard | Coordinated multi-robot exploration[END_REF][START_REF] Wurm | Coordinated multi-robot exploration using a segmentation of the environment[END_REF][START_REF] Matignon | Coordinated multi-robot exploration under communication constraints using decentralized markov decision processes[END_REF]. Our objective in this paper is to present a framework to study the theoretical complexity of planning problems with respect to these three aspects.

The theoretical complexity of some related problems have been studied in the literature. Multi-Agent Path Finding (MAPF) is an important framework introduced to study collisionfree navigation of agents in warehouses (see [START_REF] Ma | AI Buzzwords Explained: Multi-Agent Path Finding (MAPF)[END_REF][START_REF] Felner | Search-based optimal solvers for the multi-agent pathfinding problem: Summary and challenges[END_REF]). This problem was intensively studied and gave rise to a popular algorithm known as Conflict-Based Search (CBS) [START_REF] Sharon | Conflict-based search for optimal multiagent pathfinding[END_REF]. An extension of MAPF with connectivity constraints, called Connected MAPF (CMAPF), was studied as well [START_REF] Hollinger | Multirobot Coordination With Periodic Connectivity: Theory and Experiments[END_REF]. The complexity of CMAPF and algorithmic solutions were studied in [START_REF] Tateo | Multiagent Connected Path Planning: PSPACE-Completeness and How to Deal With It[END_REF][START_REF] Charrier | Complexity of planning for connected agents[END_REF]. However, CMAPF only addresses the multi-agent and connectivity aspects, and not the partial knowledge of the environment. The latter aspect is considered in the Canadian Traveler Problem (CTP), which is a well-known problem to study the navigation of an agent in a partially known graph [START_REF] Papadimitriou | Shortest paths without a map[END_REF]. While the initial framework was for a single agent, CTP has been extended to multiple agents in the settings of packet routing [START_REF] Itai | Adaptive source routing in high-speed networks[END_REF], multirobot exploration [START_REF] Burgard | Collaborative multi-robot exploration[END_REF] and more [START_REF] Lita | A System for Multi-Agent Coordination in Uncertain Environments[END_REF]. While a notion of communication was considered in [START_REF] Zhang | The k-Canadian Travelers Problem with Communication[END_REF][START_REF] Shiri | On the Online Multi-Agent O-D k-Canadian Traveler Problem[END_REF], it is limited to settings where all agents can receive information at all times or only designated agents can send information. In contrast, we are interested in studying the setting where agents' ability to communicate depends on their positions in the graph, and in establishing theoretical complexity results of resulting problems.

In this paper, we study the theoretical complexity of generating plans for a group of agents to reach a given target configuration. More precisely, we analyze the impact of enforcing or ignoring: (A) connectivity; (B) collision; (C) a bound on the length of the execution. For (A), we consider either fully-connected strategies, requiring that the agents remain connected at all times during the mission, or a decentralized strategy, allowing agents to disconnect and reconnect. (B) In some applications, collisions can be handled by a local collision avoidance system [START_REF] Hollinger | Multirobot Coordination With Periodic Connectivity: Theory and Experiments[END_REF], and one can thus abstract away and ignore collisions in graph-based planning algorithms. (C) By providing a bound on the execution length, we can study the complexity of the decision problem associated to the optimization problem. Our results are summarized in Table 1. Interestingly, The PSPACE algorithm for the connected problem with a bounded execution is subtle and relies on a variant of the Savitch's theorem [START_REF] Savitch | Relationships Between Nondeterministic and Deterministic Tape Complexities[END_REF] we present here. Additionally, the PSPACE-completeness holds even in the case in which agents can always communicate, thus the hardness of the problem already comes from the incomplete knowledge of the movement graph. For the decentralized case, we prove the NEXPTIME-hardness in the bounded and unbounded cases by two separate reductions from the True Dependency Quantified Boolean Formula problem (TDQBF) [START_REF] Peterson | Lower Bounds for Multiplayer Noncooperative Games of Incomplete Information[END_REF], thus showing that the problem becomes significantly harder in this case.

Let us compare our results with known complexity results. In the fully known environment, the CMAPF problem is PSPACE-complete in the connected and unbounded case [START_REF] Tateo | Multiagent Connected Path Planning: PSPACE-Completeness and How to Deal With It[END_REF], while it is NP-complete in the bounded case (with the bound given in unary) [START_REF] Hollinger | Multirobot Coordination With Periodic Connectivity: Theory and Experiments[END_REF]. Thus, the partial knowledge of the environment does not render the problem harder in terms of complexity. In contrast, recall that in MAPF (without connectivity), one can check the existence of a solution in polynomial time [START_REF] Yu | Multi-agent Path Planning and Network Flow[END_REF], while the bounded problem is NP-hard [START_REF] Surynek | An Optimization Variant of Multi-Robot Path Planning is Intractable[END_REF], so the hardness is due to connectivity constraints. Some algorithms were presented for CMAPF in [START_REF] Tateo | Multiagent Connected Path Planning: PSPACE-Completeness and How to Deal With It[END_REF] that can scale up to about ten agents. Since both problems are similar and belong to PSPACE, one can hope that these approaches can be extended to the partial knowledge case. On the other hand, our results show that the complexity of the decentralized case is significantly higher. While some tools and algorithms are available for Decentralized POMDPs, which are in the same complexity class, the scalability is limited and the development of efficient algorithms for this case seems more challenging (see [START_REF] Amato | Decentralized Control of Partially Observable Markov Decision Processes[END_REF] for a survey).

Preliminaries

Connected MAPF. We consider a setting where agents move on a graph, with the vertices/nodes being their possible locations and the movement edges defining how they can move. In addition, communication edges define how the agents can communicate. The graphs we consider thus have two types of edges and are called topological graphs.

Definition 1. A topological graph is a tuple G = V, E m , E c , with V a finite non-empty set of vertices, E m ⊆ V × V a set of movement edges and E c ⊆ V × V a set of undirected communication edges.
A movement edge (u, v) is said to be undirected if (u, v), (v, u) ∈ E m . Figure 1 gives an example of a topological graph. For instance, an agent can go from 1 to 3 in one step. Two agents at vertices 1 and 5 can communicate, but two agents at 1 and 4 cannot.

We suppose that each vertex has a self-loop movement edge and a self-loop communication edge. This respectively represents the ability of an agent to stay at their location and to communicate with a nearby agent (i.e. at the same location/vertex). Definition 2. A configuration is a tuple c = c 1 , . . . , c n where c i is the vertex of agent i.

We write c → c when (c i , c i ) ∈ E m for all 1 ≤ i ≤ n. This means that each agent i can move from their vertex c i in c to their vertex c i in c in one step.

Definition 3 (Execution

). An execution π is a sequence of configurations π[0], π[1], . . . , π[ ] such that π[t] → π[t + 1] for all t ∈ {0, . . . , -1}.
We denote the length of π by |π|, and write π[0..t -1] to denote the sub-execution π[0], π [START_REF] Dresner | A Multiagent Approach to Autonomous Intersection Management[END_REF], . . . , π[t -1] of π. Moreover, last(π) denotes the last configuration of π.

We say that a configuration c is connected iff the subgraph of the vertices occupied by the agents form a connected graph for relation E c , i.e. the graph V a , E c ∩ (V a ×V a ) is connected with V a = {c 1 , . . . , c n }. An execution is said to be connected iff all its configurations are connected. The Connected Multi-Agent Path Finding problem consists in finding a connected execution for the agents from a given initial configuration to a target configuration. We summarize below the known complexity results for the CMAPF problem.

Theorem 1 ( [START_REF] Hollinger | Multirobot Coordination With Periodic Connectivity: Theory and Experiments[END_REF]). The problem of deciding whether, in a given instance (G, c s , c t , k) where k is unary, there is a connected execution from c s to c t of length at most k is NP-complete.

Theorem 2 ([19]

). The problem of deciding whether for a given instance (G, c s , c t , ∞), there exists a connected execution from c s to c t is PSPACE-complete.

We do not consider collision constraints which would forbid agents from sharing the same vertex. For CMAPF with perfect knowledge, executions are not harder to compute with or without collision constraints [START_REF] Tateo | Multiagent Connected Path Planning: PSPACE-Completeness and How to Deal With It[END_REF][START_REF] Charrier | Complexity of planning for connected agents[END_REF]. The same holds in our case, and we discuss, in the Section 6, how to incorporate these constraints in our setting. Dependency Quantified Boolean Formula. A Dependency QBF (DQBF) is a formula in which dependencies of existential variables over universal variables are explicitly specified. A DQBF is of the form ∀y 1 , . . . , y n ∃x 1 (O x1 ) . . . ∃x n (O xn ) ψ, where each O xi is, the dependency set, a subset of universally quantified variables, and ψ is a Boolean formula in CNF over x 1 , . . . , x n , y 1 , . . . , y n . It is worth noting that a QBF can be seen as a DQBF with

O x1 ⊆ O x2 ⊆ ... ⊆ O xn .
The True DQBF (TDQBF) is the problem of deciding whether a given DQBF holds. Formally, a DQBF ϕ holds iff there exists a collection of Skolem functions A = (A xi : {0, 1} Ox i → {0, 1}) i=1..n such that replacing each existential variable x i by a Boolean formula representing A xi , turns ψ into a tautology. TDQBF is NEXPTIME-complete [START_REF] Peterson | Lower Bounds for Multiplayer Noncooperative Games of Incomplete Information[END_REF], and will be used to prove NEXPTIME lower bounds in Section 5.

Our framework

Modeling Imperfect Information

To formalize CMAPF in the imperfect information setting, let us show how to represent the initial knowledge of the agents, and how the information they have evolves during the execution. Agents initially know the exact set of vertices, but only have a lower and an upper approximation of the actual graph: they know that some (communication or movement) edges are certain (they must be present), while some are uncertain (they may be absent).

Definition 4 (Initial Knowledge). The initial knowledge is modeled by a pair of topological graphs (G 1 , G 2 ), with the graph

G 1 = V, E m 1 , E
G = V, E m , E c is initially unknown to them. They only know that E m 1 ⊆ E m ⊆ E m 2 and E c 1 ⊆ E c ⊆ E c 2 , written as G 1 ⊆ G ⊆ G 2 . The perfect information case is captured by G 1 = G 2 (= G).
) if it is in E m 2 \ E m 1 (resp. E c 2 \ E c 1 )
. We assume that the communication edges of the actual graph are undirected, so for all

(u, v) ∈ E c 2 \ E c 1 , either (u, v), (v, u) ∈ E c , or (u, v), (v, u) ∈ E c . We say that an edge (u, v) is an uncertain undirected movement edge when (u, v), (v, u) ∈ E m 2 \E m 1 .
The environment can leave both edges (u, v), (v, u), remove both edges (u, v), (v, u), but also remove (u, v) and leave (v, u), or remove (v, u) and leave (u, v). That is, the movements edges of the actual graph are not necessarily undirected.

Example 1. Figure 2 depicts an initial knowledge (G 1 , G 2 ). The area is divided in two zones connected by two bridges, represented by the edges (s 2 , s 4 ) and (s 3 , s 5 ), with an uncertainty on which bridge is open and on the communication between s 1 and s 4 .

A strategy σ i for agent i tells where to go next after a given execution π. Formally: Definition 5. A strategy σ i for agent i maps any execution π to a vertex such that (v, σ i (π)) ∈ E m where v is the vertex at which agent i is in the last configuration of π.

A joint strategy σ is a tuple σ 1 , . . . , σ n where σ i is a strategy for agent i. The outcome of a joint strategy σ starting from configuration c s is the execution π defined by induction as follows: π[0] is c s , and for t ≥ 1, π[t] is the configuration in which agent i is at vertex

σ i (π[0..t -1]).
In the context of imperfect information, the behaviors of the agents only depend on their observations, as in imperfect information games as in [START_REF] Berthon | Strategy logic with imperfect information[END_REF]. The strategies, as defined above, do not necessarily take observations of the agents into account. We will now formalize observations and uniform strategies, that is, those respecting the observations of the agents.

In our setting, at any time, an agent observes all movement edges adjacent (both in-and out-coming) to the vertex v it occupies. Moreover, they observe the presence or absence of a communication edge between v and v if v is occupied by another agent with which there is a direct or indirect communication (via other agents). Intuitively, during an execution, at each step, each agent updates their knowledge about the graph with these observations they receive. Moreover, they share all their knowledge with all agents with which they are connected at each step.

The observation of adjacent movement edges has been a recurrent practice in theoretical works [START_REF] Papadimitriou | Shortest paths without a map[END_REF][START_REF] Bar-Noy | The Canadian Traveller Problem[END_REF] as well as robotics [START_REF] Dudek | Robotic exploration as graph construction[END_REF][START_REF] Koenig | Greedy Mapping of Terrain[END_REF], and our formalism is inspired from these works.

The knowledge of an agent at any time corresponds intuitively to a pair of graphs as in Definition 4. For agent i and execution π, let us denote by k i (π) G the knowledge of agent i about the graph after observing the execution π in actual graph G. Given such knowledge K = k i (π) G , the agent can deduce an under-approximation and an over-approximation of the actual graph; let us denote these by G K and G K respectively. In particular, if K is the knowledge the agents have initially, then

G K = G 1 and G K = G 2 .
We present a representation of the knowledge using predicates in the appendix where a detailed formalization of k i (π) G can be found.

In the rest of the paper, we assume all considered strategies to be uniform, that is, they comply with the knowledge of the agents: the strategies prescribe the same move to all executions that are indistinguishable with the agent's observations. Formally

, if |π| = |π | and k i (π) G = k i (π ) G , then σ i (π) = σ i (π ).

Decision Problems

We consider the decision problem of reaching a configuration c t from a configuration c s in less than k steps, using uniform strategies. For two configurations c s , c t , let us call a topological graph G (c s , c t )-admissible if there is an execution from c s to c t , which is not necessarily connected. Definition 6. We say that an instance

(G 1 , G 2 , c s , c t , k) is positive if there exists a joint strategy σ such that in all (c s , c t )-admissible graphs G satisfying G 1 ⊆ G ⊆ G 2 , the outcome of σ starting in c s ends in c t in less than k steps.
Observe that the above problem requires that a strategy ensures the reachability of the target configuration only for graphs that are (c s , c t )-admissible and compatible with the initial knowledge. In fact, intuitively, we would like the strategy to work under all possible graphs G with G 1 ⊆ G ⊆ G 2 . However, requiring a strategy to ensure reachability in a nonadmissible graph does not make sense, since even a strategy with full information would fail. We thus require the strategies to make their best efforts, that is, to ensure the objective unless it is physically impossible.

Example 2. Consider the example of Figure 2. If both bridges (i.e. movement edges (s 2 , s 4 ) and (s 3 , s 5 )) are absent in the actual graph, the graph is not (s 1 , s 6 )-admissible and there cannot be a strategy ensuring reachability. The admissible graphs contain either (s 2 , s 4 ), or (s 3 , s 5 ), or possibly both. Note that, this instance is negative for k < 6 (that is, it does not admit a solution). Indeed, consider a strategy that moves the agent, for instance, to s 2 . In the graph where (s 2 , s 4 ) is absent, the agent would need to come back to s 1 and take the alternative path, which requires an execution of total length 6; and the situation is symmetric if the first move is towards s 3 . The instance is nonetheless positive for k ≥ 6 with the described strategy. However, if the edges (s 2 , s 1 ) and (s 3 , s 1 ) were not present, then the instance would be negative. In fact, once the agent moves to s 2 or s 3 , they get stuck if the graph only contains the other bridge.

We now define the connected version of Definition 6. For two configurations c s , c t , we say that a topological graph G is (c s , c t )-c-admissible if there is a connected execution from c s to c t . We will often omit the pair of configurations which will be clear from the context, and write simply admissible or c-admissible. Definition 7. We say that an instance

(G 1 , G 2 , c s , c t , k) is c-positive if there exists a joint strategy σ such that in all (c s , c t )-c-admissible graphs G satisfying G 1 ⊆ G ⊆ G 2 ,
the outcome of σ starting in c s is connected and ends in c t in less than k steps.

In the connected case, agents cannot visit a disconnected configuration. Hence, the considered strategies only visit configurations that are certainly connected. Observe that agents can make observations about the presence or absence of communication edges while being connected and use this information later.

Example 3. Let us illustrate the above property on the example of Figure 3. Assume there are two agents, the starting and goal configurations are c s = s 1 , s 6 and c t = s 5 , s 7 , and the only uncertainty is about the movement edges (s 3 , s 5 ) and (s 4 , s 5 ). Here, Agent 2 could immediately move to her target s 7 ; however, she could also cooperate with Agent 1 and lower the total completion time. Indeed, from their start configuration s 1 , s 6 , the agents first move to s 2 , s 4 where Agent 2 observes whether (s 4 , s 5 ) is present. Assume the edge is present. Then, they follow the sequence s 4 , s 6 • s 5 , s 7 ; and otherwise s 3 , s 6 • s 5 , s 7 . Thus, in order to minimize the length of the execution, the agents do not always take their shortest paths but might help other agents by obtaining information about the graph. Consider now the same example in which the communication edge (s 3 , s 6 ) is uncertain. If this edge is absent then Agent 2 cannot help Agent 1 achieve the target faster since if the former moves to s 4 and (s 4 , s 5 ) is absent, then, in order to maintain connectivity, the next configurations should be s 4 , s 6 • s 2 , s 7 • s 3 , s 7 • s 5 , s 7 . An execution of the same size is obtained when Agent 2 moves to s 7 in the first step.

For both Definitions 6 and 7 above, let us call a joint strategy a witness if it witnesses the fact that the given instance is positive, and respectively, c-positive.

We instantiate the Connected MAPF problem in four different settings. The four following decision problems are defined depending on whether we consider the connectivity requirement and whether the bound is finite. Note that the bounded problems are the decision problems associated to the optimization problems.

Bounded Decentralized Reachability. Is given (G 1 , G 2 , c s , c t , k), with k < ∞, positive? Bounded Connected Reachability. Is given (G 1 , G 2 , c s , c t , k), with k < ∞, c-positive? Unbounded Decentralized Reachability. Is given (G 1 , G 2 , c s , c t , ∞) positive? Unbounded Connected Reachability. Given (G 1 , G 2 , c s , c t , ∞) c-positive?
As we will see, the encoding of the integer k does not change the overall complexity. Lower bounds are all obtained directly for the unary encoding; the lower bounds for the binary encoding follows. Concerning the upper bounds, we explain for each case how to design an algorithm with k encoded in binary.

Connected Reachability

We first address the case where agents must be connected at each step of the execution. In this case, agents share their knowledge at all times and thus the group of agents can be considered as a single agent playing against the environment.

Unbounded Case

We first focus on the existence of an unbounded connected strategy. Interestingly, we show that verifying the existence of a connected strategy in a partially known environment is not harder than in a perfectly known environment. Theorem 3. The unbounded connected reachability problem is PSPACE-complete.

Bounded Case

We now study the existence of a bounded connected strategy. We show that this problem is PSPACE-complete even when the communication graph is complete. Please find in supplementary material detailed proofs of the Lemmas 1, 2 and Theorem 5. Proof. Let us first prove the upper bound when k is given in unary. As APTIME = PSPACE [START_REF] Chandra | Alternation[END_REF], we give an alternating algorithm that runs in polynomial time, as follows. At each step, the existential player chooses the next connected configuration to move the agents; and the universal player chooses the information about the newly discovered edges. After k steps

s z v z u z u ¬z u z t z s z s ¬z v z v ¬z l z r z r ¬z l ¬z t ¬z t z . . . 3(i -1) + 1 . . . 3(i -1) + 2
. . .

3(i -1) + 2
. . . the algorithm accepts if the target configuration is reached, or the revealed edges mean that the graph is not c-admissible. The number of steps is bounded by k, which is polynomial, thus the algorithm runs in polynomial time.

There is one subtlety to prove the correctness. The alternating algorithm actually corresponds to a slight variant of our setting which can be seen as a game. In our setting, the environment chooses a graph G with G 1 ⊆ G ⊆ G 2 at the beginning, and the agents discover the graph G as they move. In contrast, in the alternating algorithm, the universal player reveals the graph step by step; therefore the environment might adapt the graph to the moves of the existential player.

Lemma 1. The alternating algorithm is correct.

When k is binary, the previous algorithm does not run in polynomial time. However, observe that the number of alternations can be bounded by a polynomial because there is only a polynomial number of steps in which the universal players reveal new information to the coalition of agents. In fact, the universal player is only useful when some agent is at a vertex that has not been seen before, and this can only happen a linear number of times. Furthermore, the previous algorithm runs in polynomial space.

When k is binary, our problem is in STA(poly(n), * , poly(n)) where STA(s(n), t(n), a(n)) is the set of problems decided in space O(s(n)), time O(t(n)) with O(a(n))) alternations. Our problem is in PSPACE thanks to the generalization of Savitch's theorem we prove:

Lemma 2. STA(poly(n), * , poly(n)) ⊆ PSPACE.
Intuitively, this lemma is proved by guessing the computations between each universal choice by a PSPACE oracle, which yields an overall PSPACE algorithm.

Theorem 5. The bounded connected reachability problem with complete connectivity is PSPACE-hard.

Proof. The lower bound is proven by reduction from TQBF.

Consider a QBF ϕ of the form ∀z 1 ∃z 2 . . . Q n z n ψ where ψ is a Boolean formula in conjunctive normal form with n variables and m clauses.

In the reduction, we call a movement path, from node v to node u, a chain of nodes linking v to u by movement edges. In addition, we denote an occurrence of a positive (resp. negative) literal of a variable z, by z (resp. ¬z)

We create the graphs G 1 and G 2 as described in Figure 6. More precisely, for each variable z, we create a gadget shown in Figure 6a. For each clause, we create a gadget as depicted in Figure 6b. In addition, we create a movement edge between a node v z (resp. v ¬z ) and a node t γ if the literal z (resp. ¬z) is present in the clause γ.

We define the initial and target configurations c s , c t as follows. There is a single agent at each vertex of the form s γ (resp. s z ) whose target is t γ (resp. t z ). Furthermore, at each s z (resp. s ¬z ) there is one agent for each clause that contains z (resp. ¬z) and her target is t z (resp. t ¬z ).

We show that ϕ is true iff

(G 1 , G 2 , c s , c t , k) is c-positive with k = 3(n -1) + 5.
For simplicity, we classify the agents as follows.

• A Variable agent is an agent starting at a node s z ;

• a Clause agent is an agent starting at a node s γ ;

• a Positive (resp. negative) occurrence agent is an agent starting at s z (resp. s ¬z ).

(⇒) Assume that the QBF ϕ is true. There exists a collection of Skolem functions A such that for each existential variable z i (where i is even), and an assignment ν to universally quantified variables in z 1 , z 3 , . . . , z i-1 , A zi (ν) ∈ { , ⊥} is the value assigned to z i such that ϕ is true under assignment ν augmented with the values of A. We construct the following strategy σ, which guarantees that c t is reached in k steps from c s .

Intuitively, the lengths of the initial movement paths are designed so that agents starting at s zi arrive at v zi in the order of their indices. For an existential variable agent, the choice of the successor from v zi determines the value of z i ; while for a universal variable agent, the choice is made by the environment. More precisely, if the agent moves to r zi , then z i is set to true, if she moves to l ¬zi it is set to false.

Formally, all agents start by moving to their respective v nodes (e.g. A clause agent at s γ moves to v γ ). They arrive at these nodes at different moments due to the sizes of their movement paths. An existential variable agent arrives at node v zi at time 3(i -1) + 1. At this point, all universal variable agents among z 1 , z 3 , . . . , z i-1 have arrived to their respective nodes v zj , thus revealing the values of these variables. Let ν be this assignment. If A zi (ν) = , the agent moves to r zi , and otherwise, to l ¬zi . When a universal variable agent arrives to v zi at time 3(i -1) + 1, she follows the only edge dictated by the environment, either to r zi or to l ¬zi . This assigns to the variable z i in the former case, and ⊥ in the latter case. Observe that if the graph is admissible, then there must exist a path from source to target for each agent; this means that one of these edges must be present.

Consider a positive (resp. negative) occurrence agent associated to a clause γ. This agent arrives to v zi (resp. v ¬zi ) at time 3(i -1) + 2. Observe that the variable agent has already determined the value of z i in the previous step.

• if z i is assigned (resp. ⊥) then the agent moves to t γ , observe which edges are available at t γ , and immediately comes back to v zi (resp. v ¬zi ). Now, the edge between r zi (resp. l ¬zi ) and u zi (resp. u ¬zi ) has been observed by agent z i ; so if this edge is present, she moves to r zi and u zi ; and if not, then the edge from l zi to u zi must be available, and she arrives to t zi (resp. t ¬zi ) at time k.

• if z i is assigned ⊥ (resp. ) then she does not visit t γ , but moves to l zi (resp. l ¬zi ). If the edge between l zi (resp. l ¬zi ) and u zi (resp. u ¬zi ) is available, she moves to t zi (resp. t ¬zi ), otherwise she moves back and reach t zi (resp. t ¬zi ) at time k, through r zi (resp. r ¬zi ).

It remains to argue that clause agents can reach their target nodes within k steps. Since ϕ is true, by the definition of A, whatever the choice for the universal variables, some literal of each clause γ is assigned to true. Therefore, the positive or negative occurrence agent corresponding to this literal visits t γ , thus revealing the edges available from t γ to r γ and l γ . Note that at least one of these edges must be available for the graph to be admissible. Thus, a clause agent arriving to v γ at time 3(n -1) + 3 can follow the available path to reach t γ exactly at time k.

(⇐) Let σ be a witness joint strategy. Following σ, each clause agent c must know the available edges in the rest of their paths at time 3(n -1) + 3 since otherwise they cannot ensure reaching t γ at time k. Thus, for each clause γ, the node t γ is visited by some occurrence agent under strategy σ. Furthermore, an occurrence agent z (resp. ¬z) can visit node t γ and still make it to t z (resp. t ¬z ) in time iff the associated variable agent has observed the presence of the edge between u z (resp. u ¬z ) and r z (resp. l ¬z ) beforehand. In fact, otherwise, if the occurrence agent makes a wrong guess between l z and r z , they will not arrive to t z (resp. t ¬z ) at time k. Hence, the joint strategy of the variable agents determines an assignment function which satisfies ϕ.

Our reduction actually builds an undirected movement graph. Thus, PSPACE-hardness holds already for undirected movement graphs. Note that in our current setting, pairs of uncertain edges of the form (u, v) and (v, u) are treated separately, but the lower bound proof still holds when they are seen as one.

Decentralized Reachability

We now tackle the case where agents are allowed to be disconnected; at each configuration, they share their knowledge with all agents to which they are connected. This case is harder because agents no longer follow a centralized strategy and they must cooperate to exchange information at the right moment to reach their targets. Proof Sketch. For the upper bound, an NEXPTIME algorithm consists in guessing uniform strategies for all agents and checking whether the joint strategy is a witness. Such a strategy has exponential size since it is a function of the sets of knowledge of the agents and the current vertex. One can enumerate all graphs G between G 1 and G 2 , and execute the joint strategy on G to check that it ensures the reachability of the target. Moreover, the executions to be checked have at most exponential length. In fact, executions can be seen as paths in a meta-graph where vertices are configurations augmented with the sets of knowledge of the agents. This meta-graph is of exponential size, so it is sufficient to consider executions of exponential length. The overall non-deterministic algorithm is thus in exponential time.

The lower bound is shown by reduction from TDQBF. Given a DQBF ϕ = ∀y 1 , . . . , y n ∃x 1 (O x1 ) . . . ∃x n (O xn ) ψ, we build an instance (G 1 , G 2 , c s , c t , k) of unbounded decentralized reachability. We denote by γ 1 , . . . , γ m the clauses in ψ.

The graph G 1 and G 2 as follows. For each variable z, we create the gadget depicted in Figure 5a.

We create the observation gadget for all existential variables x and for all (universal) variables y ∈ O x , depicted in Figure 5b. For convenience, we write O for the pair (x, y) corresponding to observation of y by x.

Finally, we create the clause gadget, depicted in Figure 5c. A vertex γ i certainly communicates with z iff z ∈ γ i , and with ⊥ z iff ¬z ∈ γ i . Moreover, the vertex v γ communicates with all z and ⊥ z for all variables z.

We define the initial and target configurations as c s = s γ , s γ1 , .

( z , γ i ) ∈ E c 1 when z appears in γ i (⊥z, γ i ) ∈ E c 1 when ¬z appears in γ i ( z , vγ ) ∈ E c 1 , (⊥z, vγ ) ∈ E c 1 Figure 5.
Gadgets in the reduction from DQBF to unbounded decentralized reachability.

Lemma 3. DQBF ϕ holds if and only if

(G 1 , G 2 , c s , c t , ∞) is positive.
Proof. We denote the agents as such: (1) an agent that starts at s z as the existential agent z if z is an existential variable; the agent is called universal if z is universal; (2) the verification agent is the one starting at s γ ; (3) the clause agents γ i start at s γi ; (4) the observation agents O start at s O .

(⇒) Suppose the DQBF ϕ holds, and let A be the collection of Skolem functions. We build the following joint strategy. The environment chooses the truth values of universal variables z by deleting some edges v z to z or v z to ⊥ z . If the environment deletes the edge v z to z , the agent is forced to pass in ⊥ z , thus the variable z is considered to be false. If the environment deletes the edge v z to ⊥ z , the agent is forced to pass in z , thus variable z is considered to be true. If the environment deletes neither edge, then we define the strategy for agent a y to choose to pass in y, making y true by default.

The rest of the strategy is defined as follows. At the first step, each variable agent for variable z moves to v z , and each observation agent for the pair (x, y) moves to v y , and thus observes the value of universal variable y. At the second step, existential agents remain in place, while observation agents move to v O , thus sharing their observations with the corresponding existential agents. Thus, at this point, each existential agent corresponding to variable x knows the values of all universal variables y ∈ O x . Then, agent z moves to z if A z (ν) = 1 and to ⊥ z otherwise, where ν is the valuation of the variables in O z .

All clause agents move from s i to γ i and remain at γ i for two steps so that all existential and universal variable agents z are at z or ⊥ z . The verification moves to v γ and also waits for two steps. Since each clause is satisfied by the currently read valuation, each clause agent γ i communicates at least with one existential or universal agent. Thus, the verification agent communicates with all clause agents via these variable agents. Since the clause agents communicate with the verification agent at this moment, the latter can see which edges are present in the clause gadget, and can continue go to t γ without getting stuck.

(⇐) Conversely, suppose there is a witness joint strategy, in particular ensuring that the verification agent goes to t z . This means that the agent must have received all the information about the topology around vertices γ 1 , . . . , γ k . But this is only possible if the agents have occupied a configuration in which the verification agent is at v γ , all clause agents are at γ i such that for each clause γ i , there is at least one variable agent z at z if z ∈ γ i and at ⊥ z if ¬z ∈ γ i . Thus, ϕ is a positive instance of TDQBF.

Bounded Case

In the bounded case, the problem is NEXPTIME-complete independently of the encoding of the bound. Moreover, the hardness holds even for undirected graphs.

Theorem 7. The bounded decentralized reachability problem is NEXPTIME-complete. NEXPTIME-hardness holds for undirected graphs.

The NEXPTIME algorithm is similar to that of Theorem 6. We just add a counter in the algorithm to count the number of steps when the joint strategy is checked. The lower bound is by reduction from TDQBF and follows the ideas of the reduction in Theorem 6.

Discussion

Additional Results. We present results obtained by a simple observation/modification.

Unbounded Reachability and Undirected Graphs. Both the unbounded connected and unbounded decentralized reachability become trivial on undirected graphs. This is because we only require reachability for (c-)admissible graphs. In the decentralized case, each agent can run a DFS independently, and eventually reach their targets in at most 2|V | steps, and a similar search can be done by the set of agents in the connected case.

Base Station. Several works consider a designated base vertex to which all agents must stay connected during the execution [START_REF] Tateo | Multiagent Connected Path Planning: PSPACE-Completeness and How to Deal With It[END_REF][START_REF] Charrier | Complexity of planning for connected agents[END_REF][START_REF] Charrier | Reachability and Coverage Planning for Connected Agents[END_REF]. This concept is only relevant in the connected case. Our results also hold with this additional constraint. In fact, the lower bound of Theorem 3 follows from [START_REF] Tateo | Multiagent Connected Path Planning: PSPACE-Completeness and How to Deal With It[END_REF], which proves the bound also with a base. In Theorem 5, we can add the base vertex as an isolated vertex so that the reduction is still valid.

Collisions. We did not require the paths to be collision-free in the results presented in this paper. However, this property is already ensured by our proofs or can be obtained by simple modifications. The lower bound proof of Theorem 3 relies on Theorem 2 from [START_REF] Tateo | Multiagent Connected Path Planning: PSPACE-Completeness and How to Deal With It[END_REF] which holds with collision constraints as well, so this is also true for our case. The proof of Theorem 5 does not generate collision-free paths as the groups of occurrence agents start and finish at the same location and follow almost the same path. This proof can be adapted to prevent collisions by delaying each occurrence agent by 3 steps behind one another. This can be achieved easily by extending the movement paths and shifting the starting location and target location of an agent up by 3 vertices behind the previous agent. The proof of lower bound of Theorem 6 features a construction ensuring a collision-free strategy. Indeed, the observations agents only need to take turns to visit the universal variables. Thus, the result holds with collision constraints as well. The algorithms of Theorem 3, 5, and 7 can be adapted by restricting all considered configurations to collision-free ones; while c-admissibility of a graph with collision constraints can be checked using Theorem 2.

Graph Classes. The MAPF and CMAPF problems have been studied for different classes of graphs (planar, grid, . . . ). The proof of lower bound in Theorem 3 relies on the proof of unbounded reachability done in [START_REF] Charrier | Complexity of planning for connected agents[END_REF], thus the result of PSPACE-hardness on planar graphs also carries over to our problem. Planar QBF is known to be PSPACE-complete [START_REF] Lichtenstein | Planar Formulae and Their Uses[END_REF], and the construction of Theorem 5 is such that when applied to a planar QBF, the resulting graph is planar. Our PSPACE-completeness result thus holds on planar graphs. Related Work. Different definitions of robust plans [START_REF] Ma | Multi-Agent Path Finding with Delay Probabilities[END_REF][START_REF] Atzmon | k-Robust Multi-Agent Path Finding[END_REF][START_REF] Atzmon | Probabilistic Robust Multi-Agent Path Finding[END_REF] have been studied. A k-robust plan guarantees the reachability of the target in the events of at most k delays. A p-robust plan executes without a conflict with probability at least p. Our framework does not consider delayed agents but focus on synchronous executions with imperfect knowledge of the area.

The problem of MAPF with a dynamic environment has multiple formulations. The Adversarial Cooperative Path-Finding [START_REF] Ivanová | Adversarial Cooperative Path-Finding: Complexity and Algorithms[END_REF] considers that the obstacles are agents which reason to prevent the cooperation to reach its goal. [START_REF] Murano | Multi-agent Path Planning in Known Dynamic Environments[END_REF] considered the problem where the dynamics of the environment is predictable. Additionally, when obstacles have unknown dynamics, one can estimate their movements and plan to minimize the probability of a collision [START_REF] Miura | Probabilistic Uncertainty Modeling of Obstacle Motion for Robot Motion Planning[END_REF], or predict their movements [START_REF] Griswold | Control for mobile robots in the presence of moving objects[END_REF] and plan online the movement of the agents [START_REF] Seok | A View-Time Based Potential Field Method for Moving Obstacle Avoidance[END_REF]. In our setting, the environment is static, thus, all observations are fixed.

MAPF with Uncertainty (MAPFU) asks for a plan which guarantees that mishaps, localization and sensing errors do not impact the proper execution of the plan. This problem can be solved by temporal logic [START_REF] Ulusoy | Robust multi-robot optimal path planning with temporal logic constraints[END_REF], POMDPs [START_REF] Miller | Coordinated Guidance of Autonomous UAVs via Nominal Belief-State Optimization[END_REF], replanning [START_REF] Stentz | Optimal and Efficient Path Planning for Unknown and Dynamic Environments[END_REF][START_REF] Ferguson | Replanning with RRTs[END_REF][START_REF] Likhachev | Anytime Dynamic A*: An Anytime, Replanning Algorithm[END_REF], interaction regions [START_REF] Dresner | A Multiagent Approach to Autonomous Intersection Management[END_REF][START_REF] Ferrari | Multirobot motion coordination in space and time[END_REF], and belief space planning [START_REF] Bry | Rapidly-exploring Random Belief Trees for motion planning under uncertainty[END_REF][START_REF] Gonzalez | Planning with uncertainty in position an optimal and efficient planner[END_REF][START_REF] Prentice | The Belief Roadmap: Efficient Planning in Belief Space by Factoring the Covariance[END_REF]. Nebel et al. [START_REF] Nebel | Implicitly Coordinated Multi-Agent Path Finding under Destination Uncertainty: Success Guarantees and Computational Complexity[END_REF] studied the MAPF problem with an uncertainty on the destination of the agents and lack of communication. The asynchronous movement of the agents, studied in those papers, cannot be expressed in our framework as we require the agent to follow some universal clock to execute their plan. Perspectives. We proposed a setting for CMAPF in the imperfect case and studied the theoretical complexity of the reachability problem. The first natural question is to find classes of graphs (e.g. grid graphs) on which the reachability problem is easier to solve, as it was done for MAPF in [START_REF] Wang | Tractable Multi-Agent Path Planning on Grid Maps[END_REF][START_REF] Banfi | Intractability of Time-Optimal Multirobot Path Planning on 2D Grid Graphs with Holes[END_REF], and CMAPF in [START_REF] Charrier | Complexity of planning for connected agents[END_REF]. Another possible direction is to study the coverage of all vertices [START_REF] Charrier | Complexity of planning for connected agents[END_REF]. An alternative way to handle non-admissible graphs is to require that agents return to their starting configuration if the graph is discovered not to be admissible. We believe that such variants should be as hard as reachability. Furthermore, there are several possible generalizations that could be considered by introducing dynamic environments (instead of static), faulty sensing of agents, robustness, uncertainty, etc. only depends on k(K 0 , π) G and c which the algorithm already has. There is an exponential number of possibilities, and these can be enumerated in polynomial space. For each case, we check recursively whether P (G K , G K , c , c t ). Since the knowledge can increase only a polynomial number of times (since the knowledge can only increase when an edge is added or removed), the depth of the recursive calls is polynomial. Thus, overall, the procedure uses polynomial space.

s z v z u z u ¬z u z t z s z s ¬z v z v ¬z l z r z r ¬z l ¬z t ¬z t z . . .
Bounded Case.

Proof of Lemma 1. First, observe that if the existential player has a strategy σ in the alternating algorithm, then the instance is c-positive. In fact, for any graph G with G 1 ⊆ G ⊆ G 2 , consider strategy τ of the universal player which makes choices according to G. Since this σ wins against τ , either the graph is not admissible or the agents successfully arrive to the target configuration. Conversely, assume that the instance is c-positive, that is, for all choices of an admissible graph G, the agents arrive at a target configuration under some joint strategy σ. We apply σ in the alternating algorithm. Consider any strategy τ of the universal player, and observe the execution induced by (σ, τ ). If the graph induced by τ is revealed not to be admissible, then the existential player wins. Otherwise, consider any admissible graph G with G 1 ⊆ G ⊆ G 2 compatible with the edges revealed during the execution of (σ, τ ). Since σ is winning in the original game when the underlying graph is G, the existential player also wins.

Proof of Lemma 2. To build a PSPACE algorithm, we perform a DFS of the computation tree T in a succinct manner. Consider the tree T , built from T , where we only keep vertices in which the universal player makes a decision, while paths along which only the existential player moves are shortcut into single edges. The depth of this tree is polynomial by definition. The idea is to run a DFS on T to check whether the machine accepts. This can be done in polynomial space provided that the children of all vertices can be computed in polynomial space. Successors of an existential configuration c in T are computed as follows: we generate on-the-fly all possible configurations c and test whether c is reachable from c in the original alternating machine by using a PSPACE oracle. The DFS that runs in PSPACE augmented with this PSPACE oracle gives a polynomial space procedure.

Proof of Theorem 5. The lower bound is proven by reduction from TQBF. corresponding existential agents. Thus, at this point, each existential agent corresponding to variable x knows the values of all universal variables y ∈ O x . Then, agent z moves to z if A z (ν) = 1 and to ⊥ z otherwise, where ν is the valuation of the variables in O z .

All clause agents move from s i to γ i and remain at γ i for two steps so that all existential and universal variable agents z are at z or ⊥ z . The verification moves to v γ and also waits for two steps. Since each clause is satisfied by the currently read valuation, each clause agent γ i communicates at least with one existential or universal agent. Thus, the verification agent communicates with all clause agents via these variable agents. Since the clause agents communicate with the verification agent at this moment, the latter can see which edges are present in the clause gadget, and can continue go to t γ without getting stuck.

(⇐) Conversely, suppose there is a witness joint strategy, in particular ensuring that the verification agent goes to t z . This means that the agent must have received all the information about the topology around vertices γ 1 , . . . , γ k . But this is only possible if the agents have occupied a configuration in which the verification agent is at v γ , all clause agents are at γ i such that for each clause γ i , there is at least one variable agent z at z if z ∈ γ i and at ⊥ z if ¬z ∈ γ i . Thus, ϕ is a positive instance of TDQBF.

Bounded Case.

Proof of Theorem 7. The upper bound when the bound k is given in unary is obtained by the following non-deterministic algorithm:

(1) Guess a strategy σ i for each agent i, up to executions of length ≤ k. Such a strategy can be represented as a tree of depth k, and thus has size exponential in k.

(2) Check that σ i is uniform for agent i.

(3) For all admissible graphs G such that G 1 ⊆ G ⊆ G 2 , execute the joint strategy σ and check that the outcome execution from the initial configuration leads to the target configuration.

The obtained algorithm is non-deterministic and runs in exponential time. Note that the encoding of k is not relevant since for k ≥ 2|V | there is always a solution following the unbounded case.

We now prove the NEXPTIME-hardness result by reduction from TDQBF. Given an instance of TDQBF ∀y 1 , . . . , y n ∃x 1 (O x1 ) . . . ∃x n (O xn ) ψ, we build an instance of bounded decentralized reachability (G 1 , G 2 , c s , c t , k). We denote the number of clauses by m.

We construct the graph G 1 as follows:

For each variable z, we create a gadget, as depicted in Figure 7a. We create the vertices s z , v z , z , ⊥ z and t z , and we create a movement path of length 3m + 1 from t z to z and ⊥ z . Then, if the variable z is universal, we create a movement path of length 3 × n 2 + 1 from s z to v z . If the variable z is x i , that is the i-th existential variable, we build a movement path of length 3 × n 2 -2|O z | + 1 from s z to v z as follows. We first build a movement path of length 3 × (in -|O z |). We then extend this movement by a vertex ρ y for each y ∈ O z . We extend our path from the last such vertex ρ y to v z by a movement path of length 3×(n 2 -in). Furthermore, we add a bidirectional edge between ρ y and v y .

We create the clause gadget, depicted in Figure 7b, composed of the vertices s γ , v γ , t γ and for all clauses γ i , the vertices u γi , l γi , r γi , s i , c i and t i . We create a movement path of length 3 × n 2 + 2 between s γ and v γ and between all s i and γ i . For all γ i , we create movement edges from u γi to l γi and to r γi , from the vertex γ i to u γi+1 , or t γ if i = m. In addition, we add a movement edge between v γ and u γ1 . For all γ i , we add a movement path of length 3m + 1 between vertices γ i and t i . Vertex γ i communicates with z iff z ∈ γ i , and with ⊥ z iff ¬z ∈ γ i . Moreover, vertex v γ communicates with all z and ⊥ z for all variables z. agents never meet in this phase of the execution. Agent z moves to z if A z (ν) = 1 and to ⊥ z otherwise, where ν is the valuation of the variables in O z .

All clause agents reach γ i at time 3 × n 2 + 2. Moreover, the verification agent is at v γ at this point, and all existential and universal variable agents z are at z or ⊥ z . Recall that all these vertices communicate. Since each clause is satisfied by the currently read valuation, each clause agent γ i communicates at least with one existential or universal agent. Thus, the verification agent communicates with all clause agents via these variable agents. Since the clause agents can see which edges are present in the clause gadget, the verification agent has now full information about this gadget, and can continue their path until t γ without backtracking, thus in total time 3 × n 2 + 2 + 3m + 1.

(⇐) Conversely, suppose there is a joint strategy enforcing that the verification agent goes to t γ in k steps. Thus, it means that she must have received all the information about the surroundings of the vertices γ 1 , . . . , γ k , as she has no time to backtrack from a wrong choice. This information can only be sent to the verification agent from the clause agents through the variable agents after 3 × n 2 + 2 steps. The variable agents representing the assignments are connecting (i.e. satisfying) all clauses. Indeed, for all γ i , there is one variable agent z at z if z ∈ γ i and at ⊥ z if ¬z ∈ γ i . Thus, the DQBF is a positive instance of TDQBF.

Figure 2 .

 2 Figure 2. An initial knowledge (G 1 , G 2 ).

  s

Theorem 4 .

 4 The bounded connected reachability problem is in PSPACE when the bound is given in binary.

  Clause gadget γ.

Figure 4 .

 4 Figure 4. Gadgets for the reduction from QBF into the bounded reachability problem in the complete connectivity case.

5. 1 .

 1 Unbounded Case Theorem 6. The unbounded decentralized reachability problem is NEXPTIME-complete.

  Clause gadget γ.

Figure 6 .

 6 Figure 6. Gadgets for the reduction from QBF to the bounded reachability problem in the complete connectivity case.

Table 1 .

 1 Complexity Results.

		Decentralized	Connected
	bounded unbounded	NEXP-complete PSPACE-complete (Th. 7) (Th. 4, 5) NEXP-complete PSPACE-complete (Th. 6) (Th. 3)	2 3	1 4	5	Vertex in V Movement edge in E m Undirected movement edges in E m Communication edge
							in E

c Figure 1. Example of a topological graph.

  Variable gadget for variable z. Edges between vz and l¬z, and between vz and rz are both certain if z is existential and both uncertain if z is universal.Movement edge that is certain if z is existential and uncertain if z is universal (vz, tγ ) ∈ E m 1 when z is an occurrence in γ (v¬z, tγ ) ∈ E m 1 when ¬z is an occurrence in γ

	3(n -i) -1 (a) Certain Movement edge ? ? ? ? ? Uncertain Movement edge r γ l γ s γ v γ . . .	t γ

3(n -i) + 2 ∀z ? ∃z ∀z ? ∃z . . . 3(n -i) -1 . . . ∀z ? ∃z

  . . , s γm , s x1 , . . . , s xn , s y1 , . . . , s yn , s O1 , . . . , s O k , and c t = t γ , t γ1 , . . . , t γm , t x1 , . . . , t xn , t y1 , . . . , t yn , t O1 , . . . , t O k .

	s z	v z	∃z ∀z ∃z ∀z ? ?	z ⊥ z	t z	s O	v y	v x v O	t O
	(a) Gadget for variable z. Both edges (vz, z )	(b) Gadget for the observation O of universal
	and (vz, ⊥z) are certain (resp. uncertain) if z is	variable y from existential variable x.
	existential (resp. universal).
				rγ 1	t1			rγ k	t k
	sγ	vγ	uγ 1	?	γ1	. . .	uγ k	?	γ k	tγ
				?				?
				lγ 1	s1			lγ k	s k
					(c) Clause gadget.
		Certain movement edge
		Certain communication edge
	?	Uncertain movement edge

∀z ? ∃z Certain (resp. uncertain) movement edge if z is existential (resp. universal)

  Variable gadget for variable z. Edges between vz and l¬z, and between vz and rz are both certain if z is existential and both uncertain if z is universal.

	3(i -1) + 1 . . . 3(i -1) + 2 . . . 3(i -1) + 2 (a) Certain Movement edge . . . 3(n -i) + 2 ∀z ? ∃z ∀z ? ∃z . . . 3(n -i) -1 . . . 3(n -i) -1 ? ? ? ? ? Uncertain Movement edge ∀z ? ∃z Movement edge that is certain if z is existential and uncertain if z is univer-sal (vz, tγ ) ∈ E m 1 when z is an occurrence in γ (v¬z, tγ ) ∈ E m 1 when ¬z is an occurrence in γ r γ l γ s γ v γ t γ . . .

Appendix A. Complements on the Imperfect Information Setting

We present here a formal modeling of the imperfect information in our setting. In our setting, at any time, an agent observes all movement edges adjacent (in-and outcoming edges) to the vertex v it occupies. Moreover, they observe the presence or absence of a communication edge between (v, v ) if v is occupied by another agent with which there is a direct or indirect communication (via other agents). Intuitively, during an execution, at each step, each agent updates their knowledge about the graph with these observations they receive. Moreover, they share all their knowledge with all agents with which they are connected at each step.

Given graph G = V, E m , E c , let us define the direct observation obs i (c) of agent i at a configuration c to be the set:

∪ {o c ci,cj | j is an agent and (c i , c j ) ∈ E c } (A.3)

where o m u,v , o ¬m u,v , o c u,v and o ¬c u,v are abstract terms that represent the observations. In the definition of obs i (c), points (1) and ( 2) mean that agent i directly observes the set of movement edges adjacent to her current position. Point [START_REF] Yu | Planning Optimal Paths for Multiple Robots on Graphs[END_REF] means that agent i observes a communication edge when she can communicate with another agent j. Point (4) means that agent i observes the absence of a communication edge when she sees that she can not communicate directly with another agent j but can communicate with j via multi-hop. That is, we say that j is an agent connected to i in c when there is a communication path c i1 , c i2 , . . . , c i k with i 1 = i and i k = j.

Let O denote the set of all observations. We define the knowledge of an agent as a subset of O. We define the initial knowledge for the pair (G 1 , G 2 ) as follows:

This corresponds to the a priori knowledge on the graph all agents have before making any observation.

During the execution, agents update their knowledge at each step, upon visiting a new configuration. Formally, the knowledge k i ((K j ) 1≤j≤n , π) G of agent i after observing execution π in actual graph G, where each agent j starts with initial knowledge K j , is defined by induction on π:

(a)

Intuitively, the knowledge of an agent is composed of (a) her knowledge collected until now, (b) her current observation, and (c) the knowledge of the agents she is connected to and their current observation.

When the agents start with an initial knowledge (G 1 , G 2 ) that is clear from the context, we will omit the tuple (K j ) 1≤j≤n and simply write k i (π) G .

Note that during a connected execution, all agents have an identical knowledge at all times. We thus omit the subscript i, and replace the tuple of initial knowledge sets by a single set K and write k(K, π) G rather than k i ((K j ) 1≤j≤n , π) G .

Appendix B. Proofs of Section 4

Unbounded Case. We formalize the intuition presented in the proof sketch of Theorem 3. We define the following recursive property: P (G, G, c, c t ) holds for graphs G, G, and configurations c, c t if either G is not (c s , c t )-c-admissible, or there exists a connected execution π from c to c t in G such that for all G with G ⊆ G ⊆ G, writing K 0 for the initial knowledge for the pair (G, G), there exists

The following two lemmas prove Theorem 3.

Proof. We prove the following more general property by induction on the number of edges present in G 2 and absent in

If G = G then either the instance is not c-admissible and, then, P (G, G, c, c t ) holds, or there is a connected execution in G from c to c t in which case the property holds as well.

Assume G G, and consider σ a witness strategy for the instance (G, G, c, c t , ∞). Consider a graph G ⊆ G ⊆ G. If the execution π induced by σ does not reveal any new observation in G, then it must end in c t and P (G, G, c, c t ) holds. Otherwise, let i 0 be the first step where a new observation is made. Since σ is a witness strategy, it is a witness for the instance

smaller number of differences than G and G, we conclude by induction that

Let us now show that all instances that satisfy the property are c-positive. Assume P (G 1 , G 2 , c s , c t ) holds. We define the joint strategy σ on all graphs G K and executions π in G K , such that P (G K , G K , last(π), c t ), by induction on the length of π.

Assume σ is constructed for an execution π and knowledge K.

then any strategy is a witness strategy so σ can be defined arbitrarily. Otherwise, consider the connected execution π given by P (G K , G K , last(π), c t ). We define σ so that agents follow π until index i 0 , in which case either π

Proof. The existence of a connected execution can be checked in polynomial space by Theorem 2. However, the size of such an execution can be exponential, and checking P (G 1 , G 2 , c s , c t ) requires iterating over the step of the execution. We thus need to combine the enumeration of the connected execution as we check P recursively.

The procedure to check P (G, G K , c, c t ) works as follows. We non-deterministically guess a connected execution step by step, from c to c t using the PSPACE algorithm of Theorem 2. We thus only keep the last configuration in memory, a binary integer counter to bound the length of the execution (bounded by the number of configurations, thus an exponential), and the current graph G K . If there is no such execution, we accept. Otherwise, at each step, say, after having visited execution π and generated next configuration c we enumerate all possible sets K = k(K 0 , πc ) G , where K 0 is the initial knowledge for the pair (G 1 , G 2 ). This can be done by enumerating all subsets of movement edges adjacent to c , present in G K but not in G K , and similarly communication edges revealed by c . Note that k(K 0 , πc ) G Consider a QBF ϕ of the form ∀z 1 ∃z 2 . . . Q n z n ψ where ψ is a Boolean formula in conjunctive normal form with n variables and m clauses.

In the reduction, we call a movement path, from vertex v to vertex u, a chain of vertices linking v to u by movement edges. In addition, we denote an occurrence of a positive (resp. negative) literal of a variable z, by z (resp. ¬z)

Let us describe the construction of the graph G 1 depicted in Figure 6. For each variable z, we create a gadget depicted in Figure 6a. Formally, for all variables z, the i-th quantified variable, we create the following vertices: s z , s z , s ¬z , v z , v z , v ¬z , u z , u z , u ¬z , t z , t z , t ¬z , l z , l ¬z , r z and r ¬z . We create the following movement paths: between s z and v z of length 3(i -1) + 1, between s z (resp. s ¬z ) and v z (resp. v ¬z ) of length 3(i -1) + 2, between u z and t z of length 3(n -i) + 2, and between u z (resp. u ¬z ) and t z (resp. t ¬z ) of length 3(n -i)-1. Then, we add the following movement edges: from u z (resp. u ¬z ) to l z (resp. l ¬z ) and r z (resp. r ¬z ), from u z to r z and l ¬z . Finally, if the variable z is an existential variable then we add movement edges from v z to r z and l ¬z .

We create clause gadgets as depicted in Figure 6b. Formally, for all clauses γ, we create the following vertices: s γ , v γ , l γ , r γ and t γ . We create a movement path of length 3(n-1)+3 from s γ to v γ . Finally, we create movement edges from v γ to l γ and r γ .

Note that G 2 contains G 1 and for all universal variables, it contains additionally the following movement edges: from v z to r z and l ¬z , from u z to r z and l z , from u ¬z to r ¬z and l ¬z , and from t γ to l γ and r γ .

We define the initial configuration and target configuration as follows: We show that ϕ is true iff

For simplicity, we classify the agents as follows.

• A Variable agent is an agent starting at a vertex s z ;

• a Clause agent is an agent starting at a vertex s γ ;

• a Positive (resp. negative) occurrence agent is an agent starting at s z (resp. s ¬z ).

(⇒) Assume that the QBF ϕ is true. There exists a collection of Skolem functions A such that for each existential variable z i (where i is even), and an assignment ν to universally quantified variables in z 1 , z 3 , . . . , z i-1 , A zi (ν) ∈ { , ⊥} is the value assigned to z i such that ϕ is true under assignment ν augmented with the values of A. We construct the following strategy σ, which guarantees that c t is reached in k steps from c s .

Intuitively, the lengths of the initial movement paths are designed so that agents starting at s zi arrive at v zi in the order of their indices. For an existential variable agent, the choice of the successor from v zi determines the value of z i ; while for a universal variable agent, the choice is made by the environment. More precisely, if the agent moves to r zi , then z i is set to true, if she moves to l ¬zi it is set to false.

Formally, all agents start by moving to their respective v vertices (e.g. A clause agent at s γ moves to v γ ). They arrive at these vertices at different moments due to the sizes of their movement paths. An existential variable agent arrives at vertex v zi at time 3(i -1) + 1. At this point, all universal variable agents among z 1 , z 3 , . . . , z i-1 have arrived to their respective vertices v zj , thus revealing the values of these variables. Let ν be this assignment. If A zi (ν) = , the agent moves to r zi , and otherwise, to l ¬zi .

When a universal variable agent arrives to v zi at time 3(i -1) + 1, she follows the only edge dictated by the environment, either to r zi or to l ¬zi . This assigns to the variable z i in the former case, and ⊥ in the latter case. Observe that if the graph is admissible, then there must exist a path from source to target for each agent; this means that one of these edges must be present. Consider a positive (resp. negative) occurrence agent associated to a clause γ. This agent arrives to v zi (resp. v ¬zi ) at time 3(i -1) + 2. Observe that the variable agent has already determined the value of z i in the previous step.

• if z i is assigned (resp. ⊥) then the agent moves to t γ , observe which edges are available at t γ , and immediately comes back to v zi (resp. v ¬zi ). Now, the edge between r zi (resp. l ¬zi ) and u zi (resp. u ¬zi ) has been observed by agent z i ; so if this edge is present, she moves to r zi and u zi ; and if not, then the edge from l zi to u zi must be available, and she arrives to t zi (resp. t ¬zi ) at time k.

• if z i is assigned ⊥ (resp. ) then she does not visit t γ , but moves to l zi (resp. l ¬zi ). If the edge between l zi (resp. l ¬zi ) and u zi (resp. u ¬zi ) is available, she moves to t zi (resp. t ¬zi ), otherwise she moves back and reach t zi (resp. t ¬zi ) at time k, through r zi (resp. r ¬zi ).

It remains to argue that clause agents can reach their target vertices within k steps. Since ϕ is true, by the definition of A, whatever the choice for the universal variables, some literal of each clause γ is assigned to true. Therefore, the positive or negative occurrence agent corresponding to this literal visits t γ , thus revealing the edges available from t γ to r γ and l γ . Note that at least one of these edges must be available for the graph to be admissible. Thus, a clause agent arriving to v γ at time 3(n -1) + 3 can follow the available path to reach t γ exactly at time k.

(⇐) Let σ be a witness joint strategy. Following σ, each clause agent c must know the available edges in the rest of their paths at time 3(n -1) + 3 since otherwise they cannot ensure reaching t γ at time k. Thus, for each clause γ, the vertex t γ is visited by some occurrence agent under strategy σ. Furthermore, an occurrence agent z (resp. ¬z) can visit vertex t γ and still make it to t z (resp. t ¬z ) in time iff the associated variable agent has observed the presence of the edge between u z (resp. u ¬z ) and r z (resp. l ¬z ) beforehand. In fact, otherwise, if the occurrence agent makes a wrong guess between l z and r z , they will not arrive to t z (resp. t ¬z ) at time k. Hence, the joint strategy of the variable agents determines an assignment function which satisfies ϕ.

Appendix C. Proofs of Section 5

Unbounded Case. Given ϕ, let (G 1 , G 2 , c s , c t , ∞) denote the graph built in the proof sketch of Theorem 6. Lemma 6. DQBF ϕ holds if and only if (G 1 , G 2 , c s , c t , ∞) is positive.

Proof. We denote the agents as (1) an agent that starts at s z as the existential agent z if z is an existential variable; the agent is called universal if z is universal; (2) the verification agent is the one starting at s γ ; (3) the clause agents γ i start at s γi ; (4) the observation agents O start at s O .

(⇒) Suppose the DQBF ϕ holds, and let A be the collection of Skolem functions. We build the following joint strategy. The environment chooses the truth values of universal variables z by deleting some edges v z to z or v z to ⊥ z . If the environment deletes the edge v z to z , the agent is forced to pass in ⊥ z , thus the variable z is considered to be false. If the environment deletes the edge v z to ⊥ z , the agent is forced to pass in z , thus variable z is considered to be true. If the environment deletes neither edge, then we define the strategy for agent a y to choose to pass in y, making y true by default.

The rest of the strategy is defined as follows. At the first step, each variable agent for variable z moves to v z , and each observation agent for the pair (x, y) moves to v y , and thus observes the value of universal variable y. At the second step, existential agents remain in place, while observation agents move to v O , thus sharing their observations with the

Gadgets for the reduction from DQBF to the bounded decentralized reachability problem.

Graph G 2 contains G 1 and for all universal variables z, we add movement edges: from v z to z and to ⊥ z , and for all clauses γ i , we add movement edges from the vertex γ i to l γi and to r γi .

We define the initial and target configurations as c s = s γ , s γ1 , . . . , s γm , s z1 , . . . , s zn and c t = t γ , t γ1 , . . . , t γm , t z1 , . . . , t zn .

We show that ϕ is a positive instance of TDQBF iff (G 1 , G 2 , c s , c t , k) is positive with k = 3 × n 2 + 2 + 3m + 1. We refer to an agent that starts at s z as the existential agent z if z is an existential variable; the agent is called universal if z is universal. The verification agent is the agent that starts at s γ and the clause agents γ i start at s γi .

(⇒) Suppose the DQBF holds, and let A be an assignment function. We build a joint strategy. The environment chooses the truth values of variables z by deleting some edges v z to z or v z to ⊥ z . If the environment deletes the edge v z to z , it enforces the agent to pass in ⊥ z , thus the variable z is considered to be false. If the environment deletes the edge v z to ⊥ z , it enforces the agent to pass in z , thus variable z is considered to be true. If the environment deletes neither edge, then we define the strategy for agent a y to choose to pass in y, making y true by default.

The strategy is defined as follows. Each existential agent z follows the movement path of length 3 × n 2 -2|O z | + 1 to v z , but whenever they have vertex v y as a neighbor, they visit v y , come back, and continue their paths. This happens exactly O z times, so at time 3 × n 2 + 1, the existential agent is at u z . Note that along this path the agent has visited all vertices v z with z ∈ O z , thus knows which edge among (v z , z ) and (v z , ⊥ z ) is present. Thus, upon arriving to v z , the agent has the knowledge of the valuation for all variables in O z . Observe also that by construction of the movement paths between s z and v z , the