Infinite-State Games with Energy Objectives Beyond Counters

For example, ($d$-dimensional) vector addition systems ($d$-VASS) are systems with access to $d$ counters – ranging over the natural numbers – which can be incremented and decremented, but not tested for zero. VASS are a pillar of verification and infinite-state research, because of their ability to model concurrent systems.

Unfortunately, with VASS configuration graphs as arenas, almost all games are undecidable. For example, games where the objective is to (i) reach a particular control-state (or configuration), or even just to (ii) sustain an infinite run, are both undecidable, already in dimension two [17, Thm. 13.1]. In fact, it is a well-known phenomenon that branching time logics are usually undecidable for VASS (e.g. see [15, Section 6] for a severely restricted branching logic; and see [16, Section 5] for more results), implying undecidability for many other kinds of games on VASS.

However, there is a “VASS-like” game that is decidable: Energy games. Here, the configurations consist of a control-state and counters that can be incremented and decremented. There are two players, the existential player ($\exists$), and the universal player ($\forall$). Here, $\exists$ has the objective of just playing infinitely long, such that the counter values stay non-negative. The difference to other games on VASS is, however, that in the arena, the configurations are over the integers. The fact that the counter values stay non-negative is part of $\exists$’s winning condition. The game can be viewed as “VASS-like”, since $\exists$ has to construct a VASS run. Energy games have received a significant amount of attention, with well-understood decidability and complexity [1, 22, 17, 5, 8, 10, 31, 12, 11, 9]. Thus, Energy semantics – making non-negativity part of the winning condition rather than the arena – achieves decidability.

In the quest for decidable games for infinite-state systems, the remarkable case of energy games thus raises the question: Does energy semantics also lead to decidability in broader classes of infinite-state systems?

To this end, we study Energy-like semantics on infinite-state systems other than VASS, and call them viability games. Here, we take a class of infinite-state systems with instructions like push, pop, increment, decrement and allow these instructions to be applied anytime. However, the winning condition of the existential player – whose goal it is to sustain an infinite run – includes that this run is confined to valid/viable configurations. Here, being valid/viable means that the configuration existed in the original system: This is precisely how energy games are related to games on VASS arenas. The term “viability” expresses that the existential player has to maintain a more general viability condition rather than specifically keeping energy levels non-negative.

We formalize viability games in the general framework of valence systems over graph monoids [37]. These systems consist of a finite-state automaton with access to an infinite-state storage mechanism, which is decribed by a finite undirected graph $\mathrm{\Gamma }$. For example, if $\mathrm{\Gamma }$ consists of isolated vertices without self-loops, then valence systems over $\mathrm{\Gamma }$ are pushdown automata. If $\mathrm{\Gamma }$ is a clique of $d$ vertices (without self-loops), then this realizes a $d$-dimensional VASS. Adding self-loops would yield a $d$-dimensional integer VASS. The framework can also realize combinations such as (i) pushdown VASS [19, 23], which feature both a pushdown and VASS counters or (ii) pushdowns of counters [35, 38, 36], where each stack entry contains a valuation of a set of counters.

Valence systems over graph monoids have been studied with respect to various algorithmic problems, such as reachability problems [38, 18, 39], decidable underapproximations [29, 33], finite-state abstractions [3, 36, 6], logics on configuration graphs [14] and even games played on configuration graphs, in Muskalla’s dissertation [30, Ch. 19]. Unfortunately, the results on games echo the abovementioned situation on pushdowns and VASS: Essentially, games with a control-state or configuration reachability objective are decidable for valence systems over $\mathrm{\Gamma }$ precisely when $\mathrm{\Gamma }$ realizes a pushdown [30, Thms. 19.2.1&19.2.10].

Our main results provide a full description of the decidability and complexity landscape of viability games across valence systems over graph monoids. Specifically, we study the problem of determining the winner of a viability game in two variants, inherited from energy games: In the fixed initial credit setting, the initial storage content is given; in the unknown initial credit setting, the task is to decide whether there exists a storage content (i.e. counter valuation, stack content, etc.) from which the existential player wins.

Moreover, we consider these problems in the general setting where graph $\mathrm{\Gamma }$ is drawn from a class $𝒢$ of graphs (that is closed under taking induced subgraphs). This captures settings where aspects of the storage mechanism are part of the input. For example, if $𝒢$ is the class of unlooped cliques of size $\le d$, then viability games over $𝒢$ correspond to $d$-dimensional energy games. If $𝒢$ contains all unlooped cliques, then viability games over $𝒢$ are energy games over arbitrary dimension (and the dimension is part of the input).

Our results show that for every choice of $𝒢$, the above problems are either (i) $𝖯$-complete, (ii) $\mathrm{𝖼𝗈𝖭𝖯}$-complete, (iii) $\mathrm{𝖤𝖷𝖯}$-complete, (iv) $\mathrm{𝟤}𝖤𝖷𝖯$-complete, or (v) undecidable.

Viability games are indeed decidable for a relatively broad class of systems. Among valence systems, viability games are decidable essentially for two kinds of systems: VASS (i.e. energy games) and what we denote as $\mathrm{𝖯𝖣}(\mathrm{𝖦𝗋𝗉})$. The latter are an extension of pushdown systems where each stack entry carries an element from some infinite group $G$. With the instructions, one can push and pop letters, but also multiply elements of $G$ onto the top-most group element on the stack. Here, pushing creates a fresh entry initialized to $1\in G$. Popping is only possible if the top-most group element equals the neutral $1\in G$. Thus, the invalid instructions (to be avoided by the existential player) are pops with (i) a mismatching stack letter or (ii) the top-most group element being $\ne 1$.

As an example, if $G$ is the group ${\mathbb{Z}}^d$ for some $d\ge 1$, then we call these systems $\mathrm{𝖯𝖣}(\mathbb{Z}-\mathrm{𝖵𝖠𝖲𝖲})$, because one has a stack whose entries carry integer vectors that can be incremented and decremented, as in $\mathbb{Z}$-VASS [20]. One can thus regard this as stacks of $\mathbb{Z}$-VASS configurations.

Decidability of viability games for $\mathrm{𝖯𝖣}(\mathrm{𝖦𝗋𝗉})$ is noteworthy for two reasons. First, in the classic setting (i.e. arenas of valid configurations) even the special case of $\mathrm{𝖯𝖣}(\mathbb{Z}-\mathrm{𝖵𝖠𝖲𝖲})$ is as unfavorable to games as VASS: even non-termination games are undecidable (see the full version [32]), already for $d=2$. Second, in $\mathrm{𝖯𝖣}(\mathrm{𝖦𝗋𝗉})$ overall (i.e. beyond the groups ${\mathbb{Z}}^d$), even ordinary (single-player) control-state reachability is undecidable. Thus, even though it is undecidable whether a valid pop will ever be executed, we can still decide viability games over $\mathrm{𝖯𝖣}(\mathrm{𝖦𝗋𝗉})$.

Energy games have received a significant amount of attention in recent decades [10, 1, 22, 17, 5, 8, 31, 12, 11, 9]. They are equivalent to Z-reachability games [5, 8], B-VASS games [31] and can also be viewed as alternating VASS [12]. As observed by Abdulla, Mayr, Sangnier, and Sprosten [2], instead of viewing energy games as VASS games with a modified semantics, one can equivalently view them as VASS games with the restriction of being one-sided, meaning the universal player cannot modify the counters. In the same way, viability games correspond to one-sided games over valence system arenas.

Another combination of energy games with infinite-state systems beyond counters has been studied in [1]. Their approach is to add counters to existing infinite-state systems (i.e. pushdown and one-counter systems) and apply energy semantics only to the extra counters: They show that (i) pushdown games with one energy dimension and (ii) one-counter games with two extra energy dimensions are undecidable, whereas one-counter games with one energy dimension are decidable. In our work, in contrast, the energy/viability semantics applies to the entire system. However, we observe that their undecidable “pushdown energy games” (i.e. pushdown systems with extra counters) reduce to pushdown VASS games under viability semantics (see the full version [32]).

In Section 2, we provide a self-contained description of the two types of infinite-state systems for which our results yield decidability. After this, we start with preliminaries in Section 3 and define viability games in Section 4. In Section 5, we state our two main results (Main Theorems A and B) and discuss implications. Then Section 6 gives an overview of the proof and of novel ingredients. In Sections 7, 8, 9, and 10 we then sketch our proofs. Remaining proof details can be found in the full version [32].

The first type of system is that of VASS. A ($d$-dimensional) vector addition system with states (VASS) is a pair $(Q,\delta ,q_{\mathrm{𝑖𝑛𝑖𝑡}})$ consisting of a finite set $Q$ of states and a finite set $\delta \subseteq Q\times {\mathbb{Z}}^d\times Q$ of transitions, and a final state $q_{\mathrm{𝑖𝑛𝑖𝑡}}\in Q$. A (valid) configuration¹¹1The reason we call these valid configurations is that in valence systems that correspond to VASS, we will have a more liberal notion of configurations (i.e. there are things called configurations that are not valid VASS configurations. However, to keep terminology simple in this section, we also just use the term configuration. is a pair in $Q\times {\mathbb{N}}^d$. A transition $t=(p,𝒖,q)\in \delta$ is valid in a configuration $(p,𝒙)$ if $𝒖+𝒙\in {\mathbb{N}}^d$, in which case the resulting configuration is $(q,𝒙+𝒖)$, and we write $(p,𝒙)\stackrel{𝑡}{\to }(q,𝒙+𝒖)$. A sequence $w=t_1\mathrm{\cdots }{t}_m$ of transitions is valid in a configuration $(p,𝒙)$ if there are configurations $(q_0,{𝒙}_0),\mathrm{\dots },(q_m,{𝒙}_m)$ such that $(p,𝒙)=(q_0,{𝒙}_0)$ and $(q_i,{𝒙}_i)\stackrel{t_i}{\to }(q_{i+1},{𝒙}_{i+1})$. In this case, we write $(p,𝒙)\stackrel{𝑤}{\to }(q_m,{𝒙}_m)$.

The second type of system is an extension of pushdown systems, where in between letters, one can store elements of a group. In the framework of valence systems, this group is always a graph group (also called right-angled Artin group), but in fact, our decidability proof applies to any finitely generated group with a decidable word problem. (Moreover, the $\mathrm{𝖤𝖷𝖯}$ complexity bound holds as soon as the word problem of the group is solvable in $\mathrm{𝖤𝖷𝖯}$). Since this more general setting is also easier to describe, we choose it here.

We begin with some terminology. A group is a set $G$ together with an associative binary operation $\cdot :G\times G\to G$ such that (i) there is a neutral element $1\in G$, i.e. $g\cdot 1=1\cdot g=g$, and (ii) every element $g\in G$ has an inverse $g^{-1}\in G$ such that $g\cdot g^{-1}=g^{-1}\cdot g=1$. For a subset $S\subseteq G$ and a sequence $w\in S^{\ast }$ over elements of $S$, we write $[w]\in G$ for the group element obtained by multiplying the elements in $w$. A generating set of $G$ is a subset $S\subseteq G$ such that every element of $G$ can be written as a product of elements in $S$ or in $S^{-1}:=\{s^{-1}\mid s\in S\}$. The group $G$ is finitely generated if it has a finite generating set. If $S$ is a finite generating set of $G$, then the word problem is the following decision problem: Given a string $w\in {(S\cup S^{-1})}^{\ast }$, decide whether $[w]=1$. It is well-known that decidability (or complexity, up to logspace reductions) of the word problem does not depend on the chosen generating set [26, p. 88].

From now on, we fix a finitely generated group $G$, with a finite generating set $W$. A $G$-pushdown system is a tuple $𝒫=(Q,\mathrm{\Sigma },\delta ,q_{\mathrm{𝑖𝑛𝑖𝑡}})$, where $Q$ is a finite set of states, $\mathrm{\Sigma }$ is its stack alphabet,

is its finite set of transitions, and $q_{\mathrm{𝑖𝑛𝑖𝑡}}\in Q$ is its initial state. Here, edges labeled $\mathrm{\Sigma }$ are push-transitions, i.e. an edge $(p,a,q)$ with $a\in \mathrm{\Sigma }$ pushes an $a$ on the stack. Edges labeled $\overline{\mathrm{\Sigma }}=\{\overline{a}\mid a\in \mathrm{\Sigma }\}$ are pop-transitions, i.e. an edge $(p,\overline{a},q)$ will pop an $a$ from the stack.

Formally, the elements of $G$ on edges of $𝒫$ are specified by words over $W\cup W^{-1}$, which is possible since $W$ is a generating set of $G$.

​​​​A (valid) configuration of $𝒫$ is a pair $(p,u)$, where $p\in Q$ and $u$ is a sequence $g_0{a}_1{g}_1\mathrm{\cdots }{a}_m{g}_m$, where $g_0,\mathrm{\dots },g_m\in G$ are group elements, and $a_1,\mathrm{\dots },a_m\in \mathrm{\Sigma }$ are stack letters. In such a configuration, a transition $t=(p,x,q)$ is valid if

1. a.

   $x\in \mathrm{\Sigma }$. In this case, $t$ is called a push transition and the resulting configuration is $(q,g_0{a}_1{g}_1\mathrm{\cdots }{a}_m{g}_{m}x1)$.

2. b.

   $x\in \overline{\mathrm{\Sigma }}$, say $x=\overline{a}$, and $a_m=a$ and $g_m=1$. In this case, $t$ is called a pop transition, and the resulting configuration is $(q,g_0{a}_1{g}_1\mathrm{\cdots }{a}_{m-1}{g}_{m-1})$.

3. c.

   $x\in G$. In this case, $t$ is called a group transition and the resulting configuration is $(q,g_0{a}_1{g}_1\mathrm{\cdots }{a}_m(g_{m}x))$. In other words, $x$ is multiplied onto the top-most group element.

In these cases, we write $(p,u)\stackrel{𝑡}{\to }(q,v)$, where $(q,v)$ is the resulting configuration. As above, we define $(p,u)\stackrel{𝑤}{\to }(q,v)$ to mean that $(q,v)$ can be reached via a sequence $w$ of valid transitions. In this case, the sequence $w$ is called valid in $(p,u)$.

Let us now describe viability games on VASS and group pushdown systems. Such a game is played by two players, the existential ($\exists$) and the universal player ($\forall$), and is specified by a VASS (resp. a group pushdown system), so that the set $Q$ of states is partitioned as $Q=Q_{\exists }\cup Q_{\forall }$, where $Q_{\exists }$ belongs to the existential player, and $Q_{\forall }$ belongs to the universal player. During a play, the two players choose transitions. Here, the chosen transition must always respect the current state. Moreover, the current state determines which player can choose the next transition.

The key idea is that the winning condition of the existential player requires (i) the play to be infinite and (ii) all prefixes of the transition sequence to be valid in the initial configuration. In the fixed initial credit setting, the initial configuration is the empty configuration: $(q_{\mathrm{𝑖𝑛𝑖𝑡}},\mathrm{𝟎})$ for VASS and $(q_{\mathrm{𝑖𝑛𝑖𝑡}},\epsilon )$ for group pushdown systems (here, $\epsilon$ is the empty sequence). In the unknown initial credit setting, we are asked whether there exists an initial configuration from which the existential player wins.

Crucially, observe that viability games on ($d$-dimensional) VASS are equivalent to ($d$-dimensional) energy games.

Consider a $G$-pushdown system $𝒫=(Q,\mathrm{\Sigma },\delta ,q_{\mathrm{𝑖𝑛𝑖𝑡}})$, where $Q=\{q_0,\mathrm{\dots },q_5\}$, $\mathrm{\Sigma }=\{a\}$, $q_{\mathrm{𝑖𝑛𝑖𝑡}}=q_0$ and $G=\mathbb{Z}\times \mathbb{Z}$ is the group with componentwise addition and neutral element $(0,0)$, generated by $W=\{(1,0),(-1,0),(0,1),(0,-1)\}$. The game is depicted in Fig. 1, where circle states belong to the existential player ($Q_{\exists }$) and square states to the universal player ($Q_{\forall }$).

In the fixed initial credit setting, the existential player does not win this game, as she cannot win from the initial configuration $(q_{\mathrm{𝑖𝑛𝑖𝑡}},\epsilon )$. In the unknown initial credit setting, however, she does win. Specifically, she wins from any initial configuration of the form $(q_{\mathrm{𝑖𝑛𝑖𝑡}},u\cdot a(0,-1))$, where $u=g_{0}a{g}_1\mathrm{\cdots }a{g}_m$ for $g_0,\mathrm{\dots },g_m\in \mathbb{Z}\times \mathbb{Z}$, i.e. any configuration with at least one $a$ and the topmost group element $(0,-1)$. To see why the top of the stack must be $a(0,-1)$: in order to sustain an infinite play, the existential player must eventually reach $q_2$, which requires applying the group transition $(0,1)$ followed by the pop transition $\overline{a}$. For the pop transition to be valid, the topmost stack entry must be $(0,-1)$, followed by the letter $a$, so that after the group transition $(0,1)$ the topmost group element becomes $(0,0)=1$ (the neutral element of $G$), as required for a valid pop, so the $a$ can be popped.

Once the existential player reaches $q_2$ with stack content $u$, she wins by the following strategy. From $q_2$, the universal player may take the self-loop any number of times $m\in \mathbb{N}$ (each time pushing an $a$ with group element $(0,0)$, leaving the stack as $u{a}^m$) before moving to $q_3$. From $q_3$, the existential player moves to either $q_4$ or $q_5$, depending on which transition the universal player took to $q_3$, with the stack content $u{a}^m$. In all cases, the existential player can navigate back to $q_2$ with stack content $u$, by popping the $m$ copies of $a$ using the self-loop on $q_5$. Since the same strategy applies from $q_2$ with any stack content, this produces an infinite sequence of valid transitions, and the existential player wins.

It follows from our results (see Section 5) that viability games are decidable (and, even in $\mathrm{𝖤𝖷𝖯}$) for $\mathbb{Z}\times \mathbb{Z}$-pushdown systems – in both the fixed and unknown initial credit settings (in fact, the decidability proof even applies to any group with a decidable word problem). However, perhaps surprisingly, if we replace one of the $\mathbb{Z}$-counters with a VASS counter (i.e. one that must be non-negative in valid configurations), viability games become undecidable.

In the general framework of valence systems over graph monoids, the storage mechanism of an infinite-state system is specified by an undirected graph that may have self-loops. Formally, a graph is a pair $\mathrm{\Gamma }=(V,E)$, where $V$ is its set of vertices and $E\subseteq \{S\subseteq V\mid |S|\le 2\}$ is its set of edges. Nodes $a,b\in V$ are adjacent if $\{a,b\}\in E$. Here, a singleton $\{a\}$ in $E$ is a self-loop (on $a$), so we say that $a$ is looped. A clique is a set of pairwise adjacent vertices. In an independent set, all vertices are pairwise non-adjacent. An induced subgraph of $\mathrm{\Gamma }$ is a graph $(V^{\prime },E^{\prime })$, where $V^{\prime }\subseteq V$ and also $E^{\prime }=\{S\in E\mid S\subseteq V^{\prime }\}$, i.e. among its vertices, ${\mathrm{\Gamma }}^{\prime }$ has precisely those edges that appear in $\mathrm{\Gamma }$. If there is no danger of confusion, we also call a graph $\mathrm{\Delta }$ induced subgraph of $\mathrm{\Gamma }$ if $\mathrm{\Delta }$ is isomorphic to an induced subgraph of $\mathrm{\Gamma }$.

To define the storage mechanism described by a graph $\mathrm{\Gamma }$, we need to introduce the congruence ${\equiv }_{\mathrm{\Gamma }}$. To $\mathrm{\Gamma }=(V,E)$, we associate the alphabet $\mathrm{\Sigma }=V\cup \overline{V}$, where we regard $V$ as an alphabet and $\overline{V}=\{\overline{a}\mid a\in V\}$ as a decorated version of $V$. We also define the involution $\overline{\cdot }:{\mathrm{\Sigma }}^{\ast }\to {\mathrm{\Sigma }}^{\ast }$, where $a\mapsto \overline{a}$ and $\overline{a}\mapsto a$ and $w=a_1\mathrm{\cdots }{a}_n\mapsto {\overline{a}}_n\mathrm{\cdots }{\overline{a}}_1$. On ${\mathrm{\Sigma }}^{\ast }$, the set of words over $\mathrm{\Sigma }$, we consider the smallest congruence ${\equiv }_{\mathrm{\Gamma }}$ that satisfies:

Here, $a=b$ is allowed, meaning if $a$ is looped, then $\overline{a}a{\equiv }_{\mathrm{\Gamma }}a\overline{a}{\equiv }_{\mathrm{\Gamma }}\epsilon$. The congruence gives rise to a monoid, which is a set $M$ together with an associative operation and a neutral element $1\in M$. Specifially, we have the monoid ${𝕄}_{\mathrm{\Gamma }}:={\mathrm{\Sigma }}^{\ast }/{\equiv }_{\mathrm{\Gamma }}$. For a word $w\in {\mathrm{\Sigma }}^{\ast }$, we use $[w]$ to denote the congruence class of $w$.

Traditionally, the monoid ${𝕄}_{\mathrm{\Gamma }}$ is used to define “valence automata (over ${𝕄}_{\mathrm{\Gamma }}$)” that accept languages. Here, each edge carries an input word and a word over $\mathrm{\Sigma }$, where words $w\in {\mathrm{\Sigma }}^{\ast }$ are viewed as (sequences of) storage instructions. Then a run with instructions $w_1,\mathrm{\dots },w_n$ on its edges is accepting if $[w_1\mathrm{\cdots }{w}_n]=1$. Intuitively, this is because such a sequence $w_1\mathrm{\cdots }{w}_n$ has neutral effect: A pushdown automaton accepts if the instruction sequence brings the empty stack back to the empty stack (or equivalently, brings any possible stack back to itself); a VASS accepts if the instruction sequence brings the empty counters back to the empty counters (equivalently, brings any counters valuation back to itself). Note that this way, elements $[w]$ can be viewed both as configurations (i.e. the one reached by applying $w$) and as actions: applying $[w]$ to $[u]$ yields $[w][u]=[wu]$.

With suitable $\mathrm{\Gamma }$, one can now realize classical storage mechanisms like pushdowns or counters. For example, if $\mathrm{\Gamma }$ has no edges (not even self-loops), valence automata over $\mathrm{\Gamma }$ are essentially pushdown automata with stack alphabet $V$. A word $w\in {\mathrm{\Sigma }}^{\ast }={(V\cup \overline{V})}^{\ast }$ has $[w]=1$ if and only if $w$ can be brought to the empty word by deleting factors $a\overline{a}$. Viewing $V$ as push instructions and $\overline{V}$ as pop instructions, this is equivalent to $w$ being a sequence of instructions that bring the empty stack back to the empty stack.

Let $\mathrm{\Gamma }$ be an unlooped clique, i.e. a clique without self-loops. Then $w\in {\mathrm{\Sigma }}^{\ast }={(V\cup \overline{V})}^{\ast }$ has $[w]=1$ if and only if, for each $a\in V$, every prefix $u$ of the projection of $w$ to just $\{a,\overline{a}\}$, has the property ${|u|}_a\ge {|u|}_{\overline{a}}$, and also ${|w|}_a={|w|}_{\overline{a}}$. Thus, $[w]=1$ if and only if $w$ is a sequence of increment ($a$) and decrement ($\overline{a}$) operations that bring all counters from zero to zero, while maintaining non-negativity. Thus valence automata over $\mathrm{\Gamma }$ are $d$-VASS for $d=|V|$.

If $\mathrm{\Gamma }$ is a looped clique, i.e. a clique of looped vertices, then $w\in {\mathrm{\Sigma }}^{\ast }$ has $[w]=1$ if and only if ${|w|}_a={|w|}_{\overline{a}}$ for each $a\in V$, and ${𝕄}_{\mathrm{\Gamma }}\cong {\mathbb{Z}}^d$ for $d=|V|$. Hence valence automata over looped cliques are $\mathbb{Z}$-VASS [20]: counter machines with integer-valued counters.

Finally, suppose $\mathrm{𝖯𝟥}$ is the graph , i.e. the path on three vertices. The two outer vertices alone behave like a pushdown as above. The middle vertex is adjacent to both pushdown vertices, and in itself, behaves like a $1$-VASS. Thus, a valence automaton over $\mathrm{\Gamma }$ is a pushdown automaton with access to one additional VASS counter, also known as one-dimensional pushdown VASS [4, 19].

In the setting of viability games, we do not need a notion of accepting run, but we need a notion of a run that is “allowed” (or “viable”), i.e. does not perform any illegal instructions. Given that a sequence $w\in {\mathrm{\Sigma }}^{\ast }$ is considered complete in valence automata if $[w]=1$, we can define $w$ (or $[w]$) as valid or viable if $w$ can be completed to $1$, i.e. if the element $[w]$ is right-invertible in $M$. Here, an element $x\in M$ is called right-invertible if there is $y\in M$ with $xy=1$. The set of right-invertible elements of $M$ is denoted $ℛ(M)$. Thus, we call an instruction (sequence) $v\in {(V\cup \overline{V})}^{\ast }$ valid (resp. invalid) in a configuration $[u]$ if $[uv]\in ℛ({𝕄}_{\mathrm{\Gamma }})$ (resp. $[uv]\notin ℛ({𝕄}_{\mathrm{\Gamma }})$).

The idea to consider right-invertible elements as valid configurations/instruction sequences has been introduced in work on first-order logic with reachability over configuration graphs of valence systems [14]. As observed there, for those concrete storage mechanisms (such as pushdowns or VASS counters) that can be represented by $\mathrm{\Gamma }$, $ℛ({𝕄}_{\mathrm{\Gamma }})$ corresponds to real configurations. For example, if $\mathrm{\Gamma }$ has no edges and thus represents a pushdown, then $ℛ({𝕄}_{\mathrm{\Gamma }})$ is the set of all $[w]$ with $w\in V^{\ast }$, which corresponds to the set of stack words over $V$, hence $ℛ({𝕄}_{\mathrm{\Gamma }})\cong V^{\ast }$. On the other hand, stack words containing a pop not preceded by a push of the same letter, e.g. $[\overline{a}]$ or $[b\overline{a}]$ where $a\ne b$, are not valid configurations. Clearly, they are not right-invertible in ${𝕄}_{\mathrm{\Gamma }}$, and thus not in $ℛ({𝕄}_{\mathrm{\Gamma }})$. If $\mathrm{\Gamma }$ is a loopless clique, then $ℛ({𝕄}_{\mathrm{\Gamma }})$ is also the set of all $[w]$ with $w\in V^{\ast }$, but since $[ab]=[ba]$ for $a,b\in V$, we have an isomorphism $ℛ({𝕄}_{\mathrm{\Gamma }})\cong {\mathbb{N}}^d$ for $d=|V|$. Hence, $ℛ({𝕄}_{\mathrm{\Gamma }})$ is the set of valid counter valuations in a $d$-VASS. Once more, for $a,b\in V$, $[\overline{a}]$ and $[b\overline{a}]$ for $a\ne b$ are not in $ℛ({𝕄}_{\mathrm{\Gamma }})$ as those are not valid configurations.

Let $\mathrm{\Gamma }$ be a graph. A valence system over $\mathrm{\Gamma }$ is a tuple $(\mathrm{\Gamma },Q,\delta ,q_{\mathrm{𝑖𝑛𝑖𝑡}})$, where $\mathrm{\Gamma }=(V,E)$ is a graph, $Q$ is a finite set of states, $\delta \subseteq Q\times {(V\cup \overline{V})}^{\ast }\times Q$ is the transition relation, and $q_{\mathrm{𝑖𝑛𝑖𝑡}}\in Q$ is its initial state. A configuration is a pair $(q,x)\in Q\times {𝕄}_{\mathrm{\Gamma }}$. We denote the set of all configurations with $\mathrm{𝖢𝗈𝗇𝖿}$. A run is a (finite or infinite) sequence of configurations $(q_0,x_0)(q_1,x_1)\mathrm{\dots }\in {\mathrm{𝖢𝗈𝗇𝖿}}^{\ast }\cup {\mathrm{𝖢𝗈𝗇𝖿}}^{\omega }$ such that for each $i$, there is a transition $(q_i,w,q_{i+1})$ in $\delta$ such that $x_{i+1}=x_i{y}_i$, where $y_i=[w]$. Thus, after applying transitions $w_1,\mathrm{\dots },w_n$, we arrive in some $(q,x)$ with $x=[w_1]\mathrm{\cdots }[w_n]=[w_1\mathrm{\cdots }{w}_n]$.

A (valence) game arena is a valence system $(\mathrm{\Gamma },Q=Q_{\exists }\bigsqcup Q_{\forall },\delta ,q_{init})$ where the set of states $Q$ are parititoned into two sets $Q_{\exists }$, the states owned by the existential (or, $\exists$-) player and $Q_{\forall }$, the states owned by the universal (or, $\forall$-) player. Moreover, in a game arena, every state has at least one outgoing transition, and for any $p,q\in Q$, there is at most one transition from $p$ to $q$. Thus, each graph $\mathrm{\Gamma }$ defines a class of valence games arenas, in the same way it defines a class of valence systems.

A play is an infinite run. A valence game $(𝙶,\text{Obj})$, is a game arena $𝙶$ with an objective $\text{Obj}\subseteq {\mathrm{𝖢𝗈𝗇𝖿}}^{\omega }$. Intuitively, $\exists$-player controls $Q_{\exists }$ and tries to satify Obj, while $\forall$-player controls $Q_{\forall }$ and tries to violate Obj. For $\iota \in \{\exists ,\forall \}$, we denote $\{\exists ,\forall \}\setminus \{\iota \}$ by $1-\iota$. An $\iota$-strategy is a map ${\sigma }_{\iota }:Q^{\ast }{Q}_{\iota }\to Q$ such that for every ${\sigma }_{\iota }(wq)=q^{\prime }$, there is a $(q,x,q^{\prime })\in \delta$. A play $(q_1,x_1)(q_2,x_2)\mathrm{\dots }$ is compliant with ${\sigma }_{\iota }$ if for every $i$ with $q_i\in Q_{\iota }$, we have ${\sigma }_{\iota }(q_1\mathrm{\dots }{q}_i)=q_{i+1}$. Note that starting from an initial configuration $(q,x)$, any state sequence $q_1{q}_2\mathrm{\dots }$ with $q_1=q$ and similarly, any two strategies ${\sigma }_{\exists }$ and ${\sigma }_{\forall }$, define a unique play because there is at most one transition between any two states. An $\iota$-strategy ${\sigma }_{\iota }$ is winning from a configuration $(q,x)$ if all plays starting from $(q,x)$ and compliant with ${\sigma }_{\iota }$ are in Obj if $\iota =\exists$, and not in Obj if $\iota =\forall$. A configuration $(q,x)$ is won by the player that has a winning strategy from $(q,x)$. If the objective is a Borel set, each configuration is won by one of the players [28].

A single graph $\mathrm{\Gamma }$ represents a specific storage mechanism, such as $2$-VASS if $\mathrm{\Gamma }$ is . Thus, understanding a decision problem for each individual $\mathrm{\Gamma }$ tells us little about the setting where part of the storage mechanism (such as the dimension of a VASS) is given in the input. Therefore, we consider the more general setting where the graph $\mathrm{\Gamma }$ is also part of the input, but drawn from some class $𝒢$. For example, if $\mathrm{\Gamma }$ is the class of unlooped cliques, then this captures the setting of $\mathrm{𝖵𝖠𝖲𝖲}$ where the dimension is arbitrary and part of the input. We will assume that $𝒢$ is closed under taking induced subgraphs.

We are ready to define viability games. Here, the fact that only valid/viable configurations should be used is part of the objective for $\exists$-player. Consider a valence game arena $(\mathrm{\Gamma },Q=Q_{\exists }\bigsqcup Q_{\forall },\delta ,q_{\mathrm{𝑖𝑛𝑖𝑡}})$. We define the objective $\text{RIO}\subseteq {\mathrm{𝖢𝗈𝗇𝖿}}^{\omega }$, short for “right-invertibility objective”, as the set of plays $(q_1,x_1)(q_2,x_2)\mathrm{\dots }$ where $x_i\in ℛ({𝕄}_{\mathrm{\Gamma }})$ for every $i\in \mathbb{N}$. In other words, the play only visits valid/viable configurations. RIO is a Borel set.

We have the following decision problems related to viability games. In the fixed initial credit setting, the initial configuration (or, credit) $[w]$ is given. For a class $𝒢$ of graphs, $\mathrm{𝖥𝖵}(𝒢)$ is the following problem:

Given:

A graph $\mathrm{\Gamma }=(V,E)$ from $𝒢$, a valence game arena over $\mathrm{\Gamma }$, and a word $w\in {(V\cup \overline{V})}^{\ast }$.

Question:

Does $\exists$-player win $(q_{\mathrm{𝑖𝑛𝑖𝑡}},[w])$ for the objective RIO?

We also have the unknown initial credit setting, where the initial configuration is to be determined. For a class $𝒢$ of graphs, $\mathrm{𝖴𝖵}(𝒢)$ is the following problem:

Given:

A graph $\mathrm{\Gamma }=(V,E)$ from $𝒢$ and a valence game arena over $\mathrm{\Gamma }$.

Question:

Is there a $w\in {(V\cup \overline{V})}^{\ast }$ such that $\exists$-player wins $(q_{\mathrm{𝑖𝑛𝑖𝑡}},[w])$ for the objective RIO?

Intuitively, the VASS dimension of $𝒢$ is the largest dimension of VASS that can be simulated using storage mechanisms over $𝒢$. A $d$-clique is a clique of $d\in \mathbb{N}$ vertices. Recall that an (un)looped $d$-clique represents $d$-dim. $\mathbb{Z}$-VASS ($d$-dim. VASS). Therefore, we denote by $\mathbb{Z}-\mathrm{𝖵𝖠𝖲𝖲}$ (resp. $\mathrm{𝖵𝖠𝖲𝖲}$) the class of looped (resp. unlooped) cliques. For a class $𝒢$ of graphs, we define its VASS dimension $\mathrm{𝖵𝖽𝗂𝗆}(𝒢)$ as the supremum over all $d$ such that some graph in $𝒢$ contains an unlooped $d$-clique as an induced subgraph.

For some graphs $\mathrm{\Gamma }$, valence systems over $\mathrm{\Gamma }$ behave like pushdown systems where the stack entries can be configurations of other storage mechanisms. Suppose a graph $\mathrm{\Gamma }=(W\cup U,E)$ is obtained from a graph $\mathrm{\Delta }=(W,E)$ by adding a set $U$ of unlooped independent (i.e. pairwise non-adjacent) vertices. Then the elements of $ℛ({𝕄}_{\mathrm{\Gamma }})$ can be written as $[w_{r+1}{u}_r{w}_r\mathrm{\cdots }{u}_1{w}_1]$, where $u_1,\mathrm{\dots },u_r\in U$ and $[w_1],\mathrm{\dots },[w_{r+1}]\in ℛ({𝕄}_{\mathrm{\Delta }})$. This can be viewed as a stack content with letters $u_1,\mathrm{\dots },u_r$, interspersed with configurations $[w_1],\mathrm{\dots },[w_{r+1}]$ corresponding to $\mathrm{\Delta }$. Then, multiplying some $w\in {(W\cup \overline{W})}^{\ast }$ will yield $[w_{r+1}{u}_r{w}_r\mathrm{\cdots }{u}_1{w}_{1}w]$, i.e. apply $w$ to the top-most entry. Multiplying some $u\in U$ will yield $[w_{r+1}{u}_r{w}_r\mathrm{\cdots }{u}_1{w}_{1}u]$ and thus start a fresh entry on top. Finally, applying $\overline{u}$ will yield a right-invertible element (i.e. be valid/viable) if and only if $u=u_1$ (i.e. we are popping the right letter) and $[w_1]=1$ (the top-most entry is empty). If that is the case, then this yields $[w_{r+1}{u}_r{w}_r\mathrm{\cdots }{u}_1{w}_1\overline{u}]=[w_{r+1}{u}_r{w}_r\mathrm{\cdots }{u}_2{w}_2]$, thus popping the entire top-most entry.

For these reasons, we denote by $\mathrm{𝖯𝖣}(𝒢)$ the class of graphs $\mathrm{\Gamma }$ as above, where $\mathrm{\Delta }$ is drawn from $𝒢$: We think of these as pushdown systems over $𝒢$. Formally, $\mathrm{𝖯𝖣}(𝒢)$ is the class of graphs $\mathrm{\Gamma }=(W\cup U,E)$ where $U$ is a set of unlooped independent vertices, and $(W,E)\in 𝒢$. We also write $\mathrm{𝖯𝖣}$ for all graphs that are just unlooped independent graphs, i.e. $(U,\mathrm{\varnothing })$.

Suppose $\mathrm{\Gamma }$ is obtained from ${\mathrm{\Delta }}_1$ and ${\mathrm{\Delta }}_2$ by taking a disjoint union of the vertices, and making any two vertices $v_1$ from ${\mathrm{\Delta }}_1$ and $v_2$ from ${\mathrm{\Delta }}_2$ adjacent. Then ${𝕄}_{\mathrm{\Gamma }}\cong {𝕄}_{{\mathrm{\Delta }}_1}\times {𝕄}_{{\mathrm{\Delta }}_2}$ and thus valence systems over $\mathrm{\Gamma }$ can be viewed as having access to both storage mechanisms ${\mathrm{\Delta }}_1$ and ${\mathrm{\Delta }}_2$, used independently. We therefore write $\mathrm{\Gamma }={\mathrm{\Delta }}_1\times {\mathrm{\Delta }}_2$, and extend this notation to classes of graphs, i.e. ${𝒢}_1\times {𝒢}_2$. For example, $\mathrm{𝖯𝖣}\times \mathrm{𝖵𝖠𝖲𝖲}$ are the graphs corresponding to pushdown vector addition systems [4, 23, 19].

If $\mathrm{\Gamma }$ has only looped vertices, then ${𝕄}_{\mathrm{\Gamma }}$ is a group, meaning for every $x\in {𝕄}_{\mathrm{\Gamma }}$, there is a $y\in {𝕄}_{\mathrm{\Gamma }}$ with $xy=1$: Indeed, for $w\in {(V\cup \overline{V})}^{\ast }$, we have $[w\overline{w}]=1$, since $\overline{a}a{\equiv }_{\mathrm{\Gamma }}a\overline{a}{\equiv }_{\mathrm{\Gamma }}\epsilon$ for any $a\in V$. Therefore, we denote by $\mathrm{𝖦𝗋𝗉}$ the class of graphs with only looped vertices. Note that for a class $𝒢$, an algorithm for $\mathrm{𝖥𝖵}(𝒢\times \mathrm{𝖦𝗋𝗉})$ or $\mathrm{𝖴𝖵}(𝒢\times \mathrm{𝖦𝗋𝗉})$ can just ignore all letters in the $\mathrm{𝖦𝗋𝗉}$ components, since they never stand in the way of right-invertibility.

We are now ready to state our main results. We first have a full description of the decidability and complexity landscape of the fixed initial credit setting:

Likewise, we have a full description of the decidability and complexity landscape of the unknown initial credit setting:

Let us briefly interpret Main Theorems A and B in terms of concrete storage mechanisms. First, note that $𝒢\subseteq \mathrm{𝖵𝖠𝖲𝖲}\times \mathrm{𝖦𝗋𝗉}$ means that $𝒢$ corresponds to VASS (up to a group component, which does not affect the game). Then, means the VASS dimension is bounded by some fixed $d\in \mathbb{N}$, while $\mathrm{𝖵𝖽𝗂𝗆}(𝒢)=\mathrm{\infty }$ means $𝒢$ corresponds to VASS of arbitrary dimension. Moreover, graphs in $\mathrm{𝖯𝖣}(\mathrm{𝖦𝗋𝗉})$ correspond to group pushdown systems (see Section 2) where the group is a graph group.

Thus, in both theorems, case (a) corresponds to fixed-dimensional VASS. In Main Theorem A, case (b) means we allow group pushdowns or fixed-dimensional VASS, and case (c) is the same as (b), except that the VASS have arbitrary dimension. In Main Theorem B, case (b) corresponds to arbitrary VASS, whereas case (c) means we have some group pushdown system, and VASS of either fixed or arbitrary dimension.

Our results show that fixed and unknown initial credit problems are decidable precisely for a class $𝒢$ included in $\mathrm{𝖯𝖣}(\mathrm{𝖦𝗋𝗉})\times \mathrm{𝖦𝗋𝗉}\cup \mathrm{𝖵𝖠𝖲𝖲}\times \mathrm{𝖦𝗋𝗉}$. Since a direct product with $\mathrm{𝖦𝗋𝗉}$ is irrelevant for $\mathrm{𝖥𝖵}$ and $\mathrm{𝖴𝖵}$, this means the interesting settings are $\mathrm{𝖯𝖣}(\mathrm{𝖦𝗋𝗉})$ and $\mathrm{𝖵𝖠𝖲𝖲}$.

Here, $\mathrm{𝖥𝖵}(\mathrm{𝖵𝖠𝖲𝖲})$ and $\mathrm{𝖴𝖵}(\mathrm{𝖵𝖠𝖲𝖲})$ are the same as multi-dimensional energy games, meaning our results reveal $\mathrm{𝖯𝖣}(\mathrm{𝖦𝗋𝗉})$ as a new class of systems with decidable games.

This new class $\mathrm{𝖯𝖣}(\mathrm{𝖦𝗋𝗉})$ includes $\mathrm{𝖯𝖣}(\mathbb{Z}-\mathrm{𝖵𝖠𝖲𝖲})$, i.e. stacks where entries contain vectors over ${\mathbb{Z}}^d$, for some $d\in \mathbb{N}$. These are part of the class of stacked counter automata [36, 38]. Having a decidable game type for $\mathrm{𝖯𝖣}(\mathbb{Z}-\mathrm{𝖵𝖠𝖲𝖲})$ is noteworthy, because these systems behave as unfavorably to classical games as $\mathrm{𝖵𝖠𝖲𝖲}$: In games where the arena ensures validity of instructions, (i) control-state reachability games, (ii) configuration reachability games, and (iii) non-termination games (where the objective is just to construct an arbitrary infinite run), are all undecidable for $\mathrm{𝖯𝖣}(\mathbb{Z}-\mathrm{𝖵𝖠𝖲𝖲})$. For (i),(ii), this was shown in [30, Thms. 19.2.1,19.2.10]. For (iii), we provide a simple proof in the full version [32].

Therefore, in $\mathrm{𝖯𝖣}(\mathrm{𝖦𝗋𝗉})$, we identify a new class of systems where the viability semantics achieves decidability.

Decidability of viability games for $\mathrm{𝖯𝖣}(\mathrm{𝖦𝗋𝗉})$ is noteworthy for another reason: In $\mathrm{𝖯𝖣}(\mathrm{𝖦𝗋𝗉})$ (beyond $\mathrm{𝖯𝖣}(\mathbb{Z}-\mathrm{𝖵𝖠𝖲𝖲})$), even ordinary (i.e. single-player) control-state reachability is undecidable. This is because the rational subset membership problem for graph groups (which is undecidable in general [25, Theorem 2]) reduces to control-state reachability in $\mathrm{𝖯𝖣}(\mathrm{𝖦𝗋𝗉})$.

Let us briefly discuss the subtle decidability border for $\mathrm{𝖥𝖵}$ and $\mathrm{𝖴𝖵}$ for graphs of the form $\mathrm{𝖯𝖣}(\text{<foreignobject style="--ltx-fo-width:1.66em;--ltx-fo-height:0.58em;--ltx-fo-depth:0em;" height="5.8pt" overflow="visible" transform="matrix(1 0 0 -1 0 8)" width="16.6pt"><span class="ltx\_foreignobject\_container"><span class="ltx\_foreignobject\_content"><img src="x5.png" id="S5.SS0.SSS0.P0.SPx7.p1.m3.g1nest" class="ltx\_graphics ltx\_img\_landscape" width="32" height="11" alt="[Uncaptioned image]" style="width: 32px; height: unset; max-width: 100\%"></span></span></foreignobject>})$, i.e. a stack of two counters, which are either $\mathbb{Z}$-VASS counters or VASS counters. If both are VASS counters, then viability games are undecidable by a similar reduction as for ordinary safety games for $2$-VASS. It turns out, the construction can be adapted if one counter is a $\mathbb{Z}$ counter, i.e. for $\mathrm{𝖯𝖣}(\text{<foreignobject style="--ltx-fo-width:1.66em;--ltx-fo-height:0.58em;--ltx-fo-depth:0em;" height="5.8pt" overflow="visible" transform="matrix(1 0 0 -1 0 8)" width="16.6pt"><span class="ltx\_foreignobject\_container"><span class="ltx\_foreignobject\_content"><img src="x6.png" id="S5.SS0.SSS0.P0.SPx7.p1.m7.g1nest" class="ltx\_graphics ltx\_img\_landscape" width="32" height="11" alt="[Uncaptioned image]" style="width: 32px; height: unset; max-width: 100\%"></span></span></foreignobject>})$. However, if both are $\mathbb{Z}$ counters, then we are in $\mathrm{𝖯𝖣}(\mathrm{𝖦𝗋𝗉})$, where viability games are decidable.

Let us begin by mentioning those graphs for which we show undecidability (both of $\mathrm{𝖥𝖵}$ and $\mathrm{𝖴𝖵}$). We call the graphs shown in Fig. 2 the illegal graphs. Note that in Fig. 2, a dotted edge means it can be present or not (and both variants are deemed illegal). We will show that for these graphs, both $\mathrm{𝖥𝖵}$ and $\mathrm{𝖴𝖵}$ are undecidable:

As apparent from Main Theorems A and B, the decidable cases are those where every graph in $𝒢$ belongs to $\mathrm{𝖯𝖣}(\mathrm{𝖦𝗋𝗉})\times \mathrm{𝖦𝗋𝗉}$ or to $\mathrm{𝖵𝖠𝖲𝖲}\times \mathrm{𝖦𝗋𝗉}$ (or both). Since in our setting, a direct product with a group will have no influence on the game (as right-invertibility is not affected), we may as well assume that the graphs belongs to $\mathrm{𝖯𝖣}(\mathrm{𝖦𝗋𝗉})\cup \mathrm{𝖵𝖠𝖲𝖲}$. For graphs in $\mathrm{𝖵𝖠𝖲𝖲}$, the problems $\mathrm{𝖥𝖵}$ and $\mathrm{𝖴𝖵}$ are just energy games with unary-encoded numbers, and thus complexity follows from existing results:

It is immediate from the definitions that the case $\mathrm{𝖵𝖽𝗂𝗆}(𝒢)=\mathrm{\infty }$ corresponds to energy games where the dimension is arbitrary (and part of the input). Here, the fixed initial credit setting $\mathrm{𝖥𝖵}$ is $\mathrm{𝟤}𝖤𝖷𝖯$-complete [22, Cor. 6.1] and the unknown initial credit setting $\mathrm{𝖴𝖵}$ is $\mathrm{𝖼𝗈𝖭𝖯}$-complete [9, Thm. 9]. Moreover, is the case of fixed dimension. Here, both settings are $𝖯$-complete, see [22, Thms. 3.3&3.5].

Now suppose $𝒢\subseteq \mathrm{𝖯𝖣}(\mathrm{𝖦𝗋𝗉})\times \mathrm{𝖦𝗋𝗉}$, or equivalently $𝒢\subseteq \mathrm{𝖯𝖣}(\mathrm{𝖦𝗋𝗉})$. Here we discover a novel decidability result: While control-state reachability games and configuration reachability games (and even ordinary control-state reachability, without games!) are undecidable, viability games are decidable for $\mathrm{𝖯𝖣}(\mathrm{𝖦𝗋𝗉})$ storage mechanisms. Moreover, we will show that both $\mathrm{𝖥𝖵}$ and $\mathrm{𝖴𝖵}$ are $\mathrm{𝖤𝖷𝖯}$-complete for this class:

Regarding hardness, note that a graph in $\mathrm{𝖯𝖣}(\mathrm{𝖦𝗋𝗉})\times \mathrm{𝖦𝗋𝗉}$ belongs to $\mathrm{𝖵𝖠𝖲𝖲}\times \mathrm{𝖦𝗋𝗉}$ if and only if it contains at most one unlooped vertex $v$, and all the unlooped vertices are adjacent to $v$. Thus, $\mathrm{\Gamma }$ does not belong to $\mathrm{𝖵𝖠𝖲𝖲}\times \mathrm{𝖦𝗋𝗉}$ if and only if $\mathrm{\Gamma }$ contains (i) two unlooped vertices or (ii) one unlooped vertex $v$ and a looped vertex $u$ that is not adjacent to $v$. In both cases, one can reduce classic pushdown (non-termination) games to $\mathrm{𝖥𝖵}(\mathrm{\Gamma })$ and $\mathrm{𝖴𝖵}(\mathrm{\Gamma })$ which is known to be $\mathrm{𝖤𝖷𝖯}$-hard [34].

The interesting part of Thm. 6.3 is the decidability and $\mathrm{𝖤𝖷𝖯}$ upper bound of $\mathrm{𝖥𝖵}$ and $\mathrm{𝖴𝖵}$. These will be shown in Sections 7 and 8.

In addition to Thms. 6.1, 6.2, and 6.3, we also need to show that every class $𝒢$ of graphs falls into one of the cases in Main Theorems A and B. This will follow from the following, which we prove in Section 10:

Our proofs contain several novel technical ingredients. First, proving undecidability in the case of (i) (Fig. 2) requires a subtle encoding of two-counter machine: Valence systems over (i) have a pushdown, where each entry contains one $\mathbb{N}$-counter and one $\mathbb{Z}$-counter. Note that such an undecidability proof is not possible if both are $\mathbb{Z}$-counters, as then we are in the $\mathrm{𝖯𝖣}(\mathbb{Z}-\mathrm{𝖵𝖠𝖲𝖲})$ setting, which is decidable.

Second, our algorithm for $\mathrm{𝖥𝖵}(\mathrm{𝖯𝖣}(\mathrm{𝖦𝗋𝗉}))$ relies on the insight that if the stack contains a group element that does not have a representation among polynomial length words, then $\forall$ can force a victory, because these elements are “too big to cancel in time”. This implies that detecting winning strategies can be confined to group elements with representations of polynomial length $\mathrm{\ell }$. However, a naive implementation of this would encode the group elements in an exponential-sized stack alphabet (resulting in a $\mathrm{𝟤}𝖤𝖷𝖯$ algorithm). Indeed, we cannot store the group elements as words on the stack: After expanding them (potentially beyond length $\mathrm{\ell }$), we need to find a new representation of length $\le \mathrm{\ell }$ (if one exists), but this requires substantial rewriting far from the ends of the word. To mitigate this, we devise an algorithm that, as in pure pushdown systems [7], saturates only sets of (sets of) control states. This yields the optimal $\mathrm{𝖤𝖷𝖯}$ algorithm.

Third, our algorithm for $\mathrm{𝖴𝖵}(\mathrm{𝖯𝖣}(\mathrm{𝖦𝗋𝗉}))$ reduces to $\mathrm{𝖥𝖵}(\mathrm{𝖯𝖣}(\mathrm{𝖦𝗋𝗉}))$. To this end, a combinatorial argument shows that initial configurations of exponential stack height (and polynomial-sized group-valued entries) always suffice. However, an additional trick is needed to allow $\exists$ to guess an exponential-sized stack without having the opportunity to grow it infinitely. We achieve this by adapting a recent technique from indexed languages [27].

Fourth, a combinatorial argument shows that all graphs that avoid the illegal graphs (Fig. 2) belong to $\mathrm{𝖵𝖠𝖲𝖲}\times \mathrm{𝖦𝗋𝗉}$ or to $\mathrm{𝖯𝖣}(\mathrm{𝖦𝗋𝗉})\times \mathrm{𝖦𝗋𝗉}$.

Note that in the literature on valence systems, complete descriptions of decidability (let alone complexity) landscapes are rare. For decidability, this has been achieved for first-order logic with reachability [14], certain underapproximations of reachability that are designed to guarantee decidability [29, 33], and games on valence system arenas [30] (but here, only trivial cases are decidable).

However, the group elements on the stack do pose a non-trivial challenge. Indeed, recall that if $\mathrm{\Gamma }\in \mathrm{𝖯𝖣}(\mathrm{𝖦𝗋𝗉})$, then an element in $ℛ({𝕄}_{\mathrm{\Gamma }})$ is of the form $[w_{r+1}{\gamma }_r{w}_r\mathrm{\cdots }{\gamma }_1{w}_1]$, where ${\gamma }_1,\mathrm{\dots },{\gamma }_r$ are from an independent, unlooped set of vertices (i.e. pushdown letters), and $w_1,\mathrm{\dots },w_{r+1}$ are over looped vertices (i.e. generators of a group). Now, if we perform a pop of $\gamma$ in this configuration, then it depends on the top-most group element $[w_1]$ (and ${\gamma }_1$) whether this leads to a valid configuration: If $[w_1]=1$ and ${\gamma }_1=\gamma$, then this will lead to the right-invertible $[w_{r+1}{\gamma }_r{w}_r\mathrm{\cdots }{\gamma }_1{w}_1]$, but if $[w_1]\ne 1$ or $\gamma \ne {\gamma }_1$, then the result is not right-invertible. Since viability games for pushdown systems can easily be reduced via classical safety games on pushdown systems, the (infinitely many) group elements on the stack constitute the main difficulty.

We may assume that the initial credit $\lambda$ is empty, since this can easily be encoded in the arena. We may also assume that there is only a single pushdown letter (aside from group elements): If there are pushdown letters $\{{\gamma }_1,\mathrm{\dots },{\gamma }_k\}$ and looped vertices $W$, then each entry ${\gamma }_{i}w$ with $w\in {(W\cup \overline{W})}^{\ast }$ in a configuration is encoded by $\gamma g^i\gamma w$, where $\gamma$ is a single fresh pushdown letter, and $g$ is an arbitrary letter in $W$. Thus, we encode one entry by two entries, the first of which encodes the specific original letter ${\gamma }_i$ used. This works because for $g\in W$, the elements $g^i$ for $i\in \mathbb{N}$ are pairwise distinct.

Details can be found in the full version [32]. Thus we assume $\mathrm{\Gamma }=(V,E)$, with $V=\{\gamma \}\cup W$, where $\gamma$ is unlooped, the vertices in $W$ are all looped, and there are no edges between $\gamma$ and $W$. Clearly, we may assume that all transitions carry either a letter in $V\cup \overline{V}$ or $\epsilon$.

Winning strategies for $\exists$ describe infinite runs, meaning it is not immediate how to represent them finitely. In contrast, winning strategies for $\forall$ have finite representations: Since a play winning for $\forall$ must visit an invalid configuration (i.e. $(q,[u])$ with $[u]\notin ℛ({𝕄}_{\mathrm{\Gamma }})$), and everything thereafter is irrelevant, we can represent the strategy in a finite tree. Therefore, our algorithm searches for a winning strategy for $\forall$.

Specifically, a $\iota$-strategy tree for $\iota \in \{\exists ,\forall \}$ is a tree with nodes in $Q\times {𝕄}_{\mathrm{\Gamma }}$, edges are labeled by $V\cup \overline{V}\cup \{\epsilon \}$, such that the following holds: If a node $(q,[u])$ has $q\in Q_{1-\iota }$, then for every transition $q\stackrel{𝑣}{\to }{q}^{\prime }$ in $\delta$, the node $(q,[u])$ has a child $(q^{\prime },[uv])$. If $q\in Q_{\iota }$, then the node has a single child $(q^{\prime },[uv])$ for some transition $q\stackrel{𝑣}{\to }{q}^{\prime }$ in $\delta$. Here, the edges are always labeled by the multiplied $v$. We call the tree winning if all branches (i.e. plays) are winning for $\iota$-player. For $\forall$-strategy trees this means each branch visits some $(q,[u])$ with $[u]\notin ℛ({𝕄}_{\mathrm{\Gamma }})$. We consider finite winning $\forall$-strategy trees where every branch has the first such $(q,[u])$ as a leaf. Our task is thus to detect winning $\forall$-strategy trees.

If we had no group elements, then detecting $\forall$-strategy trees would amount to solving a safety game on a pushdown graph. Here, a standard approach is a saturation procedure [7]. The data that is being saturated is, for each $q\in Q$, the set $R_q$ of all subsets $P\subseteq Q$ such that, roughly speaking, there is a $\forall$-strategy tree with root node $(q,[\epsilon ])$ where we allow leaves that (i) are invalid (i.e. $\notin ℛ({𝕄}_{\mathrm{\Gamma }})$), or (ii) end in an empty configuration $[\epsilon ]$, but in $P$. We call such a “relaxed winning $\forall$-strategy tree” a $P$-tree. Then clearly, $\mathrm{\varnothing }\in R_q$ if and only if there is a winning $\forall$-strategy tree rooted in $(q,[\epsilon ])$.

In the pushdown setting, $R_q$ can be computed via saturation w.r.t. the maximal stack height: Let $R_q^i$ be the set of all $P\subseteq Q$ such that there is a $(P,i)$-tree, i.e. a $P$-tree where all stack heights across branches are $\le i$. Without group elements, it is not hard to compute $R_q^{i+1}$ from $R_q^i$ via emptiness of finite-state tree automata.

The main challenge in our algorithm is to perform the above saturation in the presence of group elements. Note that very closely related tasks are already undecidable: It is undecidable (for certain $\mathrm{\Gamma }$) whether a given regular $L\subseteq {(W\cup \overline{W})}^{\ast }$ contains some $w\in {(W\cup \overline{W})}^{\ast }$ with $[w]=1$ [25, Thm. 2]. Thus, it is undecidable whether, even in the single-player setting, there is ever a valid pop.

Let us sketch how we deal with group elements, in the case of stack height $0$. The crucial observation is that group elements can be “big” or “small”. Intuitively, small elements just need polynomially many bits, whereas big elements are “too big to cancel in time” and thus do not need to be stored exactly.

Let us make this precise. With $\mathrm{\Delta }=(W,E)$, let $g\in {𝕄}_{\mathrm{\Delta }}$ be some group element. Let $\Vert g\Vert$ denote the word length of $g$, i.e. the length of the shortest word $w\in {(W\cup \overline{W})}^{\ast }$ with $g=[w]$. We say that $q\in Q$ is $0$-eligible if there exists a $\forall$-strategy tree where (i) $q$ is in the root and (ii) every branch contains a pop, and no push. Clearly, in any $(P,0)$-tree, every ocurring state must be $0$-eligible. The following observation about big elements is key:

This is because there is a tree $t$ witnessing $0$-eligibility of height at most $|Q|$: In a tree higher than $|Q|$, we can cut a repeating occurrence of a state, and still obtain a witness. However, on this witness, every branch will multiply a group element of word length at most $|Q|$. Therefore, making $(p,wg)$ the root node will yield a $(P,0)$-tree: In every branch, we multiply some element $[v]$ with $|v|\le |Q|$ to $g$, but since $\Vert g\Vert >|Q|$, we know that $g[v]\ne 1$: Otherwise we would have $g=[\overline{v}]$. Therefore, the pop in each branch must be applied with a group element $\ne 1$ and is thus invalid – the tree is a $(\mathrm{\varnothing },0)$-tree. We say $g\in {𝕄}_{\mathrm{\Delta }}$ is big if $\Vert g\Vert >|Q|$.

By Lemma 7.2, it suffices to track small elements, i.e. those with word length $\le |Q|$, of ${𝕄}_{\mathrm{\Delta }}$ exactly. We do this using a standard construction in group theory: The Cayley graph of ${𝕄}_{\mathrm{\Delta }}$, denoted $𝒞$, is the directed graph with ${𝕄}_{\mathrm{\Delta }}$ as its vertex set, and edges $g\stackrel{𝑥}{\to }{g}^{\prime }$ for each $g,g^{\prime }\in {𝕄}_{\mathrm{\Delta }}$ and $x\in W\cup \overline{W}$ with $g^{\prime }=g\cdot [x]$. Of course, $𝒞$ is infinite, but we consider a variant where all big elements are collapsed into one: We obtain the restricted Cayley graph ${𝒞}^{\le |Q|}$ by removing all big nodes and inserting a fresh “trap vertex” $c^{\mathrm{𝑡𝑟𝑎𝑝}}$: All edges that arrive in big elements in $𝒞$ are redirected into $c^{\mathrm{𝑡𝑟𝑎𝑝}}$.

We will regard ${𝒞}^{\le |Q|}$ as an automaton with exponentially many states: Note that it can be computed in $\mathrm{𝖤𝖷𝖯}$: An element $g\in {𝕄}_{\mathrm{\Delta }}$ can be represented by the length-lexicographically minimal word $u\in {(W\cup \overline{W})}^{\ast }$ with $g=[u]$. Moreover, given words $u,u^{\prime }\in {(W\cup \overline{W})}^{\ast }$, one can decide in poly-time whether $[u]=[u^{\prime }]$: This is because the groups of the form ${𝕄}_{\mathrm{\Delta }}$, also called right-angled Artin groups, embed into matrix groups (over the reals) [13, 21], for which the word problem is in logspace [24]. One can thus find a minimal representative in $\mathrm{𝖤𝖷𝖯}$.

With Lemma 7.2 and ${𝒞}^{\le |Q|}$ in hand, we can now compute $R_q^0$: Given a set $P\subseteq Q$, we construct a finite (top-down) tree automaton that, roughly speaking, accepts $(P,0)$-trees with $q$ in their root. However, it restricts nodes to $0$-eligible states, and so when in some node $s$, the element of ${𝕄}_{\mathrm{\Delta }}$ becomes big, then the automaton can “declare victory” (for $\forall$): It accepts this node as a leaf, because Lemma 7.2 tells us that this node can be completed to even a $(\mathrm{\varnothing },0)$-tree. The automaton can therefore use ${𝒞}^{\le |Q|}$ to track the group element on the current branch. This tree automaton has exponentially many states, and it accepts some tree if and only if $P\in R_q^0$. Thus, we can compute all of $R_q^0$ in $\mathrm{𝖤𝖷𝖯}$.

Once we have computed $R_q^i$ for every $q\in Q$, we compute $R_q^{i+1}$ with similar ideas. Consider a $(P,i+1)$-tree with some push of $\gamma$ in some node $\nu$ in state $q^{\prime }$ that moves the stack height from $0$ to $1$. In each branch below this push, we either (i) eventually come back to stack height $0$ and arrive in some state $p\in Q$, or (ii) encounter an invalid pop. Let $s$ be the subtree consisting of all paths until (i) or (ii) occurs. Then the set $P^{\prime }$ of all states $p$ as above, satisfies $P^{\prime }\in R_{q^{\prime }}^i$. We can therefore “shortcut” $s$: Instead of performing the $\gamma$ push, we take one subtree for each $p\in P^{\prime }$ and place it directly under $\nu$. Repeating this shortcutting will lead to a tree with stack height $0$, but with special nodes whose children are given by some $P^{\prime }\in R_{q^{\prime }}^i$ for some $q^{\prime }$. The trees of this form can now be detected by a finite tree automaton: It is constructed as in the base case, except that each $P^{\prime }\in R_{q^{\prime }}^i$ provides a new transition to simulate shortcuts. Here, we use a fact analogous to Lemma 7.2: Note that there the bound will still be $|Q|$, since the automata for eligibility for higher $i$ have exponentially many transitions, but still only $|Q|$ states.

This way, we can compute $R_q^{i+1}$ in $\mathrm{𝖤𝖷𝖯}$ (w.r.t. input size) from the sets $R_{q^{\prime }}^i$ for $q^{\prime }\in Q$. Since $R_q^i\subseteq R_q^{i+1}$ for every $q,i$, this means the overall saturation terminates in exponentially many steps, leading to an $\mathrm{𝖤𝖷𝖯}$ upper bound overall.

Our first ingredient is a combinatorial argument that shows if a viability game with $n$ states over $\mathrm{𝖯𝖣}(\mathrm{𝖦𝗋𝗉})$ is won with some initial credit $\lambda \in {(V\cup \overline{V})}^{\ast }$, then there is such a $\lambda$ where with and $\Vert \lambda \Vert \le n$.

We sketch the proof for . The bound $\Vert \lambda \Vert \le n$ uses arguments similar to Lemma 7.2. Consider a winning $\exists$-strategy tree $\tau$ from $(q_{\mathrm{𝑖𝑛𝑖𝑡}},[\lambda ])$ for $\lambda =w_{r+1}\gamma w_r\mathrm{\cdots }\gamma w_1$ with $r>2^n$. We will argue that we can cut some infix $\gamma w_i\mathrm{\cdots }\gamma w_j$ from $\lambda$.

For each branch in $\tau$, its popping depth is the maximal $s$ such that the suffix $\gamma w_s\mathrm{\cdots }\gamma w_1$ is popped during this branch. Consider the case that all branches have a popping depth $\ge 2^n$. For every $i\in [1,2^n]$, let $S_i\subseteq Q$ be the (non-empty) set of all states visited on some branch after popping the suffix $\gamma w_i\mathrm{\cdots }\gamma w_1$ for the first time. There must be $j,\mathrm{\ell }\in [1,2^n]$, , with $S_j\supseteq S_{\mathrm{\ell }}$. But then we can remove the infix $\gamma w_{\mathrm{\ell }}\mathrm{\cdots }\gamma w_{j+1}$ from $\lambda$: By reattaching subtrees whose root contains $w_{r+1}\gamma w_r\mathrm{\cdots }\gamma w_{\mathrm{\ell }+1}$ to other nodes that used to contain $w_{r+1}\gamma w_r\mathrm{\cdots }\gamma w_{j+1}$, but have the same control-state, we obtain a winning $\exists$-strategy tree for the shorter initial credit $w_{r+1}\gamma w_r\mathrm{\cdots }\gamma w_{\mathrm{\ell }+1}\cdot \gamma w_j\mathrm{\cdots }\gamma w_1$.

If there are branches with popping depth , then for $i\le s$, they contribute to $S_i$ just as above. But for $i>s$, we expand $S_i$ by a state $p$ such that this branch visits $p$ infinitely often at its lowest stack height. Then the same cut-and-reattach procedure works. $◀$

We now use Thm. 8.1 to reduce $\mathrm{𝖴𝖵}(\mathrm{𝖯𝖣}(\mathrm{𝖦𝗋𝗉}))$ to $\mathrm{𝖥𝖵}(\mathrm{𝖯𝖣}(\mathrm{𝖦𝗋𝗉}))$. Here, we construct a valence game arena ${𝙶}^{\mathrm{𝚐𝚞𝚎𝚜𝚜}}$ where $\exists$ first guesses an initial credit $\lambda$ with and $\Vert \lambda \Vert \le n$, and then simulates the game. Here, the difficulty is to guess a stack content with exponentially many entries without allowing $\exists$ to win outright by just growing and growing the stack.

To this end, we modify a construction from [27, Section 9]: The idea is to not only guess a stack with entries, but a stack with decorated letters. Then, each time $\exists$ pushes a pushdown letter, $\forall$ can check whether the stack still has entries. But in fact, $\forall$ checks that the decoration adheres to a pattern that implies length . This pattern is a suffix-closed set of words that can be recognized by running linearly many DFAs in parallel. Let ${\gamma }_{[i,j]}$ to denote the set $\{{\gamma }_k\mid k\in [i,j]\}$.

See Fig. 4 for an illustration of $D_i$. Intuitively, $D_i$ accepts all words where between any two ${\gamma }_i$’s, there is at least one occurrence of ${\gamma }_{[1,i-1]}$. Thus, a word in the intersection can have at most one ${\gamma }_1$, at most two ${\gamma }_2$’s, etc. and at most $2^{i-1}$-many ${\gamma }_i$’s. Thus, the unique longest word in the intersection has length ${\mathrm{\Sigma }}_{i\in [1,m]}{2}^{i-1}=2^m-1$ and is a palindrome.

With Thms. 8.1 and 8.2, we are prepared to present the reduction. To this end, we construct the game ${𝙶}^{\mathrm{𝚐𝚞𝚎𝚜𝚜}}$, which is given in Fig. 3. First, $\exists$ collects an initial credit ${\lambda }^{\prime }$ in the loop $p_0-p_n$ before entering $𝙶[\gamma \leftarrow {\gamma }_{[1,n]}]$: the arena $𝙶$ where every push/pop is replaced by $n$-many pushes/pops, one for every ${\gamma }_i\in {\gamma }_{[1,n]}$. Say $\exists$ wins the game from $(q_{\mathrm{𝑖𝑛𝑖𝑡}},\lambda )$ for some $\lambda =[w_{r+1}\gamma \mathrm{\cdots }\gamma w_1]$ that obeys Thm. 8.1. She collects $\lambda$ before entering $𝙶[{\gamma }_i\leftarrow {\gamma }_{[1,n]}]$ with one caveat: she collects ${\lambda }^{\prime }=[w_{r+1}{\gamma }^r\mathrm{\cdots }{\gamma }^1{w}_1]$ such that the push-sequence ${\gamma }^r\mathrm{\cdots }{\gamma }^1$ of ${\lambda }^{\prime }$ is the $r$-length suffix of the $(2^n-1)$-length word $w_{\cap }$ accepted by ${\cap }_{[1,n]}L(D_i)$. Clearly, $\exists$ wins $(q_{\mathrm{𝑖𝑛𝑖𝑡}},\lambda )$ iff she wins on $(𝙶[\gamma \leftarrow {\gamma }_{[1,n]}]$ from ${\lambda }^{\prime }$.