Positional-Player Games

Synthesis is the automated construction of a system from its specification [46]. A reactive system interacts with its environment and has to satisfy its specification in all environments [28]. A useful way to approach synthesis of reactive systems is to consider the situation as a game between the system and its environment. In each round of the game, the environment provides an assignment to the input signals and the system responds with an assignment to the output signals. The system wins if the generated computation satisfies the specification. The system and the environment are modeled by transducers, which direct them how to assign values to the signals given the history of the interaction so far.

Aiming to study realistic settings, researchers have studied bounded synthesis [50]. There, the input to the problem also contains bounds on the sizes of the transducers. Beyond modeling the setting more accurately, bounded synthesis has turned out to have practical advantages. Indeed, bounding the system enables a reduction of synthesis to SAT [19, 22]. Bounding both the system and the environment, a naive algorithm, which essentially checks all systems and environments, was shown to be optimal [38]. In richer settings, for example ones with concurrency, partial visibility, or probability, restricting the available memory is sometimes the key to decidability or to significantly improved complexity [9, 42, 16].

Algorithms for synthesis reduce the problem to deciding a two-player graph game. The arena of the game is a graph induced from the specification. The vertices are partitioned between the two players, namely the system and the environment. Starting from an initial vertex, the players jointly generate a play, namely a path in the graph, with each player deciding the successor vertex when the play reaches a vertex she owns. The objectives of the players refer to the infinite play that they generate. Each objective $\alpha$ defines a subset of $V^{\omega }$ [41], where $V$ is the set of vertices of the game graph.¹¹1As we elaborate in Section 2, all our results apply also for edge-based objectives, namely when $\alpha$ defines a subset of $E^{\omega }$, for the set $E$ of edges of the graph. For example, in games with Büchi objectives, $\alpha$ is a subset of $V$, and a play satisfies $\alpha$ if it visits vertices in $\alpha$ infinitely often.

In the graph-game setting, a strategy for a player directs her how to proceed in vertices she owns, and it is winning if it guarantees the satisfaction of the player’s objective. Winning strategies may need to choose different successors of a vertex in different visits to the vertex. Indeed, choices may depend on the history of the play so far. The number of histories is unbounded, and extensive research has concerned the memory requirements for strategies in games with $\omega$-regular objectives, namely the minimal number of equivalence classes to which the histories can be partitioned [51, 18, 8, 10]. For example, it is well known that a winning strategy for a conjunction of $k$ Büchi objectives requires memory $k$ [18]. In practice, the strategies of the system and the environment are implemented by controllers whose state spaces correspond to the different memories that the strategies require. Clearly, we seek winning strategies whose controllers are of minimal size. Of special interest are memoryless strategies (also called positional strategies), which depend only on the current vertex. For them, all histories are in one equivalence class, leading to trivial controllers.

The need to design efficient controllers has led to extensive research on memoryless strategies. Researchers identified positional objectives, namely ones in which both players can use memoryless strategies (formally, an objective $\alpha$ is positional if in all games with objective $\alpha$, the winner of the game has a memoryless winning strategy), and half-positional objectives, namely ones in which one of the players can use a memoryless strategy (formally, an objective $\alpha$ is $1$-positional ($2$-positional) if in all games with objective $\alpha$, if the system (environment, respectively) wins the game, then it has a memoryless winning strategy). For example, it is well known that parity (and hence, also Büchi) objectives are positional [21, 55, 26]. Then, Rabin objectives are $1$-positional, and their dual Streett objectives are $2$-positional [21, 35]. On the other hand, Muller objectives are not even half-positional. In addition, researchers study positional [25, 14, 45] and $1$-positional [36, 44, 7] fragments of objectives that are in general not positional. For example, [11] identifies a class of parity automata that recognize general $\omega$-regular positional objectives.

In this work we take a different view on the topic. Rather than studying the memory required for different types of objectives, we take the approach of bounded synthesis and study games in which the memory of the players is bounded, possibly to a level that prevents them from winning. We focus on controllers of size $1$. Note that while transducers of size $1$ are not of much interest, controllers of size $1$ in the game setting correspond to memoryless strategies, and are thus of great interest. Indeed, in applications like program repair [33, 27], supervisory control [17] and regret minimization [31], researchers have studied non-intrusive control, which is modeled by memoryless strategies. Although controllers of size $1$ do not always exist, due to the obvious implementation advantages, one can first try to find a controller of size $1$, and extend the search if one does not exist. Since memoryless strategies amount to consistent behavior, restricting the memory of the environment models setting in which the system may learn an unknown yet static environment [47, 48].

We define and study positional-player games (PPGs, for short), in which both players are restricted to memoryless strategies, and half-positional-player games (HPPGs, for short), in which only one player is restricted to memoryless strategies. We distinguish between positional-Player 1 games (PP1Gs, for short), in which only the system is restricted to memoryless strategies, and positional-Player 2 games (PP2Gs, for short), in which only the environment is restricted.

We study PPGs and HPPGs with Rabin, Streett, and Muller objectives, as well as with weighted multiple objectives [40]. Such objectives are of the form $⟨\alpha ,w,t⟩$, where $\alpha \subseteq 2^V$, is a set of objectives that are all Büchi, co-Büchi, reachability, or avoid objectives, $w:2^{\alpha }\to \text{IN}$ is a non-decreasing, non-negative weight function that maps each subset $S$ of $\alpha$ to a reward earned when exactly all the objectives in $S$ are satisfied, and $t\ge 0$ is a threshold. An objective can be viewed as a maximization objective, in which case the goal is to maximize the earned reward (and $t$ serves as a lower bound) or a minimization objective, in which case the goal is to minimize the earned reward (and $t$ serves as an upper bound). Weighted multiple objectives can express generalized objectives, namely when $\alpha$ contains several objectives, all of which have to be satisfied. A weight function allows for a much richer reference to the underlying objectives: prioritizing them, referring to desired and less desired combinations, and addressing settings where we cannot expect all sub-specifications to be satisfied together.

Studying the theoretical properties of PPGs and HPPGs, we start with some easy observations on how the positionality of the objective type causes different variants of PPGs to coincide. We then study determinacy for PPGs and HPPGs; that is, whether there always exists a player that has a winning strategy. Clearly, if a player wins in a game but needs memory in order to win, she no longer wins when restricted to memoryless strategies. Can the other player always win in this case? We prove that the answer is positive for prefix-independent objectives (and only for them). On the other hand, when the other player is restricted too, the answer may be negative; thus PPGs of all objective types that are not $1$-positional or not $2$-positional need not be determined. Also, interestingly, even for objectives that are $1$-positional, Player 1 may need memory in order to win against a positional Player 2. Indeed in games in which Player 2 wins when her memory is not bounded, Player 1 can win only by learning and remembering the memoryless strategy of Player 2.

We continue and study the complexity of deciding whether Player 1 or Player 2 win in a given PPG or HPPG. Our results are summarized in Tables 1 and 2. Since memoryless strategies are polynomial in the game graph, the problems for PPGs are clearly in ${\mathrm{\Sigma }}_2^{\text{P}}$, namely they can be solved in NP using a co-NP oracle. Indeed, one can guess a strategy for the system, then guess a strategy for the environment, and finally check their outcome. Our main technical contribution here is to identify cases in which this naive algorithm is tight and cases where it can be improved. Moving to HPPGs, deciding the winner involves reasoning about the graph induced by a given strategy, and again, the complexity picture is diverse and depends on the half-positionality of the objective, the determinacy of HPPGs, and the succinctness of the objective type. In particular, handling Muller objectives, we have to cope with their complementation (a naive dualization may be exponential) and to introduce and study the alternating vertex-disjoint paths problem, which adds alternation to the graph.

For $i\in \{1,2\}$, an objective type $\gamma$ is $i$-positional if for every $\gamma$-game $𝒢$, Player $i$ wins in $𝒢$ iff she has a memoryless winning strategy in $𝒢$. Then, $\gamma$ is positional iff it is both $1$-positional and $2$-positional, thus the winner of every $\gamma$-game has a memoryless winning strategy. If $\gamma$ is neither $1$-positional nor $2$-positional, we say that it is non-positional.⁴⁴4In the literature, $1$-positional and $2$-positional objectives are sometimes termed positional, and positional objectives are sometimes termed bipositional [11]. It is known that the objective types reachability, Büchi, and parity (and thus also avoid and co-Büchi) are positional [21], Rabin is $1$-positional (and thus Streett is $2$-positional) [35], and Muller is non-positional [18]. As for weighted multiple objectives, MaxWB and MinWB are $2$- and $1$-positional, respectively, whereas MaxWR and MinWR are non-positional [40].

We lift the notion of positionality to games, studying settings in which one or both players are restricted to memoryless strategies. For $i\in \{1,2\}$, a game is a positional-Player $i$ game if Player $i$ is restricted to memoryless strategies, and is a positional-player game (PPG, for short) if both players are restricted to memoryless strategies. Positional-Player 1 and positional-Player 2 games are also called half-positional-player games (HPPG, for short).⁵⁵5An automaton is determinizable by pruning if it embodies an equivalent deterministic automaton, thus if nondeterminism can be resolved in a memoryless manner [3]. This may hint on a relation to PP1Gs. However, the labels on the transitions of automata make the setting different, and reasoning about determinization by pruning is different from reasoning about PP1Gs [37, 2].

For a game $𝒢$, we use Pos-$𝒢$, 1Pos-$𝒢$, and 2Pos-$𝒢$ to denote the positional-player and half-positional-player variants of $𝒢$, respectively. Formally, for a game $𝒢=⟨G,\psi ⟩$, we have the following.

• $\mathrm{■}$

  Player 1 wins Pos-$𝒢$ iff she has a memoryless strategy $f_1$ such that for every memoryless strategy $f_2$ for Player 2, we have that $\mathrm{𝗈𝗎𝗍𝖼𝗈𝗆𝖾}(⟨f_1,f_2⟩)$ satisfies $\psi$.

• $\mathrm{■}$

  Player 1 wins 1Pos-$𝒢$ iff she has a memoryless strategy $f_1$ such that for every strategy $f_2$ for Player 2, we have that $\mathrm{𝗈𝗎𝗍𝖼𝗈𝗆𝖾}(⟨f_1,f_2⟩)$ satisfies $\psi$.

• $\mathrm{■}$

  Player 1 wins 2Pos-$𝒢$ iff she has a strategy $f_1$ such that for every memoryless strategy $f_2$ for Player 2, we have that $\mathrm{𝗈𝗎𝗍𝖼𝗈𝗆𝖾}(⟨f_1,f_2⟩)$ satisfies $\psi$.

We conclude with some easy observations about PPGs and HPPGs and positional and half-positional objectives. The first follows immediately from the fact that the restriction to memoryless strategies only reduces the set of possible strategies. For a player $i\in \{1,2\}$, we use $\tilde{i}$ to denote the other player; thus, if $i=1$, then $\tilde{i}=2$, and if $i=2$, then $\tilde{i}=1$.

We continue with observations that use the positionality of the objective type in order to relate different variants of PPGs. The proof of Theorem 4 follows immediately from the definitions and the proof of Theorem 5 can be found in the full version.

Games with $\omega$-regular objectives enjoy determinacy: in every game, one player wins [41]. In this section we study the determinacy of PPGs and HPPGs. As expected, restricting the strategies of both players makes some games undetermined. Surprisingly, we are able to prove that for every prefix-independent objective $\psi$ that is not positional, there is an undetermined PPG with the objective $\psi$. On the other hand, all HPPGs with prefix-independent objectives are determined. Thus, if a player needs memory in order to win a game with a prefix-independent objective, then restricting her to use only memoryless strategies without restricting her opponent, not only prevents her from winning, but also makes the opponent winning.

Given a game $𝒢$, we would like to decide whether Player 1 wins in 1Pos-$𝒢$, 2Pos-$𝒢$, and Pos-$𝒢$. The complexity of the problem depends on the type of objective in $𝒢$. In this section we present general complexity results for the problem. Then, in Sections 6, 7, and 8, we provide an analysis for the different objective types. Note that since not all PPGs and HPPGs are determined, the results for Player 2 do not follow immediately from the results for Player 1. They do, however, follow from results about the dual objective.

In this section we study Rabin and Streett (and their respective special cases ExistsC and AllB) PPGs and HPPGs. Our results are summarized in Table 1 below.

We start with HPPGs (see proof in the full version).

In this section, we study the complexity of Muller PPGs and HPPGs. Our results are summarized in Table 1. We start with PPGs. It is not hard to see that Muller is path-efficient, and so Theorem 9 implies that the problem of deciding whether Player 1 wins a Muller PPG is in ${\mathrm{\Sigma }}_2^{\text{P}}$. In Theorem 12, we proved that the problem is ${\mathrm{\Sigma }}_2^{\text{P}}$-hard for Rabin and even ExistsC PPGs, and as ExistsC $⪯$ Muller, it may seem that a similar lower bound would be easy to obtain. The translation from an ExistsC objective to a Muller objective may, however, be exponential [6], which is in particular the case for the objective used in the lower bound proof in Theorem 12. Note that the AllB objective used in the lower bound proof in Theorem 13 can be translated with no blow-up to a Muller objective, but deciding whether Player 1 wins an AllB PPG is NP-complete.

Accordingly, our first heavy technical result in the context of Muller PPGs is a proof of their ${\mathrm{\Sigma }}_2^{\text{P}}$-hardness. For this, we add an alternation to the problem of vertex-disjoint paths, used in [33] in order to prove NP-hardness for AllB PPGs. We show that a Muller objective can capture the alternation, which lifts the complexity from NP to ${\mathrm{\Sigma }}_2^{\text{P}}$.

We first need some definitions and notations. Consider a directed graph $G=⟨V,E⟩$. A path $p$ in $G$ is simple if each vertex appears in $p$ at most once. Two simple paths $p$ and $q$ in $G$ are vertex-disjoint iff they do not have vertices in common, except maybe their first and last vertices. The vertex-disjoint-paths (VDP, for short) problem is to decide, given $G$ and two vertices $s,t\in V$, whether there exist two vertex-disjoint paths from $s$ to $t$ and from $t$ to $s$ in $G$. The complementing problem, termed NVDP, is to decide whether there do not exist two vertex-disjoint paths from $s$ to $t$ and from $t$ to $s$ in $G$.

Now, the alternating NVDP problem (ANVDP, for short) is to decide, given a two-player game graph $G=⟨V_1,V_2,E⟩$ and two vertices $s,t\in V$, whether there exists a memoryless strategy $f_1$ for Player 1 in $G$ such that the $⟨G_{f_1},s,t⟩$ is in NVDP. That is, there do not exist two vertex-disjoint paths from $s$ to $t$ and from $t$ to $s$ in $G_{f_1}$.

In this section we study PPGs and HPPGs with weighted multiple objectives. We focus on games with underlying Büchi or reachability objectives. In the full version, we prove that the results for underlying co-Büchi or avoid objectives follow. Essentially, this follows from the fact that weighted objectives may be dualized by complementing either the type of the objective or the way we refer to the satisfaction value. Specifically, for an objective type $\gamma \in \{\text{R, A, B, C}\}$, let $\tilde{\gamma }$ be the dual objective, thus $\tilde{R}=A$ and $\tilde{B}=C$. Then, as shown in [40], for every $\gamma \in \{\text{R, A, B, C}\}$, every MaxW-$\gamma$ objective has an equivalent MinW-$\tilde{\gamma }$ objective of polynomial size, and vise versa. Our results are summarized in Table 2 below.

We start with PPGs with underlying Büchi and reachability objectives.

We introduced and studied positional-player games, where one or both players are restricted to memoryless strategies. Below we discuss two directions for future research.

The focus on memoryless strategies corresponds to non-intrusiveness in applications like program repair [33, 27], supervisory control [17], regret minimization [31], and more. More intrusive approaches involve executing controllers of bounded size in parallel with the system or environment, leading to bounded-player games. There, the input to the problem contains, in addition to the game $𝒢$, also bounds $m_1$ and $m_2$ to the sizes of the system and the environment. Player 1 wins $(m_1,m_2)$-$𝒢$ iff she has a strategy with memory of size at most $m_1$ that wins against all strategies of size at most $m_2$ of Player 2.

Note that the games $(1,1)$-$𝒢$, $(1,\mathrm{\infty })$-$𝒢$, and $(\mathrm{\infty },1)$-$𝒢$ coincide with Pos-$𝒢$, 1Pos-$𝒢$, and 2Pos-$𝒢$, respectively, and so our complexity lower bounds here apply also to the bounded setting. Moreover, if we assume, as in work about bounded synthesis [38], that $m_1$ and $m_2$ are given in unary, then many of our upper bounds here extend easily to the bounded setting. Indeed, upper bounds that guess memoryless strategies for a player can now guess memory structures of the given size, and reason about the game obtained by taking the product with the structures. Some of our results, however, are not extended easily. For example, the NP upper bound for Streett PPGs relies on the fact that for every memoryless strategy $f_1$ for Player 1, we have that Player 2 has a winning strategy in $G_{f_1}$ iff she has a memoryless winning strategy in $G_{f_1}$. When , the latter is not helpful for Player 2, and we conjecture that the problem in the bounded setting is more complex.

The second direction concerns positional-player non-zero-sum games, namely multi-player games in which the objectives of the players may overlap [13, 52]. There, typical questions concern the stability of the game and equilibria the players may reach [54]. In particular, in rational synthesis, we seek an equilibrium in which the objective of the system is satisfied [23, 15]. The study of positional strategies in the non-zero-sum setting is of particular interest, as it also restricts the type of deviations that players may perform, and our ability to incentivize or block such deviations [39].