Temporal Explorability Games

Temporal graphs have been used to analyse dynamic networks and distributed systems in dynamic topologies, such as dissemination/propagation of information [9, 12, 24, 36] or the spread of diseases [38]. There is a large body of mathematical work that considers temporal generalizations of various graph-theoretic notions and properties [11, 18, 31]. Related algorithmic questions include graph colouring [28], travelling salesman [32], maximal matchings [27], and checking the existence of temporal cliques [29], Eulerian circuits [7], vertex-cover sets [3], and explorability [1, 2, 14] (called exploration). Several prior works on explorability assume structural properties that ensure that the graph is explorable. Questions then focus on the minimal time to explore. Pelc [33] provides several sufficient conditions on temporal graphs to be explorable. Spirakis and Michail [32] showed that without assumptions on the graph, checking explorability can be done in linear time for static graphs and is $\mathrm{𝖭𝖯}$-complete for temporal graphs. In most of the works, a path in the temporal graph is allowed to wait at a vertex for an unbounded amount of time.

The edge relation is often deliberately left unspecified and sometimes only assumed to satisfy some weak assumptions about connectedness, frequency, or fairness to study the worst or average cases in uncontrollable environments. Depending on the application, one distinguishes between “online” questions (e.g. [19, 26]), where the edge availability is revealed stepwise, as opposed to the “offline” variant where all is given in advance. We refer to [13, 22, 30] for overviews of temporal graph theory and its applications.

Fijalkow and Horn [17] study games with generalized reachability objectives, which generalize not only reachability but also explorability games. Generalized reachability conditions are conjunctions of reachability conditions: $Player1$ aims to reach at least one vertex out of each of several target sets. Explorability thus corresponds to the case where every vertex forms a singleton target set. Solving generalized reachability games is $\mathrm{𝖯𝖲𝖯𝖠𝖢𝖤}$-complete [17], but in polynomial time if all target sets are singletons.

Reachability and parity games played on (symbolically represented) temporal graphs have been introduced in [6]; solving these games is $\mathrm{𝖯𝖲𝖯𝖠𝖢𝖤}$-complete. The lower bound was shown by reduction from the emptiness problem for unary alternating finite automata, crucially relying on the presence of antagonistic choice. As in [6], our notion of temporal graphs assumes that some edge must be traversed at every unit time. Waiting (not moving the token for a while) as occasionally permitted [30, 3] can be modelled by adding self-loops.

Turn-based games involving temporal constraints have also been studied in the context of games played on the configuration graphs of timed automata [4]. Solving timed parity games is complete for $\mathrm{𝖤𝖷𝖯}$ [8, 25] and the lower bound already holds for reachability games on timed automata with only two clocks [23]. However, the time in temporal graphs is discrete as opposed to the continuous time semantics in timed automata. A direct translation of (games on) temporal graphs to equivalent timed automata games requires two clocks: one to hold the global time used to check the edge predicate and one to ensure that time progresses one unit per step. Fearnley and Jurdziński [15] showed that the reachability problem (solving one-player reachability games) for two-clock timed automata is already $\mathrm{𝖯𝖲𝖯𝖠𝖢𝖤}$-hard. Our lower bound constructions have a similar flavour but are incomparable in that they do not re-prove nor are implied by their result. They make crucial use of resetting of clocks which is impossible in our model. Our construction in turn uses either antagonistic choice (Theorem 8) or the more powerful transition guards in symbolic representations (Theorem 9).

We study the complexity of solving explorability games and contrast the worst-case complexity for related decision questions for games played on static graphs versus temporal graphs. It turns out that explorability is no harder than reachability on static graphs whereas on temporal graphs, explorability games exhibit the hardness of generalized reachability when the temporal edge availability is given explicitly. For temporal explorability games with a succinct, symbolic representation, we have $\mathrm{𝖯𝖲𝖯𝖠𝖢𝖤}$-hardness for both variants but a $\mathrm{𝖯𝖲𝖯𝖠𝖢𝖤}$-$\mathrm{𝖤𝖷𝖯}$ complexity gap for two-player games. Specifically,

1. 1.

   on static graphs, solving explorability games is complete for polynomial time (and $\mathrm{𝖭𝖫}$-complete for one-player games);

2. 2.

   on explicitly represented temporal graphs, explorability games are $\mathrm{𝖯𝖲𝖯𝖠𝖢𝖤}$-complete ($\mathrm{𝖭𝖯}$-complete in the one-player variant);

3. 3.

   reachability and thus explorability games on symbolically represented temporal graphs are $\mathrm{𝖯𝖲𝖯𝖠𝖢𝖤}$-hard even in the single-player variant. This strengthens the known lower bound from [6] which required a second antagonistic player.

Figure 2 summarizes these and related claims. Our most involved constructions are the $\mathrm{𝖯𝖲𝖯𝖠𝖢𝖤}$ lower bounds, both from the satisfiability of quantified Boolean formulae (QBF).

Without loss of generality, assume that $t\in V_1$ and that each vertex has at least one outgoing edge. We construct $ℬ$ as follows. Firstly, for every edge between vertices $v,u$, introduce a new vertex $[v,u]\in V_1^{\prime }$ that can either move to $u$ or reset, i.e. move back to $s$. Secondly, from target $t$ there exists an edge to every other vertex.

We claim that Player 1 wins the reachability game on $𝒜$ if and only if she wins the explorability game on $ℬ$. Indeed, if Player 1 does not win on $𝒜$, then she cannot visit $t$ on either arena and therefore loses in both. Conversely, if Player 1 does win on $𝒜$, then she can explore $ℬ$ by repeatedly moving from $s$ to $t$; visit a previously unseen vertex, then reset to $s$. Note that a reduction from a one-player reachability game where Player 1 owns all the vertices will construct another one-player explorability game where this still holds. $◀$

The following characterization of explorability games is adapted from [17, Theorem 4], where $s⪯t$ denotes that Player 1 wins the reachability game from $s$ with target $t$.

Suppose both conditions 1 and 2 are true. Point 1 implies that there exists a linearization of all $n$ vertices such that $v_1⪯v_2⪯\mathrm{\dots }⪯v_n$. By Point 2 we have that $s⪯v_1$ and therefore there is such a linearization of $⪯$ with $v_1=s$. Consequently, for all there exists a Player 1 strategy ${\sigma }_i$ that wins the reachability game from $v_i$ to $v_{i+1}$. Player 1 can follow the ${\sigma }_i$ from $v_i$ until $v_{i+1}$ is reached, then switch to ${\sigma }_{i+1}$ and so on, until all vertices have been visited.

Suppose we have an arena where the first condition is false: there are $u,v\in V$ with $u⋠v$ and $v⋠u$. Regardless of the starting vertex $s$, once a play visits $u$, Player 1 cannot ensure to visit $v$ from then on (or vice versa). Finally, if the second condition is false then there must be one vertex $u$ that Player 1 cannot ensure to visit from $s$. $◀$

The hardness is a consequence of Lemma 3. Note that the explorability game constructed from a one-player reachability game is also one-player. As one and two-player reachability games are $\mathrm{𝖭𝖫}$-hard and $𝖯$-hard respectively, the lower bounds follow. The upper bounds follow from Lemma 4, observing that at most $n^2$ reachability queries are necessary to verify the two conditions in the lemma. These queries can be done in $\mathrm{𝖭𝖫}$ in the one-player case, and $𝖯$ in the two-player case. $◀$

The $\mathrm{𝖭𝖯}$-hardness is due to Michail and Spirakis [32, Proposition 2] by reduction from the Hamiltonian Path problem. Indeed, a directed graph with $n$ vertices has a Hamiltonian path if and only if it can be explored in exactly $n$ steps. A matching upper bound can be achieved by stepwise guessing an exploring path of length at most $h(G)$, which is polynomial given that the input graph is explicitly represented. $◀$

We now consider the impact of an antagonistic player for explorability on temporal graphs. A key element of our lower bound construction is the interaction of antagonistic choice and the passing of time. Our reduction, from QBF, relies on a time-bounded final “flooding phase” that allows exploration only if sufficient time is left, and which can only be guaranteed by winning the preceding QBF game.

The upper bound for solving explorability games on a temporal arena $𝒜$ follows from solving the generalized reachability game on the expansion of $𝒜$, where we have a target set $F_i=\{(v_i,\theta )\mid \forall \theta \in \{0,1,\mathrm{\dots },h(𝒜)\}\}$ for every vertex $v_i$ of $𝒜$. Generalized reachability games can be solved in $\mathrm{𝖯𝖲𝖯𝖠𝖢𝖤}$ [17, Theorem 1].

We provide a matching lower bound using a reduction from QSAT. Given a QBF formula $\mathrm{\Phi }=\exists x_1\forall x_2\mathrm{\dots }\exists x_n.C_1\wedge C_2\wedge \mathrm{\dots }\wedge C_k$, we construct a two-player explorability game $G_{\mathrm{\Phi }}$ on a temporal graph so that Player 1 wins iff $\mathrm{\Phi }$ is true. Let $\phi$ refer to the matrix $C_1\wedge C_2\wedge \mathrm{\dots }\wedge C_k$ of the given formula $\mathrm{\Phi }$, that is, each $C_i$ is a disjunction of at most $3$ literals. The game $G_{\mathrm{\Phi }}$ has vertices $V=V_{\forall }\uplus V_{\exists }\uplus \{q_{\phi }\}\uplus V_{\text{literals}}\uplus V_{\text{clause}}$, where

• $\mathrm{■}$

  the vertices $V_{\exists }=\{q_1,q_3,\mathrm{\dots },q_n\}$, $V_{literals}=\{q_{x_1},q_{\neg x_1},q_{x_2},q_{\neg x_2},\mathrm{\dots },q_{x_n},q_{\neg x_n}\}$ and $V_{clauses}=\{q_{C_1},q_{C_2},\mathrm{\dots },q_{C_k}\}$ are controlled by Player 1.

• $\mathrm{■}$

  the vertices $V_{\forall }\{q_2,q_4,\mathrm{\dots },q_{n-1}\}$ and $\{q_{\phi }\}$ are controlled by Player 2.

The game is played in $4$ phases, each of a fixed length, as follows.

1. 1.

   In the initial phase, from time $0$ to $k-1$, the game starts from $q_{C_1}$ and visits all clause vertices of $V_{clauses}$ in order and then ends up in the vertex $q_1$ corresponding to the first existential quantifier. Formally, the edges available during this phase are, for all , $E(q_{C_i},q_{C_{i+1}})=E(q_{C_k},q_1)=[0,k)$. Edges of the initial phase are drawn in red in the example in Figure 4.

2. 2.

   The selection phase, from time $k$ to $k+2n-1$, the game visits the vertices corresponding to the quantifiers in order of their appearance in the formula. Depending on whether the quantifier is $\exists$ (or $\forall$), Player 1 (respectively Player 2) chooses to visit a vertex corresponding to either a positive or negative literal for each variable. The edges available during this phase are for all , $E(q_i,q_{x_i})=E(q_i,q_{\neg x_i})=E(q_{x_i},q_{i+1})=E(q_{\neg x_i},q_{i+1})=E(q_{x_n},q_{\phi })=E(q_{\neg x_n},q_{\phi })=[k,k+2n)$. Corresponding edges are in blue in Figure 4 and corresponds to choosing a valuation for the variables in the formula $\mathrm{\Phi }$.

3. 3.

   The evaluation phase, at time $k+2n$ and $k+2n+1$, starts from vertex $q_{\phi }$, where Player 2 selects a clause $C_i$ by moving to vertex $q_{C_i}$. Formally, we have for all , $E(q_{\phi },q_{C_i})=\{k+2n\}$. From $q_{C_i}$, Player 1 has the choice to visit a literal vertex $q_{\mathrm{\ell }}$ at time $k+2n+1$ if $\neg \mathrm{\ell }$ is contained in the clause $C_i$, where $\mathrm{\ell }$ is a literal. After this phase, all vertices in $V_{\forall }\uplus V_{\exists }\uplus \{q_{\phi }\}\uplus V_{\text{clause}}$ have been visited as well as half of $V_{literal}$. In Figure 4, edges for the clause selection and literal selection are in green.

4. 4.

   The game ends after a flooding phase that lasts for exactly $n-1$ steps starting from time $k+2n+2$. That is, all edges become unavailable from time $k+3n+1$ onwards. During this phase, an edge is available from a literal vertex $q_{{\mathrm{\ell }}_i}$ to both literal vertex $q_{x_{i+1}}$ and $q_{\neg x_{i+1}}$. Formally, the edges $(q_{{\mathrm{\ell }}_i},q_{{\mathrm{\ell }}_{i+1}})$, for all and $(q_{{\mathrm{\ell }}_n},q_{{\mathrm{\ell }}_1})$, where ${\mathrm{\ell }}_j\in \{x_j,\neg x_j\}$, are available at times $[k+2n+2,k+3n+1]$. Thus, in this phase Player 1 can visit exactly $n-1$ of the possibly unexplored vertices. The flooding phase is shown in yellow in Figure 4.

Suppose the QBF formula $\mathrm{\Phi }$ is true. Then the $\exists$-player has a strategy to assign values to the variables $x_i$ (for odd $i$) to ensure that $\phi (\overrightarrow{x})$ is true. By following the same choices in the selection phase (moving $q_i\stackrel{}{⟶}{q}_{x_i}$ if $x_i$ is set to $true$ and $q_i\stackrel{}{⟶}{q}_{\neg x_i}$ otherwise), Player 1 guarantees that when $q_{\phi }$ is reached, the jointly chosen variable assignment $\overrightarrow{x}$ satisfies $\phi$. At this point the play has already visited exactly one vertex among $q_{x_j}$ and $q_{\neg x_j}$ for all $j\le n$. Moreover, no matter which vertex $q_{C_i}$ is chosen by Player 2 in the next step, the corresponding clause $C_i$ is also satisfied by assignment $\overrightarrow{x}$. By construction, this means there exists a literal ${\mathrm{\ell }}_j\in C_i$ such that vertex $q_{{\mathrm{\ell }}_j}$ has been visited before. The Player 1 can then move $C_i\stackrel{}{⟶}{q}_{\neg {\mathrm{\ell }}_j}$ to end the evaluation phase. Finally, in the flooding phase, Player 1 can freely move to visit the remaining $n-1$ literal vertices not visited thus far. This guarantees that indeed, all vertices have been visited and Player 1 wins the explorability game.

If the QBF instance $\mathrm{\Phi }$ is not satisfiable, then the $\forall$-player has a strategy to assign values to the $x_{2i}$ to ensure that $\phi (\overrightarrow{x})$ is false. By following the same choices during the selection phase (moving $q_i\stackrel{}{⟶}{q}_{x_i}$ if $x_i$ is set to $true$ and $q_i\stackrel{}{⟶}{q}_{\neg x_i}$ otherwise), Player 2 guarantees that when $q_{\phi }$ is reached, the jointly chosen variable assignment does not satisfy $\mathrm{\Phi }$, meaning that there is some clause $C_i$ that is not satisfied. In the evaluation phase, the strategy $\tau$ then picks $q_{C_i}$ as the successor from $q_{\phi }$. Consequently, all successors of $q_{C_i}$ must be vertices that have already been seen in the play. This means that exactly $n$ of the literal vertices are not yet visited. However, the game ends after the following $n-1$ of the flooding phase. Therefore, one of the literal vertices must be left unexplored. $◀$

We reduce QSAT to one-player temporal reachability with symbolic time encoding. Consider a quantified Boolean formula $\mathrm{\Phi }=\exists x_1\forall x_2\mathrm{\dots }\exists x_n:\phi$ where $\phi$ is a propositional formula with variables in $X=\{x_1,\mathrm{\dots },x_n\}$. Without loss of generality assume that the quantifiers alternate strictly, starting and ending with existential quantifiers (introduce at most $n+1$ useless variables otherwise). We show how to construct the symbolic one-player game $G_{\mathrm{\Phi }}$ such that $\mathrm{\Phi }$ is satisfiable if and only if some target vertex of $G_{\mathrm{\Phi }}$ can be reached. We use elapse of time to encode valuations of variables of $\mathrm{\Phi }$. At a time $\theta \ge 0$, since $\phi$ is quantifier-free, determining whether the valuation ${\nu }_{\theta }:X\to \{0,1\}$ makes $\mathrm{\Phi }$ true can be checked with a single transition that is available exactly at time $\theta$. The difficulty arises from encoding of the “adversarial” behaviour of universal quantifiers. To do so, we leverage both the graph structure and the Presburger arithmetic.

In our encoding, time is sectored into $n$ segments of 4 bits. The horizon of $G_{\mathrm{\Phi }}$ is thus $h(G_{\mathrm{\Phi }})=2^{4n}$. For every $i\in \{1,\mathrm{\dots },n\}$ and time $\theta \in \{0,\mathrm{\dots },2^{4n}-1\}$, we call ${\alpha }_i$, ${\beta }_i$, ${\gamma }_i$, and ${\delta }_i$ the four bits of the $i$th most significant sector, i.e., the bits at indices $(4n-1)-(4i-4)$, $(4n-1)-(4i-3)$, $(4n-1)-(4i-2)$ and $(4n-1)-(4i-1)$ in the binary expansion of $\theta$. In particular, ${\alpha }_1=4n-1$ and ${\delta }_n=0$ are respectively the most and the least significant bits. Intuitively, in the sequel we use ${\beta }_i$ to represent the chosen value of variable $x_i\in X$, we control overflows of ${\beta }_i$ with assumption on ${\alpha }_i$ and ${\gamma }_i$, and ${\delta }_i$ is an extra bit acting as buffer, to allow spending time without influencing the others. In the sequel, we define constrains on such bits. To do so, for all $k\in \{0,\mathrm{\dots },4n-1\}$ and all $v\in \{0,1\}$, we require the $k$th least significant bit of a given time $\theta \in \{0,\mathrm{\dots },2^{4n}-1\}$ to be $v$. This can be expressed thanks to following Presburger formula, which states that the $k$th least significant bit in the binary expansion of $\theta$ equals $v$.

In the following, we write ${\xi }_i=v$, where $\xi \in \{\alpha ,\beta ,\gamma ,\delta \}$ and $v\in \{0,1\}$ as a shorthand for the formula for checking the corresponding bits.

In $G_{\mathrm{\Phi }}$, each quantifier will have a corresponding vertex. If $x_i\in X$ is existentially quantified, the vertex $q_i$ evaluates $x_i$ thanks to a self-loop which also set ${\delta }_i=1$. In other words, Player 1 can use the self-looping transition of $q_i$ for spending time (not more than $2^{{\alpha }_i}$ steps since ${\alpha }_i$ must be $0$) which in particular leaves him possibility to set the bit ${\beta }_i$ as an encoding the value of $x_i$. Additionally, the non-looping transition of $q_i$ is available only when the bit ${\delta }_i$ is $1$. See the left gadget of Figure 5. Observe that, if $q_i$ is entered at time $\theta$ where ${\delta }_i=0$, there are exactly two times ${\theta }_0,{\theta }_1$ when $q_i$ can be exited, and ${\theta }_0$ and ${\theta }_1$ only differ on the bit ${\beta }_i$. Formally, ${\theta }_0=\theta +2^{(4n-1)-(4i-1)}$, ${\theta }_1={\theta }_0+2^{(4n-1)-(4i-3)}$. This is a direct consequence of the availability of both outgoing transitions of $q_i$ leaving only the bit ${\beta }_i$ as degree of freedom to Player 1. We shall prove that vertices encoding existential quantifiers are the only source of branching in $G_{\mathrm{\Phi }}$. If $x_i\in X$ is universally quantified, the self-loop of the vertex $q_i$ only serves to set ${\delta }_i=1$, the evaluation of $x_i$ being driven by vertices encoding existential quantifiers and auxiliary vertices $q_i^a$, $q_i^b$ and $q_i^c$. See the right gadget of Figure 5. The vertex $q_i$ admits two behaviours. If $q_i$ is entered at a time when ${\alpha }_i=0$, then $q_i$ exits toward the vertex encoding the next existential quantifier. Otherwise, ${\alpha }_i=1$ and then $q_i$ backtracks toward the auxiliary vertices of the previous universal quantifier. The elapsing of time while backtracking will set ${\gamma }_{i-2}$ to 1, and then sets it back to 0. If ${\beta }_{i-2}=0$, the side effect of backtracking is to switch ${\beta }_{i-2}$ from 0 to 1. Otherwise, ${\beta }_{i-2}=1$, and the side effect of backtracking is to switch ${\alpha }_{i-2}$ from 0 to 1, which triggers a further backtrack in $q_{i-2}$. To end the construction of $G_{\mathrm{\Phi }}$, we add two more vertices $q_{\phi }$ (to check the valuation of $\mathrm{\Phi }$ encoded by elapse of time) and $q_{\top }$ (to end the cascade of backtrack). A complete picture is given when $\mathrm{\Phi }$ has 5 quantifiers in Figure 6. The quantifier-free Presburger formula $\widehat{\phi }$ is defined as $\phi$ where every positive occurrence $x_i$ in $\phi$ is replaced by ${\beta }_i=1$ in $\widehat{\phi }$ and every negative occurrence $\neg x_i$ is replaced by ${\beta }_i=0$. The size of $G_{\mathrm{\Phi }}$, in particular the encoding of edges availability is discussed at the end of the proof.

Next, we prove that $\mathrm{\Phi }$ is satisfiable if and only if $G_{\mathrm{\Phi }}$ admits a path from $q_1$ to $q_{\top }$ composed of exactly $2^{4n}$ edges, thanks to the unrestricted self-loop on $q_{\top }$. The argument holds by induction on the odd number $n\ge 1$ of quantifiers. In the base case, $n=1$ and $G_{\mathrm{\Phi }}$ has three vertices $q_1,q_{\phi }$ and $q_{\top }$. We show that when $q_1$ is entered at time $0$, it can be exited only at time ${\theta }_0=1$ and ${\theta }_1=5$. By construction, $q_1$ can only be exited toward $q_{\phi }$ that has a single outgoing edge toward $q_{\top }$. Hence, the edge from $q_{\phi }$ to $q_{\top }$ can only be traversed at time ${\theta }_0+1=2$ or ${\theta }_1+1=6$ where ${\beta }_1=0$ and ${\beta }_1=1$ respectively. By definition of $\widehat{\phi }$, the vertex $q_{\top }$ is reachable if and only if $\mathrm{\Phi }$ is satisfiable.

Now, assume that $\mathrm{\Phi }$ has an odd number $n\ge 3$ of quantifiers. Let $\mathrm{\Phi }=\exists x_1\forall x_2{\mathrm{\Phi }}^{\prime }$ where ${\mathrm{\Phi }}^{\prime }=\exists x_3\forall x_4\mathrm{\dots }\exists x_n:\phi$. For all $v_1,v_2\in \{\text{false},\text{true}\}$, we denote ${\mathrm{\Phi }}^{\prime }[x_1\leftarrow v_1,x_2\leftarrow v_2]$ the formula ${\mathrm{\Phi }}^{\prime }$ where $x_1$ takes value $v_1$ and $x_2$ takes value $v_2$. Observe that ${\mathrm{\Phi }}^{\prime }[x_1\leftarrow v_1,x_2\leftarrow v_2]$ is a quantified Boolean formula without free-variable. For all $v_1,v_2\in \{\text{false},\text{true}\}$, by induction hypothesis $G_{{\mathrm{\Phi }}^{\prime }[x_1\leftarrow v_1,x_2\leftarrow v_2]}$ admits a path from $q_1^{\prime }$ to $q_{\top }^{\prime }$ composed of exactly $2^{4(n-2)}$ edges if and only if ${\mathrm{\Phi }}^{\prime }[x_1\leftarrow v_1,x_2\leftarrow v_2]$ is satisfiable. Intuitively, we construct such a path of $G_{\mathrm{\Phi }}$ from $q_1$ to $q_{\top }$ based on a path of $G_{{\mathrm{\Phi }}^{\prime }}$ from $q_1^{\prime }$ to $q_{\top }^{\prime }$. This is effective since $G_{{\mathrm{\Phi }}^{\prime }[x_1\leftarrow v_1,x_2\leftarrow v_2]}$ is a subgraph of $G_{\mathrm{\Phi }[x_1\leftarrow v_1,x_2\leftarrow v_2]}$ where $q_3$ and $q_2^a$ in $G_{\mathrm{\Phi }[x_1\leftarrow v_1,x_2\leftarrow v_2]}$ match respectively with $q_1^{\prime }$ and $q_{\top }^{\prime }$ in $G_{{\mathrm{\Phi }}^{\prime }[x_1\leftarrow v_1,x_2\leftarrow v_2]}$. In fact, $G_{{\mathrm{\Phi }}^{\prime }[x_1\leftarrow v_1,x_2\leftarrow v_2]}$ has an horizon of $2^{4(n-2)}$ because ${\mathrm{\Phi }}^{\prime }$ has $n-2$ quantifiers, and $q_2^a$ has a self-loop available at all time in this horizon, that is, $G_{{\mathrm{\Phi }}^{\prime }[x_1\leftarrow v_1,x_2\leftarrow v_2]}$ cannot modify the bits of bit sectors 1 and 2. Also, $q_3$ is entered only when the $4(n-2)$ least significant bits of the time are zero due to the availability of the edge from $q_2$ to $q_3$, and $q_2^a$ is leaved only if the $4(n-2)$ bits overflow due to as a direct consequence of the availability of the edge from $q_2^a$ to $q_2^b$.

We show that when $q_1$ is entered at time $0$, it can be exited only at time ${\theta }_0=2^{4n-4}$, ${\theta }_1=2^{4n-4}+2^{4n-2}$. Then $q_2$ is visited and since in both cases ${\alpha }_2=0$, by construction, the vertex $q_3$ is visited at time ${\theta }_0+2^{4n-8}$ or ${\theta }_1+2^{4n-8}$ (where ${\delta }_2$ switched to $1$). Let ${\theta }_0^{\prime }={\theta }_0+2^{4n-8}$ where ${\beta }_1=0$ and ${\theta }_1^{\prime }={\theta }_1+2^{4n-8}$ where ${\beta }_1=1$. In both cases, ${\beta }_2=0$. For all $k\in \{0,1\}$, by induction hypothesis, there is a path from $q_3$ at time ${\theta }_k^{\prime }$ to $q_2^a$ at time ${\theta }_k^{\prime }+2^{4(n-2)}-1$ if and only if ${\mathrm{\Phi }}^{\prime }[x_1\leftarrow k,x_2\leftarrow 0]$ is satisfiable. If ${\mathrm{\Phi }}^{\prime }[x_1\leftarrow 0,x_2\leftarrow 0]$ and ${\mathrm{\Phi }}^{\prime }[x_1\leftarrow 1,x_2\leftarrow 0]$ are not satisfiable, then $G_{\mathrm{\Phi }}$ cannot reach $q_{\top }$ from $q_1$ and $\mathrm{\Phi }$ is not satisfiable. Otherwise, the two paths in $G_{\mathrm{\Phi }}$ that reach $q_2^a$ at ${\theta }_0^{\prime }+2^{4(n-2)}-1$ and ${\theta }_1^{\prime }+2^{4(n-2)}-1$ can be extended to reach $q_2$ at time ${\theta }_0+2^{4n-6}$ and ${\theta }_1+2^{4n-6}$ respectively (where ${\beta }_2$ switched to $1$). Since ${\alpha }_2=0$ in both cases, the vertex $q_3$ is visited at time ${\theta }_0+2^{4n-6}+2^{4n-8}$ and ${\theta }_1+2^{4n-6}+2^{4n-8}$ respectively (where switched to ${\delta }_2=1$). Let ${\theta }_0^{\prime \prime }={\theta }_0+2^{4n-6}+2^{4n-8}$ where ${\beta }_1=0$ and ${\theta }_1^{\prime \prime }={\theta }_1+2^{4n-6}+2^{4n-8}$ where ${\beta }_1=1$. For all $v_1,v_2\in \{\text{false},\text{true}\}$, by induction hypothesis, there is a path from $q_3$ at time ${\theta }_k^{\prime \prime }$ to $q_2^a$ at time ${\theta }_k+2^{4(n-2)}-1$ if and only if ${\mathrm{\Phi }}^{\prime }[x_1\leftarrow k,x_2\leftarrow 1]$ is satisfiable. If ${\mathrm{\Phi }}^{\prime }[x_1\leftarrow 0,x_2\leftarrow 1]$ and ${\mathrm{\Phi }}^{\prime }[x_1\leftarrow 1,x_2\leftarrow 1]$ are not satisfiable, then $G_{\mathrm{\Phi }}$ cannot reach $q_{\top }$ and $\mathrm{\Phi }$ is not satisfiable. Otherwise, the two paths in $G_{\mathrm{\Phi }}$ that reach $q_2^a$ at ${\theta }_0^{\prime \prime }+2^{4(n-2)}-1$ and ${\theta }_1^{\prime \prime }+2^{4(n-2)}-1$ can be extended to reach $q_2$ at time ${\theta }_0+2^{4n-5}$ and ${\theta }_1+2^{4n-5}$ respectively (where ${\alpha }_2$ switched to $1$). Since ${\alpha }_2=1$, the vertex $q_{\top }$ is visited at time ${\theta }_0+2^{4n-5}+1$ and ${\theta }_1+2^{4n-5}+1$ respectively. Hence, $G_{\mathrm{\Phi }}$ admit a path from $q_1$ to $q_{\top }$ if and only if there is $k\in \{0,1\}$ such that ${\mathrm{\Phi }}^{\prime }[x_1\leftarrow k,x_2\leftarrow 0]$ and ${\mathrm{\Phi }}^{\prime }[x_1\leftarrow k,x_2\leftarrow 1]$ are satisfiable, i.e., if and only if $\mathrm{\Phi }$ is satisfiable.

It is worth emphasizing that, when $G_{\mathrm{\Phi }}$ admits a path from $q_1$ to $q_{\top }$, it can be constructed with a memoryless strategy. In the above reduction, for each vertex $q_i$ that encodes an existential quantifier, the inductively constructed strategy aims in $q_i$ at evaluating ${\beta }_i$ such that the next time $q_{\phi }$ is visited its outgoing edge will be available. Hence, in $q_i$, the strategy is solely based on the value ${\beta }_{i-1},\mathrm{\dots },{\beta }_1$. Since the vertices encoding existential quantifiers are the only source of branching in $G_{\mathrm{\Phi }}$, the strategy is memoryless.

Finally, we show that the size of $G_{\mathrm{\Phi }}$ is polynomial in the size of $\mathrm{\Phi }$. Here after, the size of the formula corresponds to the number of symbols to write it. The size of a symbolic temporal graphs $G$, is defined by $|G|=|V|+{\sum }_{(u,v)\in V^2}|E(u,v)|$. The graph $G_{\mathrm{\Phi }}$ has at most $4n+2$ vertices, and all availability are expressible by a Presburger formula of polynomial size in $|\mathrm{\Phi }|$. Since the horizon of $G_{\mathrm{\Phi }}$ is $2^{4n}$, each edge availability can be expressed as a conjunction of at most $4n$ formulas of the form ${\mathrm{\Psi }}_{k,v}$. $◀$

In the proof of Theorem 9, the number of quantifiers in $\mathrm{\Phi }$ determines the number of temporal edges used in the constructed symbolic temporal graph. The gadget to encode existential quantifiers uses two temporal edges and the one for universal quantifiers uses nine temporal edges, and there is one edge for the quantifier-free formula $\phi$ (see Figure 5). Note that if a quantifier block contains more than $m$ variables, we can blow up the number of bits polynomially by having bits ${\beta }_i^j$ for $1\le j\le m$, while keeping the number of temporal edges the same, thus obtaining a reduction from QSAT with a fixed number of quantifiers. $◀$ A similar ${\mathrm{\Pi }}_m^P$-hardness also holds for a different choice of $m$. Note that this is in contrast with the $\mathrm{𝖯𝖲𝖯𝖠𝖢𝖤}$-hardness proof for two-player reachability games on symbolic temporal graphs, where the problem is $\mathrm{𝖯𝖲𝖯𝖠𝖢𝖤}$-hard even with just one temporal edge [17, Theorem 1].

A restriction that makes the problem easier is allowing waiting. It is typical in study of temporal graphs to allow waiting for an arbitrary amount of time in temporal paths, i.e., instead of having to take an edge at every timestep, edges are traversed at increasing (but not necessarily consecutive) timesteps. This corresponds to having a loop on all vertices that can be traversed at any time. In case of two-player games, this allows Player 2 to stall infinitely and therefore is not interesting. The following remark states that the explorability on a one-player temporal arena with symbolic encoding becomes easy if waiting is allowed. We show that this holds even for generalized reachability objectives.

The $\mathrm{𝖭𝖯}$ lower bound follows from checking satisfiability of an existential Presburger formula, which is known to be $\mathrm{𝖭𝖯}$-complete [37]. Given a $\exists$PA formula $\varphi$ with no free variables, consider the symbolic temporal graph $V=\{s,t\}$, such that $E(s,t)\stackrel{\text{def}}{=}\varphi (x)$ is the only available edge, where $x$ is a variable that does not occur in $\varphi$. The vertex $t$ is reachable from $s$ if, and only if, $\varphi$ is true. For the upper bound, note that the length of a shortest witnessing path, measured by the number of edges traversed, is at most quadratic in the number of vertices of the graph. The $\mathrm{𝖭𝖯}$ upper bound can be shown by guessing the vertices visited along a play, together with the time they are visited first. The intermediate path between two such vertices can only visit linearly many vertices as no vertex is repeated in such a path. If a revisit is necessary, there is another path which waits instead. If a path does exist, then the time at which it is visited will at most be exponentially large and consequentially can be guessed in polynomial time. Therefore, by guessing the path and the times at which corresponding edges are taken, we obtain an $\mathrm{𝖭𝖯}$ algorithm. $◀$

Consider a generalized reachability game $G$ on arena $𝒜=(V_1,V_2,E)$ and with targets $ℱ=F_1,\mathrm{\dots }{F}_k$. Note that under symbolic encodings, temporal graphs are ultimately periodic, meaning that there are $b,p\in \mathbb{N}$ so that for every $i>b$, $i\in E(u,v)$ if, and only if, $i+p\in E(u,v)$. This is because the set of times at which any given edge is available is defined using a Presburger formula and thus semilinear [20]. Moreover, the least common multiple of the periods of the individual edges is therefore a period of (all edges in) the temporal graph and we can bound $b$ and $p$ to be at most exponential in the size of the input.

We can therefore construct an at most exponentially larger reachability game $G^{\prime }$ in which control states record the set of states (of $G$) that have already been visited, and the time up to and within the period. That is, define the arena ${𝒜}^{\prime }=(V_1^{\prime },V_2^{\prime },E^{\prime })$ where $V^{\prime }=V\times 2^V\times \{0,1,\mathrm{\dots },b+p-1\}$ and with edge relation $E^{\prime }$ so that $(u,S,\theta )\stackrel{}{⟶}(v,S\cup \{v\},{\theta }^{\prime })$ if $\theta \in E(u,v)$ and either ${\theta }^{\prime }=\theta +1$ or both $\theta =b+p-1\text{ and }{\theta }^{\prime }=b$. Player 1 owns a state $(u,S,\theta )$ in $G^{\prime }$ iff she owns $u$ in $G$. Finally, define the reachability target set in the constructed game $G^{\prime }$ as

Notice that any play from $(v,\mathrm{\varnothing },0)$ in $G^{\prime }$ uniquely corresponds to a play from state $s$ at time $0$ in the original game $G$. The second components within control states in $G^{\prime }$ are non-decreasing and record the set of states visited by the corresponding play in $G$. By definition of our reachability target $F^{\prime }$, we see that a play is winning for Player 1 in the constructed reachability game $G^{\prime }$ if, and only if, the corresponding play is winning for Player 1 in the generalized reachability game $G$.

Note that the size of $G^{\prime }$ is $|V|\cdot |2^V|\cdot (b+p)$, where $b,p\le 2^{𝒪(|G|)}$. The claim thus follows from the (known) facts that two-, and one-reachability games can be solved in polynomial time and logarithmic space, respectively. $◀$