pages test.pgpages

# The Complexity of Bidirected Reachability in Valence Systems

Moses Ganardi  0000-0002-0775-7781 Max Planck Institute for
Software Systems (MPI-SWS)KaiserslauternGermany ,  Rupak Majumdar
0000-0003-2136-0542 Max Planck Institute for
Software Systems (MPI-SWS)KaiserslauternGermany and  Georg Zetzsche
0000-0002-6421-4388 Max Planck Institute for
Software Systems (MPI-SWS)KaiserslauternGermany

(2022)

###### Abstract.

Reachability problems in infinite-state systems are often subject to extremely
high complexity. This motivates the investigation of efficient
overapproximations, where we add transitions to obtain a system in which
reachability can be decided more efficiently. We consider _bidirected_
infinite-state systems, where for every transition there is a transition with
opposite effect.

We study bidirected reachability in the framework of valence systems, an
abstract model featuring finitely many control states and an infinite-state
storage that is specified by a finite graph. By picking suitable graphs,
valence systems can uniformly model counters as in vector addition systems,
pushdowns, integer counters, and combinations thereof.

We provide a comprehensive complexity landscape for bidirected reachability
and show that the complexity drops (often to polynomial time) from that of
general reachability, for almost every storage mechanism where reachability is
known to be decidable.

Reachability, complexity, infinite-state systems, bidirected, reversible,
vector addition systems, pushdown, counters

††ccs: Theory of computation Models of computation††ccs: Theory of computation
Formal languages and automata theory††ccs: Theory of computation Computational
complexity and cryptography††journalyear: 2022††copyright:
rightsretained††conference: 37th Annual ACM/IEEE Symposium on Logic in
Computer Science (LICS); August 2–5, 2022; Haifa, Israel††booktitle: 37th
Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) (LICS ’22),
August 2–5, 2022, Haifa, Israel††doi: 10.1145/3531130.3533345††isbn:
978-1-4503-9351-5/22/08

##  1\. Introduction

The reachability problem is one of the most fundamental tasks for infinite-
state systems: It asks for a given infinite-state system and two
configurations $c_{1}$ and $c_{2}$, whether it is possible to reach $c_{2}$
from $c_{1}$. It is a basic component in many types of verification (both for
safety and liveness), and has been studied intensively for decades.
Unfortunately, the reachability problem often exhibits prohibitively high
complexity or is subject to long-standing open problems: In _vector addition
systems with states_ (VASS), which are systems with counters over the natural
numbers that can be incremented and decremented, reachability is Ackermann-
complete (DBLP:conf/focs/Leroux21, 21, 10). Furthermore, if we allow a
pushdown in addition to the counters, we obtain _pushdown vector addition
systems_ (PVASS), for which decidability of the reachability problem is a
long-standing open problem (DBLP:conf/icalp/LerouxST15, 22).

One way to circumvent this is to consider overapproximations of the
reachability problem: Instead of deciding reachability in the original system,
we decide reachability in a system that has more transitions. Then, a negative
answer still certifies safety. A promising overapproximation is _bidirected
reachability_ : We assume that in our system, for each transition, there is
another with opposite effect. For example, in pushdown reachability, a push of
a symbol on the forward edge is reverted by the pop of the symbol on the
backward edge. In a vector addition system, incrementing a counter is reverted
by decrementing it by the same amount. In addition to its theoretical
interest, bidirected reachability is also of practical interest: for example,
several program analysis problems can be formulated or practically
approximated as bidirected pushdown reachability (ChatterjeeCP2018, 7, 48) or
bidirected interleaved pushdown reachability (DBLP:conf/ecoop/XuRS09, 39, 40,
47, 23, 24, 18). A remarkable recent result is that bidirected reachability in
PVASS with one counter is decidable (DBLP:journals/pacmpl/KP22, 18).

An important measure for the utility of bidirectedness is: _Does
bidirectedness reduce complexity?_ It is known that bidirected reachability in
VASS is $\mathsf{EXPSPACE}$-complete and in logarithmic space for a fixed
number of counters (MAYR1982305, 31). Bidirected pushdown reachability can be
solved in almost linear time (ChatterjeeCP2018, 7) whereas a truly subcubic
algorithm for pushdown reachability is a long-standing open problem
(Chaudhuri, 8). However, the general complexity landscape is far from
understood. For example, it is hitherto not even known if bidirected pushdown
reachability is $\mathsf{P}$-hard. Further, it is not known whether bidirected
reachability in $\mathbb{Z}$-VASS (which allow counter values to become
negative) is $\mathsf{NP}$-complete as for reachability
(DBLP:conf/rp/HaaseH14, 14).

### Valence systems

In this paper, we systematically compare the complexity of bidirected
reachability with general reachability. To this end, we use the framework of
_valence systems over graph monoids_ (DBLP:journals/eatcs/Zetzsche16, 43, 42,
46, 44), which are an abstract model that features finitely many control
states and an infinite storage specified by a finite graph (with self-loops
allowed). By picking a suitable graph, one can obtain classical infinite-state
models: A clique of $d$ unlooped nodes corresponds to VASS with $d$ counters.
If the vertices are looped, one obtains $\mathbb{Z}$-VASS. Two isolated
unlooped vertices yield pushdown systems.

In order to compare bidirected with general reachability, we focus on storage
mechanisms where general reachability is known to be decidable. These
mechanisms correspond to a well-understood class of graphs studied in
(DBLP:journals/iandc/Zetzsche21, 46). The latter work characterizes a class of
graphs that precisely capture PVASS with one counter. Then, it is shown in
(DBLP:journals/iandc/Zetzsche21, 46) that for every graph that avoids these
PVASS graphs as induced subgraphs, reachability is decidable iff the graph is
a transitive forest. This class of graphs is called $\mathsf{SC}^{\pm}$.

### Contribution

We provide a comprehensive complexity landscape for bidirected reachability
for valence systems over graphs in $\mathsf{SC}^{\pm}$. For every graph in
$\mathsf{SC}^{\pm}$, we prove that bidirected reachability is either
$\mathsf{L}$-complete or $\mathsf{P}$-complete. More generally, we consider
the setting where the graph is part of the input and drawn from a class
$\mathcal{G}\subseteq\mathsf{SC}^{\pm}$: This is the case, e.g. when the input
can consist of $\mathbb{Z}$-VASS with an arbitrary number of counters. Even in
this general setting, we obtain an almost complete complexity picture: Then,
bidirected reachability falls within five possible categories:
$\mathsf{L}$-complete, $\mathsf{ILD}$-complete, $\mathsf{P}$-complete, in
$\mathsf{EXP}$, or $\mathsf{EXPSPACE}$-complete. Here, the complexity class
$\mathsf{ILD}$ captures those problems that are logspace-reducible to the
feasibility problem for integer linear Diophantine equations (it lies between
$\mathsf{L}$ and $\mathsf{P}$).

To obtain the $\mathsf{P}$-hardness, we exploit a connection to algorithmic
group theory, which allows us to reduce from the subgroup membership problem
for free groups (avenhaus1984nielsen, 3). The same connection yields
undecidability of bidirected reachability if the graph has an induced 4-cycle
via a well-known group theoretic undecidability due to Mikhailova
(mikhailova1966occurrence, 33). In particular, bidirected reachability is
undecidable in systems with two pushdowns, which answers an open problem from
(DBLP:journals/pacmpl/LiZR21, 24)111This problem was answered independently in
(DBLP:journals/pacmpl/KP22, 18).. This connection also yields an example of a
graph where reachability is _undecidable_ , but bidirected reachability is
_decidable_. Finally, we can translate back to group theory: Our results imply
that the subgroup membership problem in graph groups over any transitive
forest is in $\mathsf{P}$.

Our results show that the complexity drops for almost every storage (pure
pushdowns without any additional counters are the only exceptions). For
example, reachability for $\mathbb{Z}$-VASS and for pushdown $\mathbb{Z}$-VASS
(which have a pushdown and several $\mathbb{Z}$-valued counters) are both
known to be $\mathsf{NP}$-complete (DBLP:conf/rp/HaaseH14, 14, 16), but we
place bidirected reachability in $\mathsf{P}$. The same holds for
$\mathbb{Z}$-VASS that, in addition, have a fixed number of
$\mathbb{N}$-counters. Our results also apply to stacks where each entry
contains several counter values. Moreover, in addition to such stacks, one can
have $\mathbb{Z}$-counters, then build stacks of such configurations, etc. Our
characterization implies that when the number of alternations between building
stacks and adding $\mathbb{Z}$-counters is not fixed, then bidirected
reachability can still be solved in $\mathsf{EXP}$; in contrast, general
reachability is $\mathsf{NEXP}$-complete (HaaseZetzsche2019, 15).

### Key techniques

These lower complexities are achieved using novel techniques. The
aforementioned connection to algorithmic group theory is the logspace inter-
reducibility with the subgroup membership problem if the storage graph has
self-loops everywhere. This connection between bidirected automata and
subgroups has been observed in (lohrey2010automata, 27); we provide logspace
reductions.

While the connection to group theory is used for lower bounds, our upper
bounds also require new methods. The decidability for reachability in
$\mathsf{SC}^{\pm}$ in (DBLP:journals/iandc/Zetzsche21, 46) employs VASS with
nested zero tests (reinhardt2008reachability, 35, 5), which we manage to avoid
completely. Instead, we rely on results about bidirected VASS reachability
sets (DBLP:conf/fct/KoppenhagenM97, 19) to essentially eliminate
$\mathbb{N}$-counters in our systems first. However, the main innovation is a
modified approach to reachability in systems with stacks and
$\mathbb{Z}$-counters (HaaseZetzsche2019, 15, 16). Those algorithms use a
technique of (DBLP:conf/cade/VermaSS05, 37), which constructs, given a
context-free grammar, an existential Presburger formula for its Parikh image.
While existential Presburger arithmetic is equivalent to systems of integer
linear _inequalities_ (where feasibility is $\mathsf{NP}$-complete), we show
that for the new notion of _bidirected grammars_ , the Parikh image can, in
some appropriate sense, be described using only _equations_. This leads to a
$\mathsf{P}$ upper bound, since feasibility of systems of integer linear
equations is in $\mathsf{P}$ (DBLP:journals/siamcomp/ChouC82, 9).

###### Acknowledgements.

The authors are grateful to Markus Lohrey for discussions about the algorithm
in (lohrey2010automata, 27). This work was sponsered in part by the Sponsor
DFG https://www.dfg.de/ under project Grant #389792660 TRR 248–CPEC.

##  2\. Bidirected Valence Systems

### Algebraic Preliminaries

We assume familiarity with basic notions of monoids, groups, etc. (Lang, 20).
A _subgroup_ of a group $G$ is a subset of the elements of $G$ that themselves
form a group; i.e., it is a subset of elements closed under the binary
operation as well as inverses. A subgroup $H$ of a group $G$ can be used to
decompose the underlying set of $G$ into disjoint equal-size subsets called
_cosets_. The _left cosets_ (resp.  _right cosets_) of $H$ in $G$ are the sets
obtained by multiplying each element of $H$ by a fixed element $g$ of $G$:
$gH=\\{g\cdot h\mid h\in H\\}$ (resp. $Hg=\\{h\cdot g\mid h\in H\\}$). For a
subset $S$, we write $\langle S\rangle$ for the smallest subgroup containing
$S$; this is the set of all elements of $G$ that can be written as finite
products of elements from $S$ and their inverses. If $\langle S\rangle=G$, we
say $S$ _generates_ $G$ and call the elements of $S$ the _generators_ of $G$.

A _presentation_ $(\Sigma\mid R)$ of a monoid is a description of a monoid in
terms of a set $\Sigma$ of generators and a set of binary relations
$R\subseteq\Sigma^{*}\times\Sigma^{*}$ on the free monoid $\Sigma^{*}$
generated by $\Sigma$. For a set $R\subseteq\Sigma^{*}\times\Sigma^{*}$ define
the step relation $\to_{R}$ by $sut\to_{R}svt$ for all $(u,v)\in R$ and
$s,t\in\Sigma^{*}$. Define $\equiv_{R}$ to be the smallest equivalence
relation containing $\to_{R}$. Then $\equiv_{R}$ is a _congruence_ , meaning
that if $u\equiv_{R}v$, then $sut\equiv_{R}svt$ for every $s,t\in\Sigma^{*}$.
The monoid is then presented as the quotient of $\Sigma^{*}$ by the congruence
$\equiv_{R}$. For a word $w\in\Sigma^{*}$, we write $[w]_{\equiv_{R}}$ for the
equivalence class of $w$ under $\equiv_{R}$. A commutative semigroup
presentation is a presentation $(\Sigma\mid R)$ where $(xy,yx)\in R$ for all
$x\neq y\in\Sigma$. The word problem for commutative semigroups asks, given a
commutative semigroup presentation $(\Sigma\mid R)$ and two words
$u,v\in\Sigma^{*}$, does $u\equiv_{R}v$ hold? This problem is known to be
$\mathsf{EXPSPACE}$-complete (MAYR1982305, 31).

### Graph Monoids

A _graph_ is a tuple $\Gamma=(V,I)$, where $V$ is a finite set of vertices and
$I\subseteq\\{e\subseteq V\mid 1\leq|e|\leq 2\\}$ is a finite set of
undirected edges, which can be self-loops. Thus, if $\\{v\\}\in I$, we say
that $v$ is _looped_ ; otherwise, $v$ is _unlooped_. If all nodes of $\Gamma$
are (un)looped, we call $\Gamma$ _(un)looped_. By $\Gamma^{\circ}$ and
$\Gamma^{-}$, we denote the graph obtained from $\Gamma$ by adding (removing)
self-loops on all vertices. The edge relation is also called an _independence
relation_. We also write $uIv$ for $\\{u,v\\}\in I$. A subset $U\subseteq V$
is a _clique_ if $uIv$ for any two distinct $u,v\in U$. We say that
$U\subseteq V$ is an _anti-clique_ if we do not have $uIv$ for any distinct
$u,v\in U$. Given a graph $\Gamma$, we define a monoid as follows. We define
the alphabet $X_{\Gamma}=V\cup\bar{V}$ where $\bar{V}=\\{\bar{v}\mid v\in
V\\}$. We define $R_{\Gamma}=\\{(v\bar{v},\varepsilon)\mid v\in
V\\}\cup\\{(xy,yx)\mid x\in\\{u,\bar{u}\\},\,y\in\\{v,\bar{v}\\},\,uIv\\}$. We
write $\to_{\Gamma}$ instead of $\to_{R_{\Gamma}}$ and $\equiv_{\Gamma}$ for
the smallest equivalence relation containing $\to_{\Gamma}$. As observed
above, $\equiv_{\Gamma}$ is a congruence. In particular, if $v$ has a self-
loop, then $\bar{v}v\equiv_{\Gamma}\varepsilon$. We define the monoid
$\mathbb{M}\Gamma:=X_{\Gamma}^{*}/\equiv_{\Gamma}$. We write $[w]$ for the
equivalence class of $w$ under $\equiv_{\Gamma}$ and $1$ for $[\varepsilon]$.
For each word $w\in X_{\Gamma}^{*}$, we define its _inverse_ $\bar{w}$ as
follows. If $w=v$ for some $v\in V$, then $\bar{w}$ is the letter $\bar{v}$.
If $w=\bar{v}$ for $v\in V$, then $\bar{w}=v$. Finally, if $w=w_{1}\cdots
w_{n}$ with $w_{1},\ldots,w_{n}\in X_{\Gamma}$, then
$\bar{w}=\bar{w}_{n}\cdots\bar{w}_{1}$. It is known that
$w\equiv_{\Gamma}\varepsilon$ is witnessed by a derivation
$w=w_{0}\to_{\Gamma}w_{1}\to_{\Gamma}\dots\to_{\Gamma}w_{n}=\varepsilon$
(Zetzsche2016c, 42, Equation (8.2)).

### Valence systems and reachability

Valence systems are an abstract model for studying finite-state transition
systems with “storage”. They consist of a state transition system on a finite
set of states, as well as a monoid that represents an auxiliary storage and
determines which paths in the automata form valid computations in the presence
of the auxiliary storage. For example, if the underlying storage is a stack,
the monoid can encode push and pops and determine computations that produce an
empty stack.

In this work, we only consider graph monoids as the underlying monoids. Many
classes of infinite-state systems involving combinations of stacks and
counters can be modeled as valence systems over graph monoids; see
(Zetzsche2016c, 42) for detailed examples. They have been studied in terms of
expressiveness (BuckheisterZetzsche2013a, 6, 45), computing downward closures
(Zetzsche2015a, 41), and various forms of reachability problems
(DOsualdoMeyerZetzsche2016a, 11, 32, 36, 46), see (DBLP:conf/rp/Zetzsche21,
44) for a survey on the latter.

A _valence system_ $\mathcal{A}$ over a graph $\Gamma$ consists of a finite
set of states $Q$, and a finite transition relation $\rightarrow\subseteq
Q\times X_{\Gamma}^{*}\times Q$. We also write a transition $(p,u,q)$ as
$p\mathrel{\mathop{\rightarrow}\limits^{\vbox
to0.0pt{\kern-2.0pt\hbox{$\scriptstyle u$}\vss}}}q$. A run is a sequence
$(q_{0},u_{1},q_{1})(q_{1},u_{2},q_{2})\dots(q_{n-1},u_{n},q_{n})$ of
transitions, also abbreviated
$q_{0}\mathrel{\mathop{\rightarrow}\limits^{\vbox
to0.0pt{\kern-2.0pt\hbox{$\scriptstyle u$}\vss}}}q_{n}$ if $u=u_{1}\cdots
u_{n}$.

The _reachability problem_ ($\mathsf{REACH}$) for valence systems is the
following:

Given:

A valence system $\mathcal{A}$ and states $s,t$ in $\mathcal{A}$.

Question:

Is there a run $s\mathrel{\mathop{\rightarrow}\limits^{\vbox
to0.0pt{\kern-2.0pt\hbox{$\scriptstyle w$}\vss}}}t$ for some $w\in
X_{\Gamma}^{*}$ with $[w]=1$?

If the reachability problem is restricted to valence systems over a particular
graph $\Gamma$, then we denote the problem by $\mathsf{REACH}(\Gamma)$. If we
restrict the input systems to a class $\mathcal{G}$ of graphs, then we write
$\mathsf{REACH}(\mathcal{G})$. For example, if $\mathcal{V}$ is the class of
all unlooped cliques, then $\mathsf{REACH}(\mathcal{V})$ is the reachability
problem for vector addition systems with states (VASS).

A valence system $\mathcal{A}$ is _bidirected_ if for any transition
$p\mathrel{\mathop{\rightarrow}\limits^{\vbox
to0.0pt{\kern-2.0pt\hbox{$\scriptstyle w$}\vss}}}q$, we also have
$q\mathrel{\mathop{\rightarrow}\limits^{\vbox
to0.0pt{\kern-2.0pt\hbox{$\scriptstyle\bar{w}$}\vss}}}p$. The _bidirected
reachability problem_ ($\mathsf{BIREACH}$) is the reachability problem where
$\mathcal{A}$ is restricted to bidirected valence systems. As above, we
consider the case where the system is over a particular graph $\Gamma$,
denoted $\mathsf{BIREACH}(\Gamma)$, or where the graph is drawn from a class
$\mathcal{G}$, denoted $\mathsf{BIREACH}(\mathcal{G})$.

###  2.1. Decidability Landscape for Reachability

### PVASS-graphs

A graph $\Gamma$ is a _PVASS-graph_ if it is isomorphic to one of the
following three graphs:

$\displaystyle\begin{aligned} \leavevmode\hbox to63.57pt{\vbox
to6.67pt{\pgfpicture\makeatletter\hbox{\hskip 3.33301pt\lower-3.33301pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{{}}{}{{}}{}{{{}}{}{}{}{}{}{}{}{}}{{}}{}{{}}{}{{{}}{}{}{}{}{}{}{}{}}{{}}{}{{}}{}{{{}}{}{}{}{}{}{}{}{}}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@moveto{2.0pt}{0.0pt}\pgfsys@curveto{2.0pt}{1.10458pt}{1.10458pt}{2.0pt}{0.0pt}{2.0pt}\pgfsys@curveto{-1.10458pt}{2.0pt}{-2.0pt}{1.10458pt}{-2.0pt}{0.0pt}\pgfsys@curveto{-2.0pt}{-1.10458pt}{-1.10458pt}{-2.0pt}{0.0pt}{-2.0pt}\pgfsys@curveto{1.10458pt}{-2.0pt}{2.0pt}{-1.10458pt}{2.0pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@moveto{28.45276pt}{0.0pt}\pgfsys@moveto{30.45276pt}{0.0pt}\pgfsys@curveto{30.45276pt}{1.10458pt}{29.55734pt}{2.0pt}{28.45276pt}{2.0pt}\pgfsys@curveto{27.34818pt}{2.0pt}{26.45276pt}{1.10458pt}{26.45276pt}{0.0pt}\pgfsys@curveto{26.45276pt}{-1.10458pt}{27.34818pt}{-2.0pt}{28.45276pt}{-2.0pt}\pgfsys@curveto{29.55734pt}{-2.0pt}{30.45276pt}{-1.10458pt}{30.45276pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{28.45276pt}{0.0pt}\pgfsys@moveto{56.90552pt}{0.0pt}\pgfsys@moveto{58.90552pt}{0.0pt}\pgfsys@curveto{58.90552pt}{1.10458pt}{58.0101pt}{2.0pt}{56.90552pt}{2.0pt}\pgfsys@curveto{55.80093pt}{2.0pt}{54.90552pt}{1.10458pt}{54.90552pt}{0.0pt}\pgfsys@curveto{54.90552pt}{-1.10458pt}{55.80093pt}{-2.0pt}{56.90552pt}{-2.0pt}\pgfsys@curveto{58.0101pt}{-2.0pt}{58.90552pt}{-1.10458pt}{58.90552pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{56.90552pt}{0.0pt}\pgfsys@fill\pgfsys@invoke{
}\hbox{\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{
{}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{
{}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{28.45276pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{
{}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{56.90552pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{}{{}}{}{
{}{}{}} {}{}{ {}{}{}}
{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{28.45276pt}{0.0pt}\pgfsys@lineto{56.90552pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}&&\leavevmode\hbox
to63.57pt{\vbox to9.53pt{\pgfpicture\makeatletter\hbox{\hskip
3.33301pt\lower-3.33301pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{{}}{}{{}}{}{{{}}{}{}{}{}{}{}{}{}}{{}}{}{{}}{}{{{}}{}{}{}{}{}{}{}{}}{{}}{}{{}}{}{{{}}{}{}{}{}{}{}{}{}}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@moveto{2.0pt}{0.0pt}\pgfsys@curveto{2.0pt}{1.10458pt}{1.10458pt}{2.0pt}{0.0pt}{2.0pt}\pgfsys@curveto{-1.10458pt}{2.0pt}{-2.0pt}{1.10458pt}{-2.0pt}{0.0pt}\pgfsys@curveto{-2.0pt}{-1.10458pt}{-1.10458pt}{-2.0pt}{0.0pt}{-2.0pt}\pgfsys@curveto{1.10458pt}{-2.0pt}{2.0pt}{-1.10458pt}{2.0pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@moveto{28.45276pt}{0.0pt}\pgfsys@moveto{30.45276pt}{0.0pt}\pgfsys@curveto{30.45276pt}{1.10458pt}{29.55734pt}{2.0pt}{28.45276pt}{2.0pt}\pgfsys@curveto{27.34818pt}{2.0pt}{26.45276pt}{1.10458pt}{26.45276pt}{0.0pt}\pgfsys@curveto{26.45276pt}{-1.10458pt}{27.34818pt}{-2.0pt}{28.45276pt}{-2.0pt}\pgfsys@curveto{29.55734pt}{-2.0pt}{30.45276pt}{-1.10458pt}{30.45276pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{28.45276pt}{0.0pt}\pgfsys@moveto{56.90552pt}{0.0pt}\pgfsys@moveto{58.90552pt}{0.0pt}\pgfsys@curveto{58.90552pt}{1.10458pt}{58.0101pt}{2.0pt}{56.90552pt}{2.0pt}\pgfsys@curveto{55.80093pt}{2.0pt}{54.90552pt}{1.10458pt}{54.90552pt}{0.0pt}\pgfsys@curveto{54.90552pt}{-1.10458pt}{55.80093pt}{-2.0pt}{56.90552pt}{-2.0pt}\pgfsys@curveto{58.0101pt}{-2.0pt}{58.90552pt}{-1.10458pt}{58.90552pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{56.90552pt}{0.0pt}\pgfsys@fill\pgfsys@invoke{
}\hbox{\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{
{}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{
{}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{28.45276pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{
{}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{56.90552pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{}{{}}{}{
{}{}{}} {}{}{ {}{}{}}
{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{28.45276pt}{0.0pt}\pgfsys@lineto{56.90552pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
} {
{}{}{}}{}{{}}{}{{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@moveto{0.0pt}{3.0pt}\pgfsys@moveto{3.0pt}{3.0pt}\pgfsys@curveto{3.0pt}{4.65688pt}{1.65688pt}{6.0pt}{0.0pt}{6.0pt}\pgfsys@curveto{-1.65688pt}{6.0pt}{-3.0pt}{4.65688pt}{-3.0pt}{3.0pt}\pgfsys@curveto{-3.0pt}{1.34312pt}{-1.65688pt}{0.0pt}{0.0pt}{0.0pt}\pgfsys@curveto{1.65688pt}{0.0pt}{3.0pt}{1.34312pt}{3.0pt}{3.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{3.0pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}&&\leavevmode\hbox
to63.57pt{\vbox to9.53pt{\pgfpicture\makeatletter\hbox{\hskip
3.33301pt\lower-3.33301pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{{}}{}{{}}{}{{{}}{}{}{}{}{}{}{}{}}{{}}{}{{}}{}{{{}}{}{}{}{}{}{}{}{}}{{}}{}{{}}{}{{{}}{}{}{}{}{}{}{}{}}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@moveto{2.0pt}{0.0pt}\pgfsys@curveto{2.0pt}{1.10458pt}{1.10458pt}{2.0pt}{0.0pt}{2.0pt}\pgfsys@curveto{-1.10458pt}{2.0pt}{-2.0pt}{1.10458pt}{-2.0pt}{0.0pt}\pgfsys@curveto{-2.0pt}{-1.10458pt}{-1.10458pt}{-2.0pt}{0.0pt}{-2.0pt}\pgfsys@curveto{1.10458pt}{-2.0pt}{2.0pt}{-1.10458pt}{2.0pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@moveto{28.45276pt}{0.0pt}\pgfsys@moveto{30.45276pt}{0.0pt}\pgfsys@curveto{30.45276pt}{1.10458pt}{29.55734pt}{2.0pt}{28.45276pt}{2.0pt}\pgfsys@curveto{27.34818pt}{2.0pt}{26.45276pt}{1.10458pt}{26.45276pt}{0.0pt}\pgfsys@curveto{26.45276pt}{-1.10458pt}{27.34818pt}{-2.0pt}{28.45276pt}{-2.0pt}\pgfsys@curveto{29.55734pt}{-2.0pt}{30.45276pt}{-1.10458pt}{30.45276pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{28.45276pt}{0.0pt}\pgfsys@moveto{56.90552pt}{0.0pt}\pgfsys@moveto{58.90552pt}{0.0pt}\pgfsys@curveto{58.90552pt}{1.10458pt}{58.0101pt}{2.0pt}{56.90552pt}{2.0pt}\pgfsys@curveto{55.80093pt}{2.0pt}{54.90552pt}{1.10458pt}{54.90552pt}{0.0pt}\pgfsys@curveto{54.90552pt}{-1.10458pt}{55.80093pt}{-2.0pt}{56.90552pt}{-2.0pt}\pgfsys@curveto{58.0101pt}{-2.0pt}{58.90552pt}{-1.10458pt}{58.90552pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{56.90552pt}{0.0pt}\pgfsys@fill\pgfsys@invoke{
}\hbox{\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{
{}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{
{}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{28.45276pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{
{}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{56.90552pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{}{{}}{}{
{}{}{}} {}{}{ {}{}{}}
{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{28.45276pt}{0.0pt}\pgfsys@lineto{56.90552pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
} {
{}{}{}}{}{{}}{}{{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@moveto{0.0pt}{3.0pt}\pgfsys@moveto{3.0pt}{3.0pt}\pgfsys@curveto{3.0pt}{4.65688pt}{1.65688pt}{6.0pt}{0.0pt}{6.0pt}\pgfsys@curveto{-1.65688pt}{6.0pt}{-3.0pt}{4.65688pt}{-3.0pt}{3.0pt}\pgfsys@curveto{-3.0pt}{1.34312pt}{-1.65688pt}{0.0pt}{0.0pt}{0.0pt}\pgfsys@curveto{1.65688pt}{0.0pt}{3.0pt}{1.34312pt}{3.0pt}{3.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{3.0pt}\pgfsys@stroke\pgfsys@invoke{
} {
{}{}{}}{}{{}}{}{{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}{}\pgfsys@moveto{56.90552pt}{0.0pt}\pgfsys@moveto{56.90552pt}{3.0pt}\pgfsys@moveto{59.90552pt}{3.0pt}\pgfsys@curveto{59.90552pt}{4.65688pt}{58.5624pt}{6.0pt}{56.90552pt}{6.0pt}\pgfsys@curveto{55.24864pt}{6.0pt}{53.90552pt}{4.65688pt}{53.90552pt}{3.0pt}\pgfsys@curveto{53.90552pt}{1.34312pt}{55.24864pt}{0.0pt}{56.90552pt}{0.0pt}\pgfsys@curveto{58.5624pt}{0.0pt}{59.90552pt}{1.34312pt}{59.90552pt}{3.0pt}\pgfsys@closepath\pgfsys@moveto{56.90552pt}{3.0pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\end{aligned}$

We say that a graph is _PVASS-free_ if it has no PVASS-graph as an induced
subgraph. Here, a graph $\Gamma^{\prime}=(V^{\prime},I^{\prime})$ is an
_induced subgraph_ of $\Gamma=(V,I)$ if there is an injective map $\iota\colon
V^{\prime}\to V$ with $\\{\iota(u),\iota(v)\\}\in I$ iff $\\{u,v\\}\in
I^{\prime}$ for $u,v\in V^{\prime}$. Observe that a graph $\Gamma$ is PVASS-
free if and only if in the neighborhood of each unlooped vertex, any two
vertices are adjacent. The terminology stems from the fact that if $\Gamma$ is
a PVASS-graph, then $\mathsf{REACH}(\Gamma)$ is inter-reducible with
reachability for PVASS with one counter (DBLP:journals/iandc/Zetzsche21, 46).
Whether reachability is decidable for these is a long-standing open problem
(DBLP:conf/icalp/LerouxST15, 22) (however, bidirected reachability is
decidable (DBLP:journals/pacmpl/KP22, 18)).

### Transitive forests

A graph $\Gamma$ is a _transitive forest_ if it can be built as follows.
First, the empty graph is a transitive forest. Moreover, if $\Gamma_{1}$ and
$\Gamma_{2}$ are transitive forests, then (i) the disjoint union of
$\Gamma_{1}$ and $\Gamma_{2}$ is a transitive forest and (ii) if $\Gamma$ is
the graph obtained by adding one looped or unlooped vertex $v$ to $\Gamma_{1}$
so that $v$ is adjacent to every vertex in $\Gamma_{1}$, then $\Gamma$ is also
a transitive forest.

The complexity of our algorithms will depend on the height of the trees in
transitive forests. Formally, every non-empty transitive forest is either (i)
a disjoint union of connected transitive forests, or (ii) has a _universal
vertex_ , i.e. a vertex that is adjacent to all other vertices (take the root
of the underlying tree). This induces a successive decomposition of the
transitive forest into smaller ones: For a disjoint union, take the disjoint
connected transitive forests. If there is a universal vertex, remove that
vertex to obtain a smaller transitive forest.

The decomposition is unique up to isomorphism: This is obvious in the case of
a disjoint union. If there are several universal vertices, then all removals
result in isomorphic graphs. We define the _height_ $h(\Gamma)$ of a
transitive forest $\Gamma=(V,I)$: If $V=\emptyset$, then $h(\Gamma)=0$. If
$\Gamma$ is a disjoint union of connected transitive forests
$\Gamma_{1},\ldots,\Gamma_{n}$, then $h(\Gamma)=\max\\{h(\Gamma_{i})\mid
i\in[1,n]\\}+1$. If $\Gamma$ has a universal vertex whose removal leaves
$\Gamma^{\prime}$, then $h(\Gamma)=h(\Gamma^{\prime})$.

Among the PVASS-free graphs, it is well-understood when reachability is
decidable:

###### Theorem 2.1 ((DBLP:journals/iandc/Zetzsche21, 46)).

Let $\Gamma$ be PVASS-free. Then $\mathsf{REACH}(\Gamma)$ is decidable iff
$\Gamma$ is a transitive forest.

By $\mathsf{SC}^{\pm}$, we denote the class of PVASS-free graphs $\Gamma$ that
are transitive forests. The abbreviation $\mathsf{SC}^{\pm}$ reflects that
valence systems over $\mathsf{SC}^{\pm}$ are equivalent to _stacked counter
machines_ , as explained in Section 3. Hence, Theorem 2.1 says that for every
graph in $\mathsf{SC}^{\pm}$, the reachability problem is decidable. Moreover,
for every graph $\Gamma$ outside of $\mathsf{SC}^{\pm}$, either $\Gamma$
contains a PVASS-graph (thus showing decidability of $\mathsf{REACH}(\Gamma)$
would in particular solve a long-standing open problem) or
$\mathsf{REACH}(\Gamma)$ is known to be undecidable. Therefore,
$\mathsf{SC}^{\pm}$ is the largest class of graphs $\Gamma$ for which
$\mathsf{REACH}(\Gamma)$ is currently known to be decidable.

##  3\. Main Results

We assume familiarity with the basic complexity classes $\mathsf{L}$
(deterministic logspace), $\mathsf{P}$ (deterministic polynomial time),
$\mathsf{NP}$ (non-deterministic polynomial time), $\mathsf{EXP}$
(deterministic exponential time), $\mathsf{NEXP}$ (non-deterministic
exponential time), and $\mathsf{EXPSPACE}$ (exponential space). By
$\mathsf{ILD}$, we denote the class of problems that are logspace-reducible to
the problem of solvability of integer linear Diophantine equations (ILD):

Given:

A matrix $\mathbf{A}\in\mathbb{Z}^{m\times n}$ and a vector
$\mathbf{b}\in\mathbb{Z}^{m}$.

Question:

Is there a vector $\mathbf{x}\in\mathbb{Z}^{n}$ with
$\mathbf{A}\mathbf{x}=\mathbf{b}$?

It is well known that ILD is solvable in polynomial time.

###### Theorem 3.1 ((DBLP:journals/siamcomp/ChouC82, 9)).

ILD is solvable in polynomial time.

See (DBLP:journals/siamcomp/ChouC82, 9, Theorems 1 and 13). In particular, the
class $\mathsf{ILD}$ lies in between $\mathsf{L}$ and $\mathsf{P}$. The exact
complexity of ILD seems to be open (DBLP:journals/cc/AllenderBO99, 1). It is
conceivable that $\mathsf{ILD}$ coincides with $\mathsf{L}$ or $\mathsf{P}$ or
that it lies strictly in between. Hence, we have the inclusions

$\mathsf{L}\subseteq\mathsf{ILD}\subseteq\mathsf{P}\subseteq\mathsf{NP}\subseteq\mathsf{EXP}\subseteq\mathsf{NEXP}\subseteq\mathsf{EXPSPACE}.$

In order to formulate our main result about the complexity of
$\mathsf{BIREACH}$, we need some terminology. We say that $\mathcal{G}$ is
_UC-bounded_ if there is a $k$ such that for every $\Gamma$ in $\mathcal{G}$,
every unlooped clique in $\Gamma$ has size at most $k$. Otherwise, it is
called _UC-unbounded_. Similarly, _LC-bounded_ (_LC-unbounded_ , respectively)
if the same condition holds for looped cliques. We say that $\mathcal{G}$ is
_height-bounded_ if there is a $k$ with $h(\Gamma)\leq k$ for every $\Gamma$
in $\mathcal{G}$. Otherwise, $\mathcal{G}$ is _height-unbounded_. We now
present an almost complete complexity classification of
$\mathsf{BIREACH}(\mathcal{G})$, where $\mathcal{G}$ is a subclass of
$\mathsf{SC}^{\pm}$. Here, we assume that $\mathcal{G}$ is closed under taking
induced subgraphs. This is a mild assumption that only rules out some
pathological exceptions.

###### Theorem 3.2 (Classification Theorem).

Let $\mathcal{G}\subseteq\mathsf{SC}^{\pm}$ be closed under induced subgraphs.
Then $\mathsf{BIREACH}(\mathcal{G})$ is

  1. (1)

$\mathsf{L}$-complete if $\mathcal{G}$ consists of cliques of bounded size,

  2. (2)

$\mathsf{ILD}$-complete if $\mathcal{G}$ consists of cliques, is UC-bounded,
and LC-unbounded,

  3. (3)

$\mathsf{P}$-complete if $\mathcal{G}$ contains a graph that is not a clique,
and $\mathcal{G}$ is UC-bounded and height-bounded,

  4. (4)

in $\mathsf{EXP}$ if $\mathcal{G}$ is UC-bounded and height-unbounded,

  5. (5)

$\mathsf{EXPSPACE}$-complete otherwise.

From Theorem 3.2, we can deduce our dichotomy for individual graphs $\Gamma$:
Take as $\mathcal{G}$ the set of graphs containing $\Gamma$ and its induced
subgraphs. Then $\mathcal{G}$ is UC-bounded, LC-bounded, and height-bounded
and thus falls into case (1) or (3) above.

###### Corollary 3.3 (Dichotomy for $\mathsf{BIREACH}$).

Let $\Gamma\in\mathsf{SC}^{\pm}$ be a graph. If $\Gamma$ is a clique, then
$\mathsf{BIREACH}(\Gamma)$ is $\mathsf{L}$-complete. Otherwise, the problem
$\mathsf{BIREACH}(\Gamma)$ is $\mathsf{P}$-complete.

(a) Two $\mathbb{N}$-counters, one $\mathbb{Z}$-counter

(b) Three $\mathbb{Z}$-counters

(c) Pushdown with three $\mathbb{Z}$-counters

(d) $\mathsf{C4}$

(e) Two pushdowns

(f) $\mathsf{C4}^{\circ}$

Figure 1. Example graphs for storage mechanisms

We complement Theorem 3.2 with the following undecidability result. The graph
$\mathsf{C4}$ is shown in Fig. 1(d).

###### Theorem 3.4.

If $\Gamma^{-}$ contains $\mathsf{C4}$ as an induced subgraph, then
$\mathsf{BIREACH}(\Gamma)$ is undecidable.

In the case $\Gamma=\mathsf{C4}$, undecidability also follows from an
independent result of (DBLP:journals/pacmpl/KP22, 18) that uses different
techniques.

### Intuition on graph classes

Let us phrase our results in terms of infinite-state systems. In (1) and (2),
we have cliques. A clique with $d$ unlooped vertices and $e$ looped vertices
corresponds to counter machines with $d$-many $\mathbb{N}$-counters and
$e$-many $\mathbb{Z}$-counters (see Fig. 1(a) with $d=2$, $e=1$). Thus, (1)
and (2) show $\mathsf{L}$-completeness for for fixed $d$ and $e$, and
$\mathsf{ILD}$-completeness if only $d$ is fixed. This is in contrast to
reachability: Even for fixed $d$, reachability in machines with $d$-many
$\mathbb{N}$-counters can be non-elementary (DBLP:conf/focs/Leroux21, 21, 10).
Moreover, for $d=0$, these graphs correspond to $\mathbb{Z}$-VASS (see Fig.
1(b) for $e=3$). Thus, we show: For a fixed number of counters in
$\mathbb{Z}$-VASS, the complexity drops from $\mathsf{NL}$ (for general
reachability) to $\mathsf{L}$. If the number of counters in $\mathbb{Z}$-VASS
is not fixed, then we have a drop from $\mathsf{NP}$ (DBLP:conf/rp/HaaseH14,
14) to $\mathsf{ILD}\subseteq\mathsf{P}$.

In (3), we go beyond just counters. Recall the recursive structure of every
graph in $\mathsf{SC}^{\pm}$. In terms of storage, taking a disjoint union
$\Gamma_{1}\cup\Gamma_{2}$ is the same as _building stacks_ : One obtains a
stack, where each entry of the stack is either a storage content of
$\Gamma_{1}$ or $\Gamma_{2}$. Moreover, adding a universal looped vertex
corresponds to _adding a $\mathbb{Z}$-counter_
(DBLP:journals/eatcs/Zetzsche16, 43, 42): This means, in addition to the
configuration of the previous model, we also have a new $\mathbb{Z}$-counter.
After decomposing $\Gamma$ further and further, we are left with a clique of
unlooped vertices. Therefore, valence systems over $\mathsf{SC}^{\pm}$ are
called _stacked counter machines_ : We start with a number of
$\mathbb{N}$-counters and then alternate between building stacks and adding
$\mathbb{Z}$-counters. The height $h(\Gamma)$ is the number of alternations
between the two steps (building stacks and adding $\mathbb{Z}$-counters).

For example, if $\Gamma_{k}$ has two non-adjacent nodes $v_{1},v_{2}$ and
looped nodes $u_{1},\ldots,u_{k}$ such that each $u_{i}$ is adjacent to all
other vertices (see Fig. 1(c) for $\Gamma_{3}$), then valence systems over
$\Gamma_{k}$ are pushdown $\mathbb{Z}$-VASS with $k$ counters. Thus, (3) says
that in stacked counter automata, with a bounded number of
$\mathbb{N}$-counters and a bounded number of alternations (but arbitrarily
many $\mathbb{Z}$-counters!), bidirected reachability is still in
$\mathsf{P}$. This is again a striking complexity drop: In pushdown
$\mathbb{Z}$-VASS, reachability is $\mathsf{NP}$-complete (HagueLin2011, 16),
and the same is true for any fixed number of alternations (if there are no
$\mathbb{N}$-counters) (HaaseZetzsche2019, 15). In fact,
$\mathsf{NP}$-hardness holds for pushdown $\mathbb{Z}$-VASS already for a
single counter (HaaseZetzsche2019, 15). Moreover, our $\mathsf{P}$ upper bound
still holds with a bounded number of $\mathbb{N}$-counters.

In (4), not even the number of alternations is fixed. We obtain an
$\mathsf{EXP}$ upper bound, which is again a drop from reachability: In
stacked counter automata (without $\mathbb{N}$-counters), reachability is
$\mathsf{NEXP}$-complete (HaaseZetzsche2019, 15).

In (5), we show that if neither the alternations nor the number of
$\mathbb{N}$-counters is fixed, $\mathsf{BIREACH}$ is
$\mathsf{EXPSPACE}$-complete. This strengthens
$\mathsf{EXPSPACE}$-completeness of $\mathsf{BIREACH}$ in VASS. Again, general
reachability has much higher complexity: Since our model includes VASS, the
problem is Ackermann-hard (DBLP:conf/focs/Leroux21, 21, 10) and could be even
higher: The algorithm for reachability for general $\mathsf{SC}^{\pm}$ in
(DBLP:journals/iandc/Zetzsche21, 46) uses VASS with nested zero tests, for
which no complexity upper bound is known.

Finally, our undecidability result (Theorem 3.4) says in particular that
reachability in bidirected two-pushdown machines is undecidable: By drawing
$\mathsf{C4}$ as in Fig. 1(e), one can see that it realizes two stacks (the
left two nodes act as a stack, and the right two nodes act as a stack).

##  4\. $\mathsf{BIREACH}$ and subgroup membership

If $\Gamma$ is looped, then $\mathbb{M}\Gamma$ is a group. The groups of this
form are called _graph groups_ or _right-angled Artin groups_ and have been
studied intensively over the last decades (lohrey2008submonoid, 28, 12, 26,
29), in part because of their rich subgroup structure (see, e.g. (Wise2012,
38)). The _subgroup membership problem_ ($\mathsf{SUBMEM}$) is the following.

Given:

A looped graph $\Gamma$, words $w_{1},\ldots,w_{k},w\in X_{\Gamma}^{*}$.

Question:

Does $[w]\in\langle[w_{1}],\ldots,[w_{k}]\rangle$?

If the input graph $\Gamma$ is fixed, we write $\mathsf{SUBMEM}(\Gamma)$. If
$\Gamma$ is drawn from a class $\mathcal{G}$, then we write
$\mathsf{SUBMEM}(\mathcal{G})$. Surprisingly, describing the class of graphs
$\Gamma$ for which $\mathsf{SUBMEM}(\Gamma)$ is decidable is a longstanding
open problem (lohrey2013rational, 25).

Our first observation is that if $\Gamma$ is looped, then the complexity of
$\mathsf{BIREACH}(\Gamma)$ matches that of subgroup membership over
$\mathbb{M}\Gamma$. The connection between subgroups and bidirected valence
automata (albeit under different names) is a prominent theme in group theory.
It is implicit in the well-known concept of Stallings graphs and was used by
(lohrey2010automata, 27) in decidability results. We show that the conversion
can be done in logspace, in both directions.

###### Theorem 4.1.

For any looped graph $\Gamma$, the problems $\mathsf{BIREACH}(\Gamma)$ and
$\mathsf{SUBMEM}(\Gamma)$ are logspace inter-reducible.

Reducing $\mathsf{SUBMEM}(\Gamma)$ to $\mathsf{BIREACH}(\Gamma)$ is easy: To
test whether $[w]$ is contained in $\langle[w_{1}],\dots,[w_{k}]\rangle$ we
construct a bidirected valence system $\mathcal{A}$ with two states $s,t$ and
the transitions $s\mathrel{\mathop{\rightarrow}\limits^{\vbox
to0.0pt{\kern-2.0pt\hbox{$\scriptstyle\bar{w}$}\vss}}}t$ and
$t\mathrel{\mathop{\rightarrow}\limits^{\vbox
to0.0pt{\kern-2.0pt\hbox{$\scriptstyle w_{i}$}\vss}}}t$ for all $1\leq i\leq
k$, and the reverse transitions. Then
$[w]\in\langle[w_{1}],\dots,[w_{k}]\rangle$ holds if and only if there exists
$u\in X_{\Gamma}^{*}$ with $s\mathrel{\mathop{\rightarrow}\limits^{\vbox
to0.0pt{\kern-2.0pt\hbox{$\scriptstyle u$}\vss}}}t$ and $[u]=1$. For the
converse, the following Lemma shows that we can compute in logspace a coset
representation of $\\{[w]\in\mathbb{M}\Gamma\mid
s\mathrel{\mathop{\rightarrow}\limits^{\vbox
to0.0pt{\kern-2.0pt\hbox{$\scriptstyle w$}\vss}}}t\\}$.

###### Lemma 4.2.

Given a looped graph $\Gamma$, a bidirected valence system $\mathcal{A}$ over
$\Gamma$ and states $s,t$ from $\mathcal{A}$, one can compute words
$w_{0},w_{1},\dots,w_{n}\in X_{\Gamma}^{*}$ in logspace such that
$\\{[w]\in\mathbb{M}\Gamma\mid s\mathrel{\mathop{\rightarrow}\limits^{\vbox
to0.0pt{\kern-2.0pt\hbox{$\scriptstyle
w$}\vss}}}t\\}=[w_{0}]\langle[w_{1}],\dots,[w_{n}]\rangle$

Lemma 4.2 reduces reachability to testing membership of $[\bar{w}_{0}]$ in the
set $\langle[w_{1}],\dots,[w_{n}]\rangle$, which is an instance of
$\mathsf{SUBMEM}$. To show Lemma 4.2, we compute in logspace a spanning tree
of the automaton (using (DBLP:journals/jacm/Reingold08, 34)). Then $w_{0}$ is
obtained from the unique path from $s$ to $t$ in the tree. The words
$w_{1},\ldots,w_{n}$ are obtained as labels of _fundamental cycles_
(biggs1997algebraic, 4): These are cycles consisting of one edge outside the
tree and a path inside the tree.

$s$$t$$5$$2$$3$$2$$1$ (a)

(b)

Figure 2. $\mathbb{Z}$-VASS for Example 4.3 (reverse edges are omitted) and
the graph $\mathsf{P4}^{\circ}$

###### Example 4.3.

Lemma 4.2 can be directly used to show that the problem
$\mathsf{BIREACH}(\mathcal{G})$ is in $\mathsf{ILD}$ if $\mathcal{G}$ consists
of looped cliques. In other words, bidirectional reachability for
$\mathbb{Z}$-VASS is in $\mathsf{ILD}$, whereas standard reachability for
$\mathbb{Z}$-VASS is $\mathsf{NP}$-complete (DBLP:conf/rp/HaaseH14, 14). As an
example, consider the bidirected $\mathbb{Z}$-VASS in Fig. 2(a). We compute
the value of an arbitrary $s$-$t$-path, e.g. $w_{0}=5+2=7$, a spanning tree
(the bold edges), and the fundamental cycles with values $w_{1}=5+3-2=6$ and
$w_{2}=5+2-1-2=4$. Since $7+6x+4y=0$ has no integer solution, there is no
$s$-$t$-path with value 0.

The connection between $\mathsf{BIREACH}$ and $\mathsf{SUBMEM}$ can be used to
identify a graph for which the problem $\mathsf{REACH}(\Gamma)$ is undecidable
but $\mathsf{BIREACH}(\Gamma)$ is decidable: Let $\mathsf{P4}^{\circ}$ be the
graph in Fig. 2(b). As shown by (lohrey2008submonoid, 28), the problem
$\mathsf{REACH}(\mathsf{P4}^{\circ})$ is undecidable. However, a result by
(kapovich2005foldings, 17) implies that if a graph $\Gamma$ is looped and
chordal, then $\mathsf{SUBMEM}(\Gamma)$ is decidable (a simpler proof was then
given by Lohrey and Steinberg (lohrey2010automata, 27)). Thus, since
$\mathsf{P4}^{\circ}$ is looped and chordal,
$\mathsf{SUBMEM}(\mathsf{P4}^{\circ})$, and hence
$\mathsf{BIREACH}(\mathsf{P4}^{\circ})$, is decidable.

For the proof of Theorem 3.4, we rely on an undecidability result of
(mikhailova1966occurrence, 33):

###### Theorem 4.4 ((mikhailova1966occurrence, 33)).

$\mathsf{SUBMEM}(\mathsf{C4}^{\circ})$ is undecidable.

The graph $\mathsf{C4}^{\circ}$ is shown in Figure 1(f). The proof of Theorem
4.4 is a simple (but not obvious) reduction of the word problem of any
finitely presented group (since (mikhailova1966occurrence, 33) is in Russian,
we refer to (LyndonSchupp, 30, Chapter IV, Lemma 4.2) or (LohreyZ18, 29, proof
of Lemma 4.2) for short expositions of this reduction). Since there are
finitely presented groups with an undecidable word problem (LyndonSchupp, 30,
Chapter IV, Theorem 7.2), this implies undecidability of
$\mathsf{SUBMEM}(\mathsf{C4}^{\circ})$.

Via Theorem 4.1, Theorem 4.4 implies that
$\mathsf{BIREACH}(\mathsf{C4}^{\circ})$ is undecidable. Using standard
arguments one can transfer the undecidability of
$\mathsf{SUBMEM}(\mathsf{C4}^{\circ})$ to $\mathsf{SUBMEM}(\mathsf{C4})$, and
thus obtain Theorem 3.4.

##  5\. Lower Bounds

We now prove the lower bounds in Theorem 3.2.

###  $\mathsf{L}$-hardness

We can reduce from the reachability on undirected graphs to the problem
$\mathsf{BIREACH}(\Gamma)$ for any $\Gamma$ by replacing each undirected edge
by bidirected $\varepsilon$-labeled transitions. Since the former problem is
$\mathsf{L}$-complete under $\mathsf{AC}^{0}$ many-one reductions
(DBLP:journals/cc/AlvarezG00, 2, 34), so is $\mathsf{BIREACH}(\Gamma)$.

###  $\mathsf{ILD}$-hardness

Next, assume that $\mathcal{G}$ is LC-unbounded. Observe that ILD is the
subgroup membership problem over $\mathbb{Z}^{m}$, where $m$ is part of the
input, and hence log-space reducible to $\mathsf{SUBMEM}(\mathcal{G})$. Since
the equivalence of $\mathsf{SUBMEM}$ and $\mathsf{BIREACH}$ for looped graphs
is uniform in the graph $\Gamma$ (see Section 4),
$\mathsf{BIREACH}(\mathcal{G})$ is $\mathsf{ILD}$-hard.

###  $\mathsf{P}$-hardness

Suppose $\Gamma$ has two non-adjacent vertices $u,v$. In $\Gamma^{\circ}$, $u$
and $v$ generate a free group over two generators, for which subgroup
membership is $\mathsf{P}$-hard (avenhaus1984nielsen, 3). By Theorem 4.1, this
implies $\mathsf{P}$-hardness of $\mathsf{BIREACH}(\Gamma^{\circ})$. Using
standard arguments, $\mathsf{BIREACH}(\Gamma^{\circ})$ reduces to
$\mathsf{BIREACH}(\Gamma)$. Thus, $\mathsf{BIREACH}(\Gamma)$ is
$\mathsf{P}$-hard.

###  $\mathsf{EXPSPACE}$-hardness

We reduce from the word problem over commutative semigroups, which is
$\mathsf{EXPSPACE}$-hard (MAYR1982305, 31). Since $\mathcal{G}$ is UC-
unbounded and closed under induced subgraphs, it contains an unlooped clique
$\Gamma$ of size $|\Sigma|$. We can assume that $\Sigma$ is its node set. Let
$\mathcal{A}$ be the bidirected valence system over $\Gamma$ with three states
$q_{0},q_{1},q_{2}$, the transitions
$q_{0}\mathrel{\mathop{\rightarrow}\limits^{\vbox
to0.0pt{\kern-2.0pt\hbox{$\scriptstyle\bar{u}$}\vss}}}q_{1}$,
$q_{1}\mathrel{\mathop{\rightarrow}\limits^{\vbox
to0.0pt{\kern-2.0pt\hbox{$\scriptstyle v$}\vss}}}q_{2}$, and the transitions
$q\mathrel{\mathop{\rightarrow}\limits^{\vbox
to0.0pt{\kern-2.0pt\hbox{$\scriptstyle\bar{x}y$}\vss}}}q$ for all $(x,y)\in
R$, and their reverse transitions. Then $u\equiv_{R}v$ holds if and only if
$q_{0}\mathrel{\mathop{\rightarrow}\limits^{\vbox
to0.0pt{\kern-2.0pt\hbox{$\scriptstyle w$}\vss}}}q_{2}$ for some $w\in
X_{\Gamma}^{*}$ with $[w]=1$.

##  6\. Upper Bounds I: $\mathsf{L}$ and $\mathsf{ILD}$

In this section we will study $\mathsf{BIREACH}(\mathcal{G})$ for classes
$\mathcal{G}$ of cliques, and prove the $\mathsf{L}$ and $\mathsf{ILD}$ upper
bounds from Theorem 3.2. If $\Gamma$ is an unlooped clique then
$\mathsf{BIREACH}(\Gamma)$ is the reachability problem over bidirected vector
addition systems with states or, equivalently, the word problem for
commutative semigroups (MAYR1982305, 31).

Fix a bidirected valence system $\mathcal{A}=(Q,\to)$ over a clique
$\Gamma=(V,I)$. Let $U$ and $L$ be the sets of unlooped and looped vertices in
$\Gamma$, respectively, and let $s,t\in Q$. We can view the unlooped vertices
as $\mathbb{N}$-counters, which may not fall below zero, and the looped
vertices as $\mathbb{Z}$-counters. Formally, the monoid $\mathbb{M}\Gamma$ is
isomorphic to $\mathbb{B}^{U}\times\mathbb{Z}^{L}$ where $\mathbb{B}$ is the
bicyclic monoid, i.e. the set $\mathbb{N}^{2}$ equipped with the associative
operation
$(a^{-},a^{+})\oplus(b^{-},b^{+})=(a^{-}+b^{-}-\min(a^{+},b^{-}),a^{+}+b^{+}-\min(a^{+},b^{-}))$.
We identify each element $(0,a^{+})$ in $\mathbb{B}$ with $a^{+}\in\mathbb{N}$
and each $(a^{-},0)$ with $-a^{-}\in-\mathbb{N}$. Let $\Phi\colon
X_{\Gamma}^{*}\to\mathbb{Z}^{L}$ be the function which computes the value of
the $\mathbb{Z}$-counters, i.e. $\Phi(w)(v)=|w|_{v}-|w|_{\bar{v}}$ for all
$w\in X_{\Gamma}^{*}$, $v\in L$. Let $\Psi\colon
X_{\Gamma}^{*}\to\mathbb{B}^{U}$ be the morphism defined by $\Psi(v)(v)=(0,1)$
and $\Psi(\bar{v})(v)=(1,0)$ for all $v\in U$, and $\Psi(x)(v)=(0,0)$ for all
$x\in(V\cup\bar{V})\setminus\\{v,\bar{v}\\}$. Then
$\mathbb{M}\Gamma\to\mathbb{B}^{U}\times\mathbb{Z}^{L}$,
$[w]\mapsto(\Psi(w),\Phi(w))$ for $w\in X_{\Gamma}^{*}$, is an isomorphism.

###  $\mathbb{N}$-counters

If we consider only $\mathbb{N}$-counters, i.e. $\mathcal{A}$ is a bidirected
VASS, the reachability problem and the structure of reachability sets are well
understood:

###### Lemma 6.1 ((MAYR1982305, 31)).

One can decide in deterministic space $2^{O(|U|)}\cdot\log\|\mathcal{A}\|$
whether there exists a path $s\mathrel{\mathop{\rightarrow}\limits^{\vbox
to0.0pt{\kern-2.0pt\hbox{$\scriptstyle w$}\vss}}}t$ with $\Psi(w)=\mathbf{0}$
and, if so, return such a path.

We define $\mathsf{Reach}(p,q)=\\{\Psi(w)\mid
p\mathrel{\mathop{\rightarrow}\limits^{\vbox
to0.0pt{\kern-2.0pt\hbox{$\scriptstyle
w$}\vss}}}_{\mathcal{A}}q\\}\cap\mathbb{N}^{U}$ for any states $p,q\in Q$.
Lemma 6.2 lets us partition the set $U$ of $\mathbb{N}$-counters into
(exponentially) bounded components $B$ and simultaneously unbounded components
$U\setminus B$. In the proof, we employ a representation of
$\mathsf{Reach}(p,q)$ as a hybrid linear set
$\bigcup_{i=1}^{m}\\{\mathbf{b}_{i}+\sum_{j=1}^{\ell}\lambda_{j}\mathbf{p}_{j}\mid\lambda_{1},\dots,\lambda_{\ell}\in\mathbb{N}\\}$
with $\mathbf{b}_{i},\mathbf{p}_{j}\in\mathbb{N}^{\Sigma}$ as shown in
(DBLP:conf/fct/KoppenhagenM97, 19). See Section C.1.

###### Lemma 6.2.

One can compute in deterministic space $2^{O(|U|)}\cdot\log\|\mathcal{A}\|$ a
set $B\subseteq U$ and a number $b\leq 2^{O(|U|)}\cdot\|\mathcal{A}\|$ such
that for all $q\in Q$ we have:

  * •

$\mathbf{v}(u)\leq b$ for all $\mathbf{v}\in\mathsf{Reach}(s,q)$ and $u\in B$,

  * •

for every $c\in\mathbb{N}$ there exists $\mathbf{v}\in\mathsf{Reach}(s,q)$
with $\mathbf{v}(u)\geq c$ for all $u\in U\setminus B$.

### Adding $\mathbb{Z}$-counters

We will decide reachability in $\mathcal{A}$ by computing a representation for

$\mathsf{Eff}(s,t)=\\{\Phi(w)\mid s\mathrel{\mathop{\rightarrow}\limits^{\vbox
to0.0pt{\kern-2.0pt\hbox{$\scriptstyle
w$}\vss}}}_{\mathcal{A}}t,\,\Psi(w)=\mathbf{0}\\}.$

Since $[w]=1$ if and only if $\Psi(w)=\mathbf{0}$ and $\Phi(w)=\mathbf{0}$ we
only need to test $\mathbf{0}\in\mathsf{Eff}(s,t)$. Observe that
$\mathsf{Eff}(s,t)$ is either empty or a coset
$\mathsf{Eff}(s,t)=\mathbf{u}+\mathsf{Eff}(s,s)$ for any
$\mathbf{u}\in\mathsf{Eff}(s,t)$. Using Lemma 6.1 we can test whether there is
a path $s\mathrel{\mathop{\rightarrow}\limits^{\vbox
to0.0pt{\kern-2.0pt\hbox{$\scriptstyle w$}\vss}}}t$ with $\Psi(w)=\mathbf{0}$,
and, if so, we find $\mathbf{u}:=\Phi(w)\in\mathsf{Eff}(s,t)$. It remains to
compute a representation of the subgroup $\mathsf{Eff}(s,s)$.

###### Proposition 6.3.

In deterministic space $2^{O(|U|)}\cdot\log\|\mathcal{A}\|$, we can compute
$L^{\prime}\supseteq L$, $|L^{\prime}|\leq|\Gamma|$, and
$\mathbf{v}_{1},\dots,\mathbf{v}_{n}\in\mathbb{Z}^{L^{\prime}}$ with
$\mathsf{Eff}(s,s)=\\{\mathbf{v}|_{L}\mid\mathbf{v}\in\langle\mathbf{v}_{1},\dots,\mathbf{v}_{n}\rangle,~{}\mathbf{v}|_{L^{\prime}\setminus
L}=\mathbf{0}\\}$.

_Proof Sketch._ We eliminate the $\mathbb{N}$-counters in $\mathcal{A}$ by
replacing the unbounded counters by $\mathbb{Z}$-counters and maintaining the
bounded ones in the finite state. We obtain a system $\mathcal{A}^{\prime}$
over a looped clique, for which the statement follows from Lemma 4.2. Clearly,
every valid $\mathcal{A}$-run translates into a valid
$\mathcal{A}^{\prime}$-run. However, in a valid $\mathcal{A}^{\prime}$-run,
the formerly unbounded counters can now take negative values. We can prepend a
cycle run which takes sufficiently large values in the unbounded components,
and append the reverse cycle run to cancel its effect. This ensures that all
counters remain nonnegative during the run, which can thus be translated into
an $\mathcal{A}$-run. ∎

We can now prove the upper bounds for cases (1) and (2) in Theorem 3.2. As
explained above we can test in exponential space (logarithmic space if
$\mathcal{G}$ consists of cliques of bounded size) whether $\mathsf{Eff}(s,t)$
is nonempty and, if so compute a vector $\mathbf{u}\in\mathsf{Eff}(s,t)$. It
remains to test $\mathbf{0}\in\mathsf{Eff}(s,t)$, which is equivalent to
$-\mathbf{u}\in\mathsf{Eff}(s,s)$. Using Proposition 6.3, this can be solved
in $\mathsf{ILD}$. If $|\Gamma|$ is bounded then this is in $\mathsf{L}$ (even
$\mathsf{TC}^{0}$) (DBLP:conf/stacs/ElberfeldJT12, 13, Theorem 13).

###### Proposition 6.4.

If $\mathcal{G}$ is a UC-bounded class of cliques, then the problem
$\mathsf{BIREACH}(\mathcal{G})$ belongs to $\mathsf{ILD}$. If $\mathcal{G}$ is
a class of cliques of bounded size, then $\mathsf{BIREACH}(\mathcal{G})$
belongs to $\mathsf{L}$.

Similarly we can prove the following result, which will be used in Section 7.

###### Theorem 6.5.

Given a clique $\Gamma\in\mathcal{G}$, a bidirected valence system
$\mathcal{A}=(Q,\to)$ over $\Gamma$, and states $s,t\in Q$, one can test in
exponential space (polynomial time if $\mathcal{G}$ is UC-bounded) if
$\mathsf{Eff}(s,t)$ is nonempty and, if so, compute a coset representation
$\mathbf{u}+\langle\mathbf{v}_{1},\dots,\mathbf{v}_{n}\rangle$ for
$\mathsf{Eff}(s,t)$.

##  7\. Upper Bounds II: $\mathsf{P}$, $\mathsf{EXP}$, $\mathsf{EXPSPACE}$

We now prove the upper bounds of (3) and (4) in Theorem 3.2. Let
$\mathsf{SC}^{\pm}_{d}$ be the class of graphs in $\mathsf{SC}^{\pm}$ where
each unlooped clique has size at most $d$, and let
$\mathsf{SC}^{\pm}_{d,\ell}$ be the class of those graphs $\Gamma$ in
$\mathsf{SC}^{\pm}_{d}$ with $h(\Gamma)\leq\ell$. We prove that (i)
$\mathsf{BIREACH}(\mathsf{SC}^{\pm})$ is in $\mathsf{EXPSPACE}$, (ii) for
every $d$, $\mathsf{BIREACH}(\mathsf{SC}^{\pm}_{d})$ is in $\mathsf{EXP}$ and
(iii) for every $d,\ell\geq 0$, the problem
$\mathsf{BIREACH}(\mathsf{SC}^{\pm}_{d,\ell})$ is in $\mathsf{P}$.

### Key ideas and outline

The graphs in $\mathsf{SC}^{\pm}_{d,\ell}$ correspond to the following storage
mechanisms. The simplest case, graphs in $\mathsf{SC}^{\pm}_{d,0}$, consist in
collections of $d$ counters with values in $\mathbb{N}$, or $d$-VASS. The
storage mechanism corresponding to $\mathsf{SC}^{\pm}_{d,1}$ is a stack, where
each entry contains $d$ such $\mathbb{N}$-counters. In addition, they have
$\mathbb{Z}$-counters in parallel to such stacks (note that using more
$\mathbb{N}$-counters in addition to a stack would be a PVASS, which we are
avoiding). Thus, $\mathsf{SC}^{\pm}_{d,1}$ corresponds to “stacks of $d$
$\mathbb{N}$-counters, plus $\mathbb{Z}$-counters”. The _building stacks_ and
_adding $\mathbb{Z}$-counters_ can now be iterated to obtain the storage
mechanisms for $\mathsf{SC}^{\pm}_{d,\ell}$ for higher $\ell$: A storage
mechanism with stacks, where each entry is a configuration of an
$\mathsf{SC}^{\pm}_{d,1}$ storage, plus additional $\mathbb{Z}$-counters, is
one in $\mathsf{SC}^{\pm}_{d,2}$, etc.

Our algorithms work as follows. We first translate a valence system over
$\mathsf{SC}^{\pm}_{d,\ell}$ into a type of grammar that we call $k$-grammar.
This translation is quite similar to existing approaches to show that general
reachability over $\mathsf{SC}^{\pm}_{1,\ell}$ is decidable
(lohrey2008submonoid, 28) and even $\mathsf{NP}$-complete (HaaseZetzsche2019,
15). The difference to the previous approaches is that for _bidirected_
valence systems, we can construct _bidirected $k$-grammars_, which are
$k$-grammars that satisfy a carefully chosen set of symmetry conditions. In
this translation, we also eliminate the $d$ $\mathbb{N}$-counters: Roughly
speaking, Theorem 6.5 lets us replace them by a gadget that preserves their
interaction with the $\mathbb{Z}$-counters.

After the reduction to grammars, the algorithm in (HaaseZetzsche2019, 15) (and
also the $\mathsf{NP}$ algorithm for pushdown $\mathbb{Z}$-VASS (HagueLin2011,
16), which correspond to $\mathsf{SC}^{\pm}_{0,1}$) employs a result by
(DBLP:conf/cade/VermaSS05, 37). It says that given a context-free grammar, one
can construct in polynomial time an existential Presburger formula for its
Parikh image. Existential Presburger arithmetic corresponds to systems of
integer linear _inequalities_ , for which feasibility is
$\mathsf{NP}$-complete. (To be precise, (HaaseZetzsche2019, 15) uses
Presburger arithmetic extended with Kleene stars, to deal with
$\mathsf{SC}^{\pm}_{0,\ell}$ for $\ell>1$.) We show that for _bidirected_
grammars, we have an analogous result that yields systems of linear integer
_equations_ , which can be solved in $\mathsf{P}$.

This analogue of (DBLP:conf/cade/VermaSS05, 37) lets us express emptiness of
bidirected grammars using _coset circuits_ , which are (newly introduced)
circuits to describe cosets $C\subseteq\mathbb{Z}^{m}$. They can be seen as
compressed representations of integer linear equation systems. In the final
step, we observe that those coset circuits translate into exponential-sized
linear equation systems. Moreover, for every fixed $\ell$, on input from
$\mathsf{SC}^{\pm}_{d,\ell}$, the coset circuits have bounded depth, resulting
in polynomial-sized equation systems.

### Grammars

Let us now define $k$-grammars. They have a set $N$ of nonterminal symbols
(which can be rewritten by a grammar rule) and a set $T$ of terminal symbols
(which can not be rewritten). We allow letters in $T$ to occur negatively, but
the letters in $N$ can only occur non-negatively. Hence, we derive vectors in
$\mathbb{N}^{N}+\mathbb{Z}^{T}$, or equivalently, vectors
$\mathbf{u}\in\mathbb{Z}^{N\cup T}$, where $\mathbf{u}(a)\geq 0$ for each
$a\in N$. We say that a vector $\mathbf{v}\in\mathbb{N}^{N}$ _occurs_ in such
a $\mathbf{u}$ if $\mathbf{u}(a)\geq\mathbf{v}(a)$ for every $a\in N$.

#### Formal definition

A _$k$ -grammar_ is a tuple $G=(N,T,P)$, where

  * •

$N$ is a finite alphabet of _nonterminals_ , which is a disjoint union
$N=\bigcup_{i=0}^{k}N_{i}$,

  * •

$T$ is a finite alphabet of _terminals_ , which is a disjoint union
$T=\bigcup_{i=0}^{k}T_{i}$,

  * •

$P$ is a finite set of _productions_ of one of two forms:

    * –

$a\to b$ with $a\in N_{i}$, $b\in N_{j}$, $|i-j|=1$.

    * –

$a\to\mathbf{u}$ with $a\in N_{0}$ and
$\mathbf{u}\in\mathbb{N}^{N_{0}}+\mathbb{Z}^{T}$.

The letters in $T_{i}$ ($N_{i}$) are the _level- $i$ (non)terminals_. We write

$N_{[i,j]}=\bigcup_{i\leq r\leq j}N_{r},$

and analogously for $T_{[i,j]}$. Define $R\subseteq N$ as the subset of $a\in
N$ that appear on some right-hand side of the grammar. We also write
$R_{i}=R\cap N_{i}$ and use the notation $R_{[i,j]}$ as for $N$ and $T$.

#### Derivations

In these grammars, derivations produce vectors in
$\mathbb{N}^{N}+\mathbb{Z}^{T}$ instead of words.222 Usually, grammars derive
strings rather than vectors. We could also develop our theory using grammars
that generate strings, but since we are only interested in the generated
strings up to reordering of letters, we simplify the exposition by working
directly with vectors.  A _configuration_ is a vector
$\mathbf{v}\in\mathbb{N}^{N}+\mathbb{Z}^{T}$. For $i\in[0,k]$, we define the
$i$-derivation relation $\,\Rightarrow_{i}\,$ as follows. We begin with
defining $\,\Rightarrow_{0}\,$ and then define each $\,\Rightarrow_{i}\,$
based on $\,\Rightarrow_{i-1}\,$. For configurations
$\mathbf{v},\mathbf{v}^{\prime}\in\mathbb{N}^{N}+\mathbb{Z}^{T}$, we have
$\mathbf{v}\,\Rightarrow_{0}\,\mathbf{v}^{\prime}$ if there is some $a\in
N_{0}$ and a production $a\to\mathbf{u}$ with
$\mathbf{u}\in\mathbb{Z}^{N_{0}\cup T}$ or $\mathbf{u}\in N_{1}$ such that
$\mathbf{v}(a)>0$ and $\mathbf{v}^{\prime}=\mathbf{v}-a+\mathbf{u}$.

In order to define $\,\Rightarrow_{i}\,$ inductively for $i>0$, we first need
to define generated sets. Let $\,\mathrel{\mathop{\Rightarrow}\limits^{\vbox
to0.0pt{\kern-2.0pt\hbox{$\scriptstyle*$}\vss}}}_{i}\,$ denote the reflexive
transitive closure of $\,\Rightarrow_{i}\,$. We define the generated set
$L(a)$ for each $a\in N_{i}$:

$L(a)=\\{\mathbf{u}\in\mathbb{N}^{N_{[i+1,k]}}+\mathbb{Z}^{T_{[i+1,k]}}\mid\text{$a\,\mathrel{\mathop{\Rightarrow}\limits^{\vbox
to0.0pt{\kern-2.0pt\hbox{$\scriptstyle*$}\vss}}}_{i}\,\mathbf{u}$}\\}.$

We define $\,\Rightarrow_{i}\,$ based on $\,\Rightarrow_{i-1}\,$: We have
$\mathbf{v}\,\Rightarrow_{i}\,\mathbf{v}^{\prime}$ if there is an $a\in N_{i}$
with $\mathbf{v}(a)>0$ and a production $a\to a^{\prime}$ for some
$a^{\prime}\in N_{i-1}$ and a $\mathbf{u}\in\mathbb{Z}^{N\cup T}$ with
$\mathbf{u}\in L(a^{\prime})$ and
$\mathbf{v}^{\prime}=\mathbf{v}-a+\mathbf{u}$. If $a\to b$ is a production
with $a\in N_{i}$ and $b\in N_{i+1}$ and $\mathbf{v}(a)>0$ and
$\mathbf{v}^{\prime}=\mathbf{v}-a+b$, then we also have
$\mathbf{v}\,\Rightarrow_{i}\,\mathbf{v}^{\prime}$. The _emptiness problem_
asks, given a $k$-grammar $G$ and a nonterminal $a$ of $G$, is
$L(a)\neq\emptyset$?

#### Intuition

We give some intuition on how $\mathsf{REACH}(\mathsf{SC}^{\pm}_{0,\ell})$ is
translated into a grammar. Each nonterminal is of the form $(p,s^{x},q)$,
where $p,q$ are states of the valence system and $s^{x}$ specifies some part
of the storage mechanism (see Section D.1 for details). Then $(p,s^{x},q)$
represents the set of all runs of the system from $p$ to $q$ such that on part
$s^{x}$, the run has overall neutral effect.

Specifically, in the case of $\mathsf{SC}^{\pm}_{0,1}$, i.e. pushdown
$\mathbb{Z}$-VASS, reachability amounts to checking whether a context-free
language contains a word whose letter counts satisfy some linear condition. In
a $0$-grammar, we have context-free rewriting rules ($a\to\mathbf{u}$), which
involve nonterminals ($N$) and terminals ($T$). In addition, the definition of
$L(a)$ requires that a derived contains no terminal from $T_{0}$ anymore: This
is used to implement the linear condition on letter counts for pushdown
$\mathbb{Z}$-VASS.

For $\mathsf{SC}^{\pm}_{0,\ell}$, $\ell>1$, we need to simulate stacks with
$\mathsf{SC}^{\pm}_{0,\ell-1}$ configurations in each stack entry. Here, we
can use a higher $k$: A derivation step at level $k$ involves an entire
derivation at level $k-1$. This corresponds to the fact that between a pair of
push and pop of a $\mathsf{SC}^{\pm}_{d,\ell}$ machine, there is an entire run
of an $\mathsf{SC}^{\pm}_{d,\ell-1}$ machine.

### Bidirected grammars

We are now ready to present the symmetry conditions of bidirected grammars.
For a $k$-grammar $G$, an _involution_ is a map ${\cdot}^{\dagger}\colon N\to
N$ such that for $a\in N_{i}$, we have ${a}^{\dagger}\in N_{i}$ for
$i\in[0,k]$ and ${({a}^{\dagger})}^{\dagger}=a$. Then, for
$\mathbf{u}\in\mathbb{Z}^{N\cup T}$, we define
${\mathbf{u}}^{\dagger}\in\mathbb{Z}^{N\cup T}$ as
${\mathbf{u}}^{\dagger}(a)=\mathbf{u}({a}^{\dagger})$ for $a\in N$ and
${\mathbf{u}}^{\dagger}(a)=-\mathbf{u}(a)$ for $a\in T$. Here,
${\mathbf{u}}^{\dagger}$ can be thought of as the inverse of $\mathbf{u}$.

We say that a $k$-grammar $G$ is _bidirected_ if there is an involution
${\cdot}^{\dagger}\colon N\to N$ such that

  1. (1)

for every production $a\to\mathbf{u}$ in $P$, we have a production
${a}^{\dagger}\to{\mathbf{u}}^{\dagger}$ in $P$,

  2. (2)

for every $a\in R_{0}$ and every production $a\to b+\mathbf{u}$ with $b\in
R_{0}$, $\mathbf{u}\in\mathbb{N}^{R_{0}}+\mathbb{Z}^{T}$, we have
$b\,\mathrel{\mathop{\Rightarrow}\limits^{\vbox
to0.0pt{\kern-2.0pt\hbox{$\scriptstyle*$}\vss}}}_{0}\,a+{\mathbf{u}}^{\dagger}$,

  3. (3)

for every production $a\to b$ with $a\in N_{i}$, $b\in N_{j}$ with $|i-j|=1$
and $a\in R$, we also have $b\to a$,

  4. (4)

for every $a\in R$, we have $L(a)\neq\emptyset$,

  5. (5)

if $a\in R_{0}$, then $a\,\mathrel{\mathop{\Rightarrow}\limits^{\vbox
to0.0pt{\kern-2.0pt\hbox{$\scriptstyle*$}\vss}}}_{0}\,a+a+{a}^{\dagger}$.

#### Intuition on bidirectedness

We give some intuition on these symmetry conditions. Recall that in the
translation from automata to grammars, each nonterminal is of the form
$(p,s^{x},q)$, where $p,q$ are states and $s^{x}$ represents part of the
storage mechanism. The involution is given by
${(p,s^{x},q)}^{\dagger}=(q,s^{x},p)$. Since the map ${\cdot}^{\dagger}$
negates terminal letters, which represent counter values, condition (1)
reflects the existence of paths that go in the opposite direction with
opposite effect.

Conditions (2),(3) let us reverse productions: Consider a production
$(p,s^{x},q)\to(p,s^{x},t)+(t,s^{x},q)$. It says one can get a run from $p$ to
$q$ by combining one from $p$ to $t$ with one from $t$ to $q$. Now (2) yields
a derivation $(p,s^{x},t)\,\mathrel{\mathop{\Rightarrow}\limits^{\vbox
to0.0pt{\kern-2.0pt\hbox{$\scriptstyle*$}\vss}}}_{0}\,(p,s^{x},q)+{(t,s^{x},q)}^{\dagger}=(p,s^{x},q)+(q,s^{x},t)$.
This reflects that paths from $p$ to $t$ can be obtained from ones from $p$ to
$q$ and ones from $q$ to $t$.

_Cross-level productions_ $a\to b$ with $a\in N_{i}$, $b\in N_{j}$ with
$|i-j|=1$ describe the relationship between comparable parts $s^{x}$ of the
storage. Here, “comparable” means “a subset of the counters.” For example, if
$r^{y}$ represents a subset of the counters in $s^{x}$, we have productions
$(p,s^{x},q)\to(p,r^{y},q)$, which tell us: A run $\rho$ from $p$ to $q$ that
is neutral on $r^{y}$ is also neutral on $s^{x}$ _if_ $\rho$’s effect on the
additional counters in $s^{x}$ is zero (recall that a derivation on level
$i-1$ can only be used as a step on level $i$ if its effect on the terminal
letters is zero). Now (3) says that this is symmetric: The production
$(p,r^{y},q)\to(p,s^{x},q)$ tells us that any run that is even neutral on
$s^{x}$ is in particular neutral on $r^{y}$.

The last two conditions (4) and (5) stem from the fact that we sometimes
construct derivations that, as a byproduct, create vectors
$a+{a}^{\dagger}=(p,s^{x},q)+(q,s^{x},p)$. On the one hand, we want to argue
that such cycles can always be eliminated by further derivation. This is
guaranteed by (4), which lets us derive some vector $\mathbf{u}$ from $a$ and
then because of (2), the inverse ${\mathbf{u}}^{\dagger}$ from
${a}^{\dagger}$. This results in the vector
$\mathbf{u}+{\mathbf{u}}^{\dagger}$, but the nonterminals in $\mathbf{u}$ are
on a higher level than $a$. Thus, inside of a derivation on level $k$, we can
completely get rid of it. Finally, (5) complements this by letting us create
such cycles. This simplifies the set of derived vectors.

#### Constructing bidirected grammars

We obtain the following reduction. It is technically involved, but since it
follows similar ideas to existing approaches ((lohrey2008submonoid, 28, 15)),
we defer details to the appendix.

###### Proposition 7.1.

There is a polynomial-time Turing reduction from
$\mathsf{BIREACH}(\mathsf{SC}^{\pm}_{d})$ to the emptiness problem for
bidirected $k$-grammars. If the input graphs are from
$\mathsf{SC}^{\pm}_{d,\ell}$, then we only use $k$-grammars with $k\leq
2\ell$.

Note that the reduction described in Proposition 7.1 is a Turing reduction.
This is because we need to ensure (4). To this end, the reduction involves a
saturation that successively enlarges the set of nonterminals that are known
to generate a non-empty set: At first, it only allows a small set of triples
$(p,s^{x},q)\in N$, whose language is non-empty by construction, to appear on
right-hand sides. It then invokes the emptiness check, which yields more
triples (nonterminals) that can then appear on right-hand sides in the next
iteration, etc.

###### Example 7.2.

Let us see Proposition 7.1 in an example. Consider the graph $\Gamma$ in Fig.
3(a) and the valence system in Fig. 3(b). Observe that $\Gamma$ corresponds to
a pushdown $\mathbb{Z}$-VASS: The nodes $a,b$ realize a stack, and $c$ acts as
a $\mathbb{Z}$-counter. For simplicity, we show the translation in the final
step of the saturation (described after Proposition 7.1), i.e. where the set
of triples $(p,s^{x},q)\in N$ with $L((p,s^{x},q))\neq\emptyset$ has
stabilized. The entry $s^{x}$ in the nonterminals represents to a subset of
the nodes in the graph: First, ${a}^{\tiny{\trianglepafillha}}$ and
${b}^{\tiny{\trianglepafillha}}$ represent only the node $a$ and $b$,
respectively. Second, ${c}^{\tiny{\trianglepafillha}}$ represents the set
$\\{a,b\\}$. Third, ${c}^{\tiny{\trianglepa}}$ represents $\\{a,b,c\\}$. This
decomposition into subsets is derived from the tree structure of $\Gamma$ as a
transitive forest, see Fig. 3(c). The decomposition also determines the
nonterminal levels: We have $N_{0}=\\{(p,s^{x},q)\mid
s^{x}\in\\{{a}^{\tiny{\trianglepafillha}},{b}^{\tiny{\trianglepafillha}}\\}\\}$,
$N_{1}=\\{(p,s^{x},q)\mid s^{x}={c}^{\tiny{\trianglepafillha}}\\}$ and
$N_{2}=\\{(p,s^{x},q)\mid s^{x}={c}^{\tiny{\trianglepa}}\\}$. The terminal
letters correspond to looped nodes, and their levels also stem from the
decomposition into a tree, i.e. $T_{0}=T_{1}=\emptyset$ and $T_{2}=\\{c\\}$.

$a$$c$$b$ (a) The graph $\Gamma$ $q_{0}$$q_{1}$$a$$b$$c$ (b) Valence system
over $\Gamma$ (reverse edges are not shown) level 2level 1level
0${c}^{\tiny{\trianglepa}}$${c}^{\tiny{\trianglepafillha}}$${a}^{\tiny{\trianglepafillha}}$${b}^{\tiny{\trianglepafillha}}$$c$$a$$b$
(c) Decomposition of $\Gamma$ into a tree.

Figure 3. Graph and example valence system

Intuitively, a nonterminal $(p,s^{x},q)$ represents runs of the valence system
in which only transitions over nodes (in $\Gamma$) in $s^{x}$ and its
ancestors in the tree are used and where the effect on the storage is neutral
w.r.t. nodes in $s^{x}$. However, the derived multisets of $(p,s^{x},q)$ can
also contain nonterminals $(p^{\prime},r^{y},q^{\prime})$ as “placeholders”,
where $r^{y}$ is above $s^{x}$ in the tree decomposition. This allows
derivations at a higher level to insert neutral runs into each other to
simulate runs that are neutral on the union of two subtrees.

Note that $(q_{0},{u}^{\tiny{\trianglepafillha}},q_{1})$ and
$(q_{1},{u}^{\tiny{\trianglepafillha}},q_{0})$ have empty languages for
$u\in\\{a,b\\}$, because there is no run between $q_{0}$ and $q_{1}$ with a
neutral effect w.r.t $a$ and $\bar{a}$. Therefore, we will not use these
nonterminals on the right-hand side. However, all other nonterminals
$(p,s^{x},q)$ have non-empty languages. Thus, the set $R\subseteq N$ contains
all nonterminals $(p,s^{x},q)$ with $p=q$.

We begin with productions for nonterminals
$(p,{a}^{\tiny{\trianglepafillha}},p)$:

$\displaystyle(p,{u}^{\tiny{\trianglepafillha}},p)$
$\displaystyle\to(p,{u}^{\tiny{\trianglepafillha}},p)+(p,{u}^{\tiny{\trianglepafillha}},p)$
$p\in\\{q_{0},q_{1}\\}$, $u\in\\{a,b\\}$
$\displaystyle(p,{a}^{\tiny{\trianglepafillha}},p)$
$\displaystyle\to(q,{a}^{\tiny{\trianglepafillha}},q)$
$p,q\in\\{q_{0},q_{1}\\}$

Note that the second production stems from the fact that we can start from
$q_{0}$, then move to $q_{1}$ with $a$, then execute a loop from $q$ to $q$,
and then go back to $q_{0}$ with $\bar{a}$. We also have productions for the
$c$ and $-c$ loops at $q_{1}$:

$\displaystyle(q_{1},{u}^{\tiny{\trianglepafillha}},q_{1})$ $\displaystyle\to
c,$ $\displaystyle(q_{1},{u}^{\tiny{\trianglepafillha}},q_{1})$
$\displaystyle\to-c$ for $u\in\\{a,b\\}$

Finally, we have cross-level productions:

$\displaystyle(p,{c}^{\tiny{\trianglepafillha}},p)$
$\displaystyle\to(p,{u}^{\tiny{\trianglepafillha}},p)$
$\displaystyle(p,{u}^{\tiny{\trianglepafillha}},p)$
$\displaystyle\to(p,{c}^{\tiny{\trianglepafillha}},p)$ (level 0/1)
$\displaystyle(p,{c}^{\tiny{\trianglepa}},p)$
$\displaystyle\to(p,{c}^{\tiny{\trianglepafillha}},p)$
$\displaystyle(p,{c}^{\tiny{\trianglepafillha}},p)$
$\displaystyle\to(p,{c}^{\tiny{\trianglepa}},p)$ (level 1/2)

for every $p\in\\{q_{0},q_{1}\\}$ and $u\in\\{a,b\\}$.

### Reversing derivations on each level

We will show an analogue of (2) at levels $i>0$, by induction on $i$. Since a
step on level $i>0$ involves an entire derivation on level $i-1$ (which can
result in several nonterminals), the induction works with a stronger property
where the reverse derivation can not only start in one produced nonterminal
(as in (2)), but arbitrary vectors in $\mathbb{N}^{R_{i}}$. But then, suppose
we want to reverse

$(p,s^{x},q)\,\Rightarrow_{0}\,(p,s^{x},t)+(t,s^{x},q).$

Deriving $(p,s^{x},q)$ from $(p,s^{x},t)+(t,s^{x},q)$ would require either
$(p,s^{x},t)$ or $(t,s^{x},q)$ to derive a vector without nonterminals, which
would be too strong a condition. However, we can use a slight relaxation: We
will show that derivations can be reversed _up to a byproduct of cycles
$b+{b}^{\dagger}$_. For instance, in our example, the condition (2) yields
$(p,s^{x},t)\,\mathrel{\mathop{\Rightarrow}\limits^{\vbox
to0.0pt{\kern-2.0pt\hbox{$\scriptstyle*$}\vss}}}_{0}\,(p,s^{x},q)+{(t,s^{x},q)}^{\dagger}$
and hence

$(p,s^{x},t)+(t,s^{x},q)\,\mathrel{\mathop{\Rightarrow}\limits^{\vbox
to0.0pt{\kern-2.0pt\hbox{$\scriptstyle*$}\vss}}}_{0}\,(p,s^{x},q)+{(t,s^{x},q)}^{\dagger}+(t,s^{x},q).$

To make “up to cycles $b+{b}^{\dagger}$” precise, we now introduce the
equivalence relations $\approx_{a}$.

First, we define the relation $\leadsto$ on $N$ as follows. For $a\in N_{i}$
and $b\in N_{[i,k]}$, we have $a\leadsto b$ iff there is a configuration
$\mathbf{u}\in\mathbb{N}^{N_{[i,k]}}+\mathbb{Z}^{T_{[i,k]}}$ with
$\mathbf{u}(b)\geq 1$ and $a\,\Rightarrow_{i}\,\mathbf{u}$. In other words,
for $a\in N_{i}$ and $b\in N_{[i,k]}$, we have $a\leadsto b$ if $b$ can be
reached from $a$ in one derivation step on level $i$.

Let $\mathrel{\mathop{\leadsto}\limits^{\vbox
to0.0pt{\kern-2.0pt\hbox{$\scriptstyle*$}\vss}}}$ denote the reflexive
transitive closure of $\leadsto$. For each $a\in N_{i}$, we define the monoid
$\Delta_{a}$, which is generated by all $b+{b}^{\dagger}$ with $b\in
N_{[i+1,k]}$ and $a\mathrel{\mathop{\leadsto}\limits^{\vbox
to0.0pt{\kern-2.0pt\hbox{$\scriptstyle*$}\vss}}}b$. Hence,
$\Delta_{a}\subseteq\mathbb{N}^{N_{[i+1,k]}}$. For
$\mathbf{u},\mathbf{u}^{\prime}\in\mathbb{N}^{N_{[i,k]}}+\mathbb{Z}^{T_{[i,k]}}$,
we have $\mathbf{u}\approx_{a}\mathbf{u}^{\prime}$ if and only if there are
$\mathbf{d},\mathbf{d}^{\prime}\in\Delta_{a}$ with
$\mathbf{u}+\mathbf{d}=\mathbf{u}^{\prime}+\mathbf{d}^{\prime}$. A $k$-grammar
is called _$i$ -bidirected_ if for every $a\in R_{i}$ and every derivation
$a\,\mathrel{\mathop{\Rightarrow}\limits^{\vbox
to0.0pt{\kern-2.0pt\hbox{$\scriptstyle*$}\vss}}}_{i}\,\mathbf{u}+\mathbf{v}$
with $\mathbf{u}\in\mathbb{N}^{R_{i}}$, $\mathbf{u}\neq\mathbf{0}$,
$\mathbf{v}\in\mathbb{N}^{R_{[i,k]}}+\mathbb{Z}^{T_{[i,k]}}$, then
$\mathbf{u}\,\mathrel{\mathop{\Rightarrow}\limits^{\vbox
to0.0pt{\kern-2.0pt\hbox{$\scriptstyle*$}\vss}}}_{i}\,a+\mathbf{v}^{\prime}$
for some $\mathbf{v}^{\prime}$ with
$\mathbf{v}^{\prime}\approx_{a}{\mathbf{v}}^{\dagger}$. In short, up to
differences in $\Delta_{a}$, we can reverse derivations on level $i$ that
start in nonterminals in $R$. Note that if $G$ is $i$-bidirected, then on
$R_{i}$, the relation $\mathrel{\mathop{\leadsto}\limits^{\vbox
to0.0pt{\kern-2.0pt\hbox{$\scriptstyle*$}\vss}}}$ is symmetric and thus an
equivalence. We show the following:

###### Lemma 7.3.

If $G$ is bidirected, then it is $i$-bidirected for each $i\in[0,k]$.

### Expressing emptiness using cosets

An important ingredient in our proof is to work with integer linear
_equations_ instead of inequalities. While solution sets of systems of
inequalities are semilinear sets in $\mathbb{Z}^{m}$, solution sets of
equation systems are cosets of $\mathbb{Z}^{m}$. Recall that a coset in
$\mathbb{Z}^{m}$ is a set of the form $\mathbf{u}+U$, where
$\mathbf{u}\in\mathbb{Z}^{m}$ and $U\subseteq\mathbb{Z}^{m}$ is a subgroup. In
this section, we will translate emptiness in bidirected grammars into a
problem about cosets of $\mathbb{Z}^{N\cup T}$. In general, we employ three
operations for constructing cosets. First, we can take $\mathbf{u}+\langle
S\rangle$ for $\mathbf{u}\in\mathbb{Z}^{N\cup T}$ and any set
$S\subseteq\mathbb{Z}^{N\cup T}$. Recall that $\langle S\rangle$ is the
subgroup generated by $S$. Second, if $C_{1},C_{2}\subseteq\mathbb{Z}^{N\cup
T}$ are cosets, then their point-wise sum $C_{1}+C_{2}$ is a coset, and the
set $C_{1}\cap C_{2}$ is either a coset or empty.

A central role will be played by the group $H_{a}$, which we define for each
$a\in R_{i}$:

(1) $H_{a}=\langle-b+\mathbf{u}\mid\text{$b\in R_{i}$ and
$b\,\Rightarrow_{i}\,\mathbf{u}$ and
$a\mathrel{\mathop{\leadsto}\limits^{\vbox
to0.0pt{\kern-2.0pt\hbox{$\scriptstyle*$}\vss}}}b$}\rangle$

Hence, $H_{a}$ is the group generated by all differences that are added when
applying derivation steps $b\,\Rightarrow_{i}\,\mathbf{u}$ for
$a\mathrel{\mathop{\leadsto}\limits^{\vbox
to0.0pt{\kern-2.0pt\hbox{$\scriptstyle*$}\vss}}}b$. We observe that if
$a\,\mathrel{\mathop{\Rightarrow}\limits^{\vbox
to0.0pt{\kern-2.0pt\hbox{$\scriptstyle*$}\vss}}}_{i}\,\mathbf{u}$, then
$-a+\mathbf{u}\in H_{a}$. We will need a coset to express that in such a
derivation, there are no level-$i$ letters (resp. no level-$i$ terminals)
left. We will do this by intersecting with the cosets

$S_{i}=\mathbb{Z}^{N_{[i+1,k]}\cup T_{[i+1,k]}},\hskip
5.69046ptS^{\prime}_{i}=\mathbb{Z}^{N_{[i+1,k]}}+\mathbb{Z}^{T_{[i,k]}}.$

Using $H_{a}$ and $S_{i}$, we can now define the coset that will essentially
characterize $L(a)$. For $a\in R_{i}$, we set

(2) $L_{a}=(a+H_{a})\cap S_{i}.$

One of the main results of this section will be that for $a\in R_{i}$, we can
describe $L(a)$ in terms of $L_{a}$. Following the theme that we can do things
only “up to differences in $\Delta_{a}$” on each level, we need a group
version of $\Delta_{a}$. For every $a\in N_{i}$, we have the subgroup
$D_{a}\subseteq\mathbb{Z}^{N_{i+1}}$, which we define next. If $a\in N_{i}$
with $i\in[0,k-1]$, we set $D_{a}=\langle b+{b}^{\dagger}\mid b\in
N_{i+1},~{}a\mathrel{\mathop{\leadsto}\limits^{\vbox
to0.0pt{\kern-2.0pt\hbox{$\scriptstyle*$}\vss}}}b\rangle$. For $a\in N_{k}$,
we define $D_{a}=\\{\mathbf{0}\\}$. In other words, $D_{a}$ is the group
generated by $\Delta_{a}$, for every $a\in N$. With this notation, one of the
crucial ingredients in our proof is to show that $L_{a}=L(a)+D_{a}$, i.e.
$L_{a}$ describes $L(a)$ up to differences in $D_{a}$ (see Theorem 7.4). By
our observation about $H_{a}$, it is obvious that $L(a)+D_{a}\subseteq L_{a}$.
The key step is that also $L_{a}\subseteq L(a)+D_{a}$.

While the cosets $L_{a}$ are coset versions of the sets $L(a)$, we will also
need coset versions of a slight variant of $L(a)$. For each $a\in R_{i}$, by
$M(a)$, we denote the vectors that are derivable from $a$, but may still
contain level-$i$ terminals:

$M(a)=\\{\mathbf{u}\in\mathbb{N}^{N_{[i+1,k]}}+\mathbb{Z}^{T_{[i,k]}}\mid
a\,\mathrel{\mathop{\Rightarrow}\limits^{\vbox
to0.0pt{\kern-2.0pt\hbox{$\scriptstyle*$}\vss}}}_{i}\,\mathbf{u}\\}.$

Thus, $M(a)$ differs from $L(a)$ by collecting all derivable
$\mathbf{u}\in\mathbb{N}^{N_{[i+1,k]}}+\mathbb{Z}^{T}$, where all level-$i$
nonterminals have been eliminated, but not necessarily all level-$i$
terminals, meaning $L(a)=M(a)\cap S_{i}$. Just as $L_{a}$ is a coset analogue
of $L(a)$, we have a coset analogue of $M(a)$:

$M_{a}=(a+H_{a})\cap S^{\prime}_{i}.$

The cosets $M_{a}$ will be needed to express, using cosets, whether $L(a)$ is
empty for nonterminals $a\in N_{i}$ that do not necessarily belong to $R_{i}$:
Those are the nonterminals for which we do not know whether $L(a)$ is empty.
Such sets $L(a)$ do not directly correspond to cosets. However, we will be
able to use cosets to characterize when $L(a)$ is empty. Here, we use the
cosets $K_{a}$ for $a\in N_{i}$, $i\in[0,k-1]$:

$K_{a}=(L_{a}+\langle-b+M_{b}\mid b\in
R_{i+1},~{}a\mathrel{\mathop{\leadsto}\limits^{\vbox
to0.0pt{\kern-2.0pt\hbox{$\scriptstyle*$}\vss}}}b\rangle)\cap S_{i+1}.$

We shall see that the coset $K_{a}$ corresponds to those vectors in
$\mathbb{N}^{N_{[i+1,k]}}+\mathbb{Z}^{T_{[i+1,k]}}$ that can be derived using
$a$. Using the cosets $K_{b}$ for $b\in N_{[0,k-1]}$, we will be able to
characterize emptiness of $L(a)$ for $a\in N_{[1,k]}$. In order to do the same
for $a\in N_{0}$, we need a final type of cosets. For each production
$a\to\mathbf{u}$ with $\mathbf{u}=b_{1}+\cdots+b_{n}+\mathbf{v}$ in our
grammar with $b_{1},\ldots,b_{n}\in N_{0}$ and $\mathbf{v}\in\mathbb{Z}^{T}$,
we define

$K_{a\to\mathbf{u}}=(M_{b_{1}}+\cdots+M_{b_{n}}+\mathbf{v})\cap S_{0}.$

The key ingredient in our proof is the following analogue of the translation
of (DBLP:conf/cade/VermaSS05, 37) to Presburger arithmetic. Here, we express
the set $L(a)$ of derivable vectors of a nonterminal $a$ as a coset.

###### Theorem 7.4.

If $G=(N,T,P)$ is bidirected, then $M(a)+D_{a}=M_{a}$ for every $a\in R$. In
particular, $L(a)+D_{a}=L_{a}$.

#### Intuition for the proof of Theorem 7.4

Before we sketch the proof, let us compare it with the construction of
(DBLP:conf/cade/VermaSS05, 37). They show that if we assign to each production
$p$ in a context-free grammar a number $\mathbf{x}(p)$ saying how often $p$ is
applied, then there is a derivation consistent with $\mathbf{x}$ if and only
if:

  1. (i)

each nonterminal is produced as many times as it is consumed (except for the
start-symbol, which is consumed once more) and

  2. (ii)

the participating nonterminals (i.e. for which $\mathbf{x}(p)>0$) must be
_connected_ : The latter means, for each nonterminal, it must be possible to
reach its consumed nonterminal by way of productions that occur in
$\mathbf{x}$.

Essentially, we will argue that for bidirected grammars, one can drop (ii).
This is because, independently of a particular derivation, each set $N_{i}$
decomposes into connected components with respect to
$\mathrel{\mathop{\leadsto}\limits^{\vbox
to0.0pt{\kern-2.0pt\hbox{$\scriptstyle*$}\vss}}}$. Then, instead of
stipulating connectedness of the set of used nonterminals, we only need all
used nonterminals to be in the same $\mathrel{\mathop{\leadsto}\limits^{\vbox
to0.0pt{\kern-2.0pt\hbox{$\scriptstyle*$}\vss}}}$-component. To construct a
derivation inside one $\mathrel{\mathop{\leadsto}\limits^{\vbox
to0.0pt{\kern-2.0pt\hbox{$\scriptstyle*$}\vss}}}$ component, we need to show
that there exist “connecting derivations” between each pair in
$\mathrel{\mathop{\leadsto}\limits^{\vbox
to0.0pt{\kern-2.0pt\hbox{$\scriptstyle*$}\vss}}}$. This is made precise in the
notion of Kirchhoff graphs, which we define next.

#### Kirchhoff graphs

Let $a\in R_{i}$. A _Kirchhoff graph for $a$_ is a directed graph whose set of
vertices is $\\{b\in R_{i}\mid a\mathrel{\mathop{\leadsto}\limits^{\vbox
to0.0pt{\kern-2.0pt\hbox{$\scriptstyle*$}\vss}}}b\\}$, such that there exists
an edge $(b,c)$ for each $b,c\in R_{i}$ with
$a\mathrel{\mathop{\leadsto}\limits^{\vbox
to0.0pt{\kern-2.0pt\hbox{$\scriptstyle*$}\vss}}}b$ and
$a\mathrel{\mathop{\leadsto}\limits^{\vbox
to0.0pt{\kern-2.0pt\hbox{$\scriptstyle*$}\vss}}}c$, and where an edge $(b,c)$
is weighted by an element
$\mathbf{g}_{b,c}\in\mathbb{N}^{N_{[i+1,k]}}+\mathbb{Z}^{T_{[i+1,k]}}$ such
that the following holds:

  1. (i)

$b\,\mathrel{\mathop{\Rightarrow}\limits^{\vbox
to0.0pt{\kern-2.0pt\hbox{$\scriptstyle*$}\vss}}}_{i}\,c+\mathbf{g}_{b,c}$ for
every $b,c$,

  2. (ii)

$\mathbf{g}_{b,b}=\mathbf{0}$ for every $b$, and

  3. (iii)

for any vertices $b,c,d$, we have
$\mathbf{g}_{b,c}+\mathbf{g}_{c,d}\approx_{a}\mathbf{g}_{b,d}$.

The term stems from the fact that these graphs satisfy (up to $\approx_{a}$) a
condition like Kirchhoff’s law on voltage drops: The weight sum of every cycle
is zero. In our case, adding up the $\mathbf{g}_{b,c}$ along a cycle will
yield zero up to $\approx_{a}$. This implies the following property:

###### Lemma 7.5.

If $e_{1},\ldots,e_{\ell},f_{1},\ldots,f_{\ell}\in R_{i}$ satisfy
$a\mathrel{\mathop{\leadsto}\limits^{\vbox
to0.0pt{\kern-2.0pt\hbox{$\scriptstyle*$}\vss}}}e_{j}$ and
$a\mathrel{\mathop{\leadsto}\limits^{\vbox
to0.0pt{\kern-2.0pt\hbox{$\scriptstyle*$}\vss}}}f_{j}$ for
$j\in\\{1,\ldots,\ell\\}$ and $\pi$ is a permutation of $\\{1,\ldots,\ell\\}$,
then in a Kirchhoff graph for $a$, we have

$\mathbf{g}_{e_{1},f_{1}}+\cdots+\mathbf{g}_{e_{\ell},f_{\ell}}\approx_{a}\mathbf{g}_{e_{1},f_{\pi(1)}}+\cdots+\mathbf{g}_{e_{\ell},f_{\pi(\ell)}}.$

###### Proof.

Let us first observe that for any $e\in\\{e_{1},\ldots,e_{\ell}\\}$ and
$f\in\\{f_{1},\ldots,f_{\ell}\\}$, the relation

$\displaystyle\mathbf{g}_{e,f}+\mathbf{g}_{e^{\prime},f^{\prime}}$
$\displaystyle\approx_{a}(\mathbf{g}_{e,e^{\prime}}+\mathbf{g}_{e^{\prime},f})+(\mathbf{g}_{e^{\prime},e}+\mathbf{g}_{e,f^{\prime}})$
$\displaystyle\approx_{a}(\mathbf{g}_{e,e^{\prime}}+\mathbf{g}_{e^{\prime},e})+(\mathbf{g}_{e^{\prime},f}+\mathbf{g}_{e,f^{\prime}})$
$\displaystyle\approx_{a}\mathbf{g}_{e^{\prime},f}+\mathbf{g}_{e,f^{\prime}}$

follows from the definition of Kirchhoff graphs. This is the case of

(3)
$\mathbf{g}_{e_{1},f_{1}}+\cdots+\mathbf{g}_{e_{\ell},f_{\ell}}\approx_{a}\mathbf{g}_{e_{1},f_{\pi(1)}}+\cdots+\mathbf{g}_{e_{\ell},f_{\pi(\ell)}}$

where $\pi$ is a transposition, i.e. a permutation that swaps two points and
lets all others fixed. Since every permutation of $\\{1,\ldots,\ell\\}$ can be
written as a composition of several transpositions, Eq. 3 follows in full
generality. ∎

###### Lemma 7.6.

If $G$ is $i$-bidirected, then for each $a\in R_{i}$, there exists a Kirchhoff
graph for $a$.

###### Proof.

Write $\\{b\in R_{i}\mid a\mathrel{\mathop{\leadsto}\limits^{\vbox
to0.0pt{\kern-2.0pt\hbox{$\scriptstyle*$}\vss}}}b\\}=\\{b_{1},\ldots,b_{n}\\}$.
To simplify notation, we write $\mathbf{g}_{r,s}$ instead of
$\mathbf{g}_{b_{r},b_{s}}$. We have to pick $\mathbf{g}_{j,j}=\mathbf{0}$.
Since $G$ is $i$-bidirected, we know that
$\mathrel{\mathop{\leadsto}\limits^{\vbox
to0.0pt{\kern-2.0pt\hbox{$\scriptstyle*$}\vss}}}$ is symmetric. In particular,
for any $j\in[1,n-1]$, there exists a $\mathbf{g}_{j,j+1}$ such that
$b_{j}\,\mathrel{\mathop{\Rightarrow}\limits^{\vbox
to0.0pt{\kern-2.0pt\hbox{$\scriptstyle*$}\vss}}}_{i}\,b_{j+1}+\mathbf{g}_{j,j+1}$.
Moreover, $i$-bidirectedness of $G$ guarantees that there exists a
$\mathbf{g}_{j+1,j}$ with
$\mathbf{g}_{j+1,j}\approx_{b_{j}}{\mathbf{g}_{j,j+1}}^{\dagger}$ such that
$b_{j+1}\,\mathrel{\mathop{\Rightarrow}\limits^{\vbox
to0.0pt{\kern-2.0pt\hbox{$\scriptstyle*$}\vss}}}_{i}\,b_{j}+\mathbf{g}_{j+1,j}$.
Note that since $a\mathrel{\mathop{\leadsto}\limits^{\vbox
to0.0pt{\kern-2.0pt\hbox{$\scriptstyle*$}\vss}}}b_{j}$ and
$\mathrel{\mathop{\leadsto}\limits^{\vbox
to0.0pt{\kern-2.0pt\hbox{$\scriptstyle*$}\vss}}}$ is symmetric, we have
$\Delta_{b_{j}}=\Delta_{a}$ and thus
$\mathbf{g}_{j+1,j}\approx_{a}{\mathbf{g}_{j,j+1}}^{\dagger}$. Finally, for
$r,s\in[1,n]$ with $r<s$, we pick
$\mathbf{g}_{r,s}=\mathbf{g}_{r,r+1}+\cdots+\mathbf{g}_{s-1,s}$ and similarly
$\mathbf{g}_{s,r}=\mathbf{g}_{s,s-1}+\cdots+\mathbf{g}_{r+1,r}$.

Let us now show that this is indeed a Kirchhoff graph for $a$. We clearly have
$b_{r}\,\mathrel{\mathop{\Rightarrow}\limits^{\vbox
to0.0pt{\kern-2.0pt\hbox{$\scriptstyle*$}\vss}}}_{i}\,b_{s}+\mathbf{g}_{r,s}$
for any $r,s\in[1,n]$. It remains to show that

$\mathbf{g}_{r,s}+\mathbf{g}_{s,t}\approx_{a}\mathbf{g}_{r,t}$

for any $r,s,t\in[1,n]$. It suffices to do this in the case that $|s-t|=1$,
because the other cases follow by induction. Consider the case $t=s+1$ (the
case $s=t+1$ is analogous). We have to show that

$\mathbf{g}_{r,s}+\mathbf{g}_{s,s+1}\approx_{a}\mathbf{g}_{r,s+1}.$

If $r\leq s$, then both sides are identical by definition. If $r>s$, then
$\mathbf{g}_{r,s}$ is defined as
$\mathbf{g}_{r,s}=\mathbf{g}_{r,s+1}+\mathbf{g}_{s+1,s}$. By the choice of
$\mathbf{g}_{s+1,s}$, we know that
$\mathbf{g}_{s+1,s}\approx_{a}{\mathbf{g}_{s,s+1}}^{\dagger}$ and thus
$\mathbf{g}_{s+1,s}+\mathbf{g}_{s,s+1}\approx_{a}\mathbf{0}$. Hence:

$\mathbf{g}_{r,s}+\mathbf{g}_{s,s+1}=\mathbf{g}_{r,s+1}+\mathbf{g}_{s+1,s}+\mathbf{g}_{s,s+1}\approx_{a}\mathbf{g}_{r,s+1}.\qed$

For Theorem 7.4, we need two additional lemmas. The first follows from
property (5) and induction on $i$.

###### Lemma 7.7.

For bidirected $G=(N,T,P)$ and $a\in R_{i}$, we have $D_{a}\subseteq H_{a}$.

Next observe that $L_{a}$ contains vectors obtained by adding, but also
_subtracting_ effects of derivation steps. We now show that if our grammar is
$i$-bidirected, then each such subtraction can be realized by a sequence of
ordinary derivation steps: The lemma says that every element of $H_{a}$ can be
written as a positive sum of derivation effects (up to a difference in
$D_{a}$).

###### Lemma 7.8.

If $G$ is $i$-bidirected, then

$H_{a}=\\{-b+\mathbf{u}\mid\exists b\in R_{i}\colon
b\,\Rightarrow_{i}\,\mathbf{u}~{}\text{and}~{}a\mathrel{\mathop{\leadsto}\limits^{\vbox
to0.0pt{\kern-2.0pt\hbox{$\scriptstyle*$}\vss}}}b\\}^{*}+D_{a}$

for every $a\in R_{i}$

Here, $F^{*}$ denotes the submonoid of $\mathbb{Z}^{N\cup T}$ generated by the
set $F$. We are now ready to prove Theorem 7.4.

###### Proof of Theorem 7.4.

We begin with the inclusion “$\subseteq$”. A simple induction on the length of
a derivation shows that every element of $M(a)$ belongs to $M_{a}$. Lemma 7.7
tells us that $D_{a}\subseteq H_{a}$, and since $D_{a}\subseteq S_{i}$, this
implies $M_{a}+D_{a}\subseteq M_{a}$, hence $M(a)+D_{a}\subseteq M_{a}$.

We now prove “$\supseteq$”. An element of $M_{a}$ is of the form
$a+\mathbf{v}$ with $\mathbf{v}\in H_{a}$ and $a+\mathbf{v}\in
S^{\prime}_{i}$. We claim that then $a+\mathbf{v}$ belongs to $M(a)+D_{a}$.
Since $\mathbf{v}\in H_{a}$, Lemma 7.8 tells us that

$\mathbf{v}=\sum_{j=1}^{n}-b_{j}+\mathbf{u}_{j}+\mathbf{x}_{j}$

with $b_{j}\in R_{i}$, $a\mathrel{\mathop{\leadsto}\limits^{\vbox
to0.0pt{\kern-2.0pt\hbox{$\scriptstyle*$}\vss}}}b_{j}$,
$\mathbf{u}_{j}\in\mathbb{N}^{R_{i}}$,
$\mathbf{x}_{j}\in\mathbb{N}^{N_{[i+1,k]}}+\mathbb{Z}^{T_{[i,k]}}$ where
$b_{j}\,\Rightarrow_{i}\,\mathbf{u}_{j}+\mathbf{x}_{j}$ for $j\in[1,n]$.

Since $G$ is $i$-bidirected by Lemma 7.3, Lemma 7.6 yields a Kirchhoff graph
for $a$ with weights $\mathbf{g}_{b,c}$ for any $b,c\in R_{i}$ with
$a\mathrel{\mathop{\leadsto}\limits^{\vbox
to0.0pt{\kern-2.0pt\hbox{$\scriptstyle*$}\vss}}}b$ and
$a\mathrel{\mathop{\leadsto}\limits^{\vbox
to0.0pt{\kern-2.0pt\hbox{$\scriptstyle*$}\vss}}}c$. Let us now construct a
derivation in $G$. Without loss of generality, we may assume that
$\mathbf{u}_{1},\ldots,\mathbf{u}_{\ell}\neq\mathbf{0}$ and
$\mathbf{u}_{\ell+1}=\cdots=\mathbf{u}_{n}=\mathbf{0}$. For each
$j\in[1,\ell]$, we pick some nonterminal $c_{j}\in R_{i}$ such that $c_{1}=a$
and $\mathbf{u}_{j-1}(c_{j})>0$ for $j\in[2,\ell]$. By our choice of the
$\mathbf{g}$’s, we can now derive as follows. We use the derivation steps
$b_{j}\,\Rightarrow_{i}\,\mathbf{u}_{j}+\mathbf{x}_{j}$. But since it is
possible that $b_{j+1}\,\Rightarrow_{i}\,\mathbf{u}_{j+1}+\mathbf{x}_{j+1}$
cannot be applied after
$b_{j}\,\Rightarrow_{i}\,\mathbf{u}_{j}+\mathbf{x}_{j}$, we use derivations
$c_{j}\,\mathrel{\mathop{\Rightarrow}\limits^{\vbox
to0.0pt{\kern-2.0pt\hbox{$\scriptstyle*$}\vss}}}_{i}\,b_{j}+\mathbf{g}_{c_{j},b_{j}}$
as connecting derivations. Here, we think of the $\mathbf{g}_{c_{j},b_{j}}$ as
“garbage” that we produce in order to use the connecting derivations.
Afterwards, we will cancel out these garbage elements. We begin with a
connecting derivation in order to apply
$b_{1}\,\Rightarrow_{i}\,\mathbf{u}_{1}+\mathbf{x}_{1}$:

$\displaystyle a=c_{1}$
$\displaystyle\,\mathrel{\mathop{\Rightarrow}\limits^{\vbox
to0.0pt{\kern-2.0pt\hbox{$\scriptstyle*$}\vss}}}_{i}\,b_{1}+\mathbf{g}_{c_{1},b_{1}}$
$\displaystyle\,\Rightarrow_{i}\,\mathbf{u}_{1}+\mathbf{x}_{1}+\mathbf{g}_{c_{1},b_{1}}=a+(-c_{1}+\mathbf{u}_{1})+\mathbf{g}_{c_{1},b_{1}}.$

Since $c_{2}$ must occur in
$a+(-c_{1}+\mathbf{u}_{1}+\mathbf{x}_{1})+\mathbf{g}_{c_{1},b_{1}}$, we can
apply $c_{2}\,\mathrel{\mathop{\Rightarrow}\limits^{\vbox
to0.0pt{\kern-2.0pt\hbox{$\scriptstyle*$}\vss}}}_{i}\,b_{2}+\mathbf{g}_{c_{2},b_{2}}$,
etc. Doing this $\ell$ times yields

$a\,\mathrel{\mathop{\Rightarrow}\limits^{\vbox
to0.0pt{\kern-2.0pt\hbox{$\scriptstyle*$}\vss}}}_{i}\,a+\sum_{j=1}^{\ell}-c_{j}+\mathbf{u}_{j}+\mathbf{x}_{j}+\mathbf{g}_{c_{j},b_{j}}.$

Let us denote the sum on the right-hand side by $\mathbf{y}$. Since want to
derive $a+\sum_{j=1}^{\ell}(-b_{j}+\mathbf{u}_{j}+\mathbf{x}_{j})$ instead of
$a+\mathbf{y}$, we now need to correct two aspects: (i) Our derivation
subtracted $c_{1},\ldots,c_{\ell}$ instead of $b_{1},\ldots,b_{\ell}$, so we
need to add $c$’s and subtract $b$’s and (ii) we need to cancel out the
garbage elements $\mathbf{g}_{c_{j},b_{j}}$. When replacing $b$’s by $c$’s, it
could be that some $c$’s are equal to $b$’s, so for (i), we don’t have to
change those. So we pick a permutation $\pi$ of $\\{1,\ldots,\ell\\}$ and a
number $r\in[1,\ell]$ so that (a) $c_{j}=b_{\pi(j)}$ for $j\in[1,r]$ and (b)
$\\{b_{\pi(r+1)},\ldots,b_{\pi(\ell)}\\}$ and $\\{c_{r+1},\ldots,c_{\ell}\\}$
are disjoint. Now observe that the nonterminals
$\\{b_{\pi(r+1)},\ldots,b_{\pi(\ell)}\\}$ are never consumed in the derivation
arriving at $a+\mathbf{y}$. However, since $a+\mathbf{v}\in S_{i}$, we know
that $b_{1}+\cdots+b_{\ell}$ must occur in $\sum_{j=1}^{\ell}\mathbf{u}_{j}$.
Therefore, in particular $b_{\pi(r+1)}+\cdots+b_{\pi(\ell)}$ must occur in
$\mathbf{y}$. But this means we can, for each $j\in[r+1,\ell]$, apply the
derivation $b_{\pi(j)}\,\mathrel{\mathop{\Rightarrow}\limits^{\vbox
to0.0pt{\kern-2.0pt\hbox{$\scriptstyle*$}\vss}}}_{i}\,c_{j}+\mathbf{g}_{b_{\pi(j)},c_{j}}$
to $\mathbf{y}$ (in any order). Thus, from $a$, using
$\,\mathrel{\mathop{\Rightarrow}\limits^{\vbox
to0.0pt{\kern-2.0pt\hbox{$\scriptstyle*$}\vss}}}_{i}\,$, we can derive

$\displaystyle
a+\sum_{j=1}^{\ell}-c_{j}+\mathbf{u}_{j}+\mathbf{x}_{j}+\mathbf{g}_{c_{j},b_{j}}+\sum_{j=r+1}^{\ell}-b_{\pi(j)}+c_{j}+\mathbf{g}_{b_{\pi(j)},c_{j}}$
$\displaystyle=a+\sum_{j=1}^{\ell}-b_{j}+\mathbf{u}_{j}+\mathbf{x}_{j}+\left(\sum_{j=1}^{\ell}\mathbf{g}_{c_{j},b_{j}}+\sum_{j=r+1}^{\ell}\mathbf{g}_{b_{\pi(j)},c_{j}}\right).$

Moreover, since $a+\mathbf{v}\in S_{i}$, we know that
$b_{\ell+1}+\cdots+b_{n}$ must occur in
$\sum_{j=1}^{\ell}-b_{j}+\mathbf{u}_{j}+\mathbf{x}_{j}$, and so we can just
apply the steps $b_{j}\,\Rightarrow_{i}\,\mathbf{u}_{j}+\mathbf{x}_{j}$ for
$j\in[\ell+1,n]$ in any order to obtain:

$a\,\mathrel{\mathop{\Rightarrow}\limits^{\vbox
to0.0pt{\kern-2.0pt\hbox{$\scriptstyle*$}\vss}}}_{i}\,a+\sum_{j=1}^{n}-b_{j}+\mathbf{u}_{j}+\mathbf{x}_{j}+\left(\sum_{j=1}^{\ell}\mathbf{g}_{c_{j},b_{j}}+\sum_{j=r+1}^{\ell}\mathbf{g}_{b_{\pi(j)},c_{j}}\right).$

Now since $a+\mathbf{v}\in S^{\prime}_{i}$, the right-hand side contains no
more level-$i$ nonterminals. Hence, the right-hand side belongs to $M(a)$.
Finally, since $\pi(j)=j$ for $j\in[1,r]$ and
$\mathbf{g}_{c_{j},c_{j}}\approx\mathbf{0}$ for $j\in[1,\ell]$, the term in
parentheses belongs to $D_{a}$ by Lemma 7.5. Hence, $a+\mathbf{v}\in
M(a)+D_{a}$.

Finally, note that $L(a)+D_{a}=L_{a}$ follows from $M(a)+D_{a}=M_{a}$, because
$D_{a}\subseteq S_{i}$ and thus $L(a)+D_{a}=(M(a)\cap
S_{i})+D_{a}=(M(a)+D_{a})\cap S_{i}=M_{a}\cap S_{i}=L_{a}$. ∎

While Theorem 7.4 describes what nonterminals $a\in R_{i}$ can derive, we also
need an analogue $a\in N_{i}\setminus R_{i}$. It is a straightforward
consequence of previous steps:

###### Corollary 7.9.

Suppose $G$ is $i$-bidirected. (1) For $a\in N_{i}$ for $i\in[1,k]$, we have
$L(a)\neq\emptyset$ iff there is some $a^{\prime}\in N_{i-1}$ and a production
$a\to a^{\prime}$ such that $K_{a^{\prime}}\neq\emptyset$. (2) For $a\in
N_{0}$, we have $L(a)\neq\emptyset$ iff there is some production
$a\to\mathbf{u}$ with $\mathbf{u}\in\mathbb{N}^{N_{0}}+\mathbb{Z}^{T}$ such
that $K_{a\to\mathbf{u}}\neq\emptyset$.

### Constructing coset circuits

We will express our cosets in compact representations called _coset circuits_.
Let $Y$ be a finite set. A _matrix representation_ of a coset
$S\subseteq\mathbb{Z}^{Y}$ is a matrix $\mathbf{A}\in\mathbb{Z}^{X\times Z}$
and a vector $\mathbf{b}\in\mathbb{Z}^{X}$ such that $Y\subseteq Z$ and
$S=\\{\pi_{Y}(\mathbf{x})\mid\mathbf{A}\mathbf{x}=\mathbf{b}\\}$, where
$\pi_{Y}\colon\mathbb{Z}^{Z}\to\mathbb{Z}^{Y}$ is the projection onto
$\mathbb{Z}^{Y}$. Note that for a coset given as
$S=\mathbf{v}+\langle\mathbf{u}_{1},\ldots,\mathbf{u}_{n}\rangle$, we can
directly compute a matrix representation. A _coset circuit over
$\mathbb{Z}^{Y}$_ is a directed acyclic graph $C$, whose vertices are called
_gates_ and

  1. (1)

Leaves, i.e. gates $g$ with in-degree $0$, are labeled by a matrix
representation of a coset $C(g)$.

  2. (2)

Gates with in-degree $>0$ are labeled by $+$ or $\cap$.

In a coset circuit, each gate $g$ evaluates to a coset $C(g)$ of
$\mathbb{Z}^{Y}$ (or the empty set): The leaves evaluate to their labels. A
gate $g$ with incoming edges from $g_{1},\ldots,g_{m}$, $m\geq 1$, evaluates
to either $C(g_{1})+\cdots+C(g_{m})$ or $C(g_{1})\cap\cdots\cap C(g_{m})$
depending on whether $v$’s label is $+$ or $\cap$.

We will construct a coset circuit that has for each $a\in N$, a gate for
$H_{a},L_{a},M_{a},K_{a}$ and also for $K_{a\to\mathbf{u}}$ for productions
$a\to\mathbf{u}\in P$. By Corollary 7.9, this lets us check emptiness of
$L(a)$ for each $a\in N$. For $H_{a},L_{a},K_{a\to\mathbf{u}}$ with $a\in
N_{0}$, we can directly create leaves with matrix representations. For the
others, the definitions do not tell us directly how to compute the cosets
using sums and intersections, e.g.: $H_{a}$ is defined by a (potentially
infinite) generating set. Thus, we first show that $H_{a}$ is generated by
finitely many cosets.

###### Lemma 7.10.

Let $G=(N,T,P)$ be a bidirected $k$-grammar. For every $a\in R_{i}$,
$i\in[1,k]$, we have

$H_{a}=\langle-b+L_{c}\mid b\in R_{i},c\in
R_{i-1},a\mathrel{\mathop{\leadsto}\limits^{\vbox
to0.0pt{\kern-2.0pt\hbox{$\scriptstyle*$}\vss}}}b,b\to c\in P\rangle.$

###### Proof.

By definition, we have $H_{a}=\langle-b+L(c)\mid b\in R_{i},c\in
R_{i-1},a\mathrel{\mathop{\leadsto}\limits^{\vbox
to0.0pt{\kern-2.0pt\hbox{$\scriptstyle*$}\vss}}}b,b\to c\in P\rangle$. Since
Theorem 7.4 tells us that $L_{c}=L(c)+D_{c}$, the inclusion “$\subseteq$” is
immediate. For “$\supseteq$”, because of $L(c)+D_{c}$, we shall prove that
$D_{c}\subseteq H_{a}$. (Note that this is not an immediate consequence of
Lemma 7.7, because $a\in R_{i}$ and $c\in R_{i-1}$ are on different levels).

For $D_{c}\subseteq H_{a}$, it suffices to prove that every generator
$e+{e}^{\dagger}$ with $e\in R_{i}$,
$c\mathrel{\mathop{\leadsto}\limits^{\vbox
to0.0pt{\kern-2.0pt\hbox{$\scriptstyle*$}\vss}}}e$, of $D_{c}$ belongs to
$H_{a}$. Since $c\mathrel{\mathop{\leadsto}\limits^{\vbox
to0.0pt{\kern-2.0pt\hbox{$\scriptstyle*$}\vss}}}e$, $e$ appears on a right-
hand side of a production and thus $L(e)\neq\emptyset$. Hence, there is some
$\mathbf{u}\in\mathbb{Z}^{N_{[i+1,k]}\cup T}$ with
$e\,\mathrel{\mathop{\Rightarrow}\limits^{\vbox
to0.0pt{\kern-2.0pt\hbox{$\scriptstyle*$}\vss}}}_{i}\,\mathbf{u}$. This
implies that $e+{e}^{\dagger}\,\mathrel{\mathop{\Rightarrow}\limits^{\vbox
to0.0pt{\kern-2.0pt\hbox{$\scriptstyle*$}\vss}}}_{i}\,\mathbf{u}+{\mathbf{u}}^{\dagger}$.
Since $\mathbf{u}+{\mathbf{u}}^{\dagger}\in D_{a}\subseteq H_{a}$ (Lemma 7.7)
and $e+{e}^{\dagger}-(\mathbf{u}+{\mathbf{u}}^{\dagger})\in H_{a}$, this
proves that $e+{e}^{\dagger}\in H_{a}$. ∎

This is a straightforward consequence of Theorem 7.4. We have now described
each coset in terms of other cosets using sum, intersection, but also
_generated subgroup_ (such as in Lemma 7.10). In order to describe cosets only
using sums and intersections, we use:

###### Lemma 7.11.

Let $g_{1},\ldots,g_{n}\in\mathbb{Z}^{m}$ and let $U,S\subseteq\mathbb{Z}^{m}$
be subgroups with $(g_{i}+U)\cap S\neq\emptyset$ for all $i\in[1,n]$. Then

(4) $\langle(g_{1}+U)\cap S,\ldots,(g_{n}+U)\cap S\rangle=(\langle
g_{1},\ldots,g_{n}\rangle+U)\cap S.$

In other words, Lemma 7.11 says that instead of imposing the condition of
belonging to $S$ _locally_ at each summand $g_{i}+U$, it suffices to impose it
_globally_ on the sum $\langle g_{1},\ldots,g_{n}\rangle+U$.

###### Proof of Lemma 7.11.

The inclusion “$\subseteq$” is obvious because $U$ and $S$ are subgroups.
Conversely, suppose $h=x_{1}g_{1}+\cdots+x_{n}g_{n}+u\in S$ for some
$x_{1},\ldots,x_{n}\in\mathbb{Z}$ and $u\in U$. Since $(g_{i}+U)\cap
S\neq\emptyset$, we can choose $u_{i}\in U$ for each $i\in[1,n]$ such that
$g_{i}+u_{i}\in S$. We compute in the quotient $A/S$. Note that since $h\in S$
and $g_{i}+u_{i}\in S$, we have
$[u]=-[x_{1}g_{1}+\cdots+x_{n}g_{n}]=[x_{1}u_{1}+\cdots+x_{n}u_{n}]$ and thus
$u-x_{1}u_{1}-\cdots-x_{n}u_{n}\in S$. Therefore, we have

(5)
$\displaystyle\begin{split}h=\underbrace{x_{1}(g_{1}+u_{1})}_{\in\langle(g_{1}+U)\cap
S\rangle}&~{}+~{}\cdots~{}+~{}\underbrace{x_{n}(g_{n}+u_{n})}_{\in\langle(g_{n}+U)\cap
S\rangle}\\\ &~{}+~{}\underbrace{u-x_{1}u_{1}-\cdots-x_{n}u_{n}}_{\in U\cap
S}.\end{split}$

This proves that $h$ belongs to the left-hand side of Eq. 4, since that set is
closed under adding $U\cap S$. ∎

Hence, if we have built gates for $U$ and $S$ and are given vectors
$g_{1},\ldots,g_{n}$, then to create a gate for
$\langle(g_{1}+U),\ldots,(g_{n}+U)\rangle\cap S$, we can create one for
$(\langle g_{1},\ldots,g_{n}\rangle+U)\cap S$. Since we can directly compute a
matrix representation for $\langle g_{1},\ldots,g_{n}\rangle$, we can
introduce a leaf for this subgroup.

Let us now describe how, using Lemma 7.11, each coset can be expressed using
only sums and intersection. To simplify notation, for any $a\in N_{i}$, we
write $P_{a}=\\{(b,c)\mid b\in N_{i},c\in
N_{i-1},a\mathrel{\mathop{\leadsto}\limits^{\vbox
to0.0pt{\kern-2.0pt\hbox{$\scriptstyle*$}\vss}}}b,b\to c\in P\\}$. Note that

$\displaystyle H_{a}$ $\displaystyle=\langle-b+\mathbf{u}\mid
a\mathrel{\mathop{\leadsto}\limits^{\vbox
to0.0pt{\kern-2.0pt\hbox{$\scriptstyle*$}\vss}}}b,~{}b\to\mathbf{u}\in
P\rangle$ $\displaystyle\text{for $a\in R_{0}$},$ $\displaystyle H_{a}$
$\displaystyle=\langle-b+L_{c}\mid(b,c)\in P_{a}\rangle$
$\displaystyle\text{for $a\in R_{[1,k]}$}.$

Thus, for $a\in R_{0}$, we have a finite generating set for $H_{a}$ given
explicitly in the grammar and can thus create a leaf gate for $H_{a}$ labeled
by an explicit matrix representation for $H_{a}$. However, for $a\in
R_{[1,k]}$, we need to eliminate the the $\langle\cdot\rangle$ operator. To
this end, we write

(6) $\begin{split}H_{a}&=\langle-b+L_{c}\mid(b,c)\in P_{a}\rangle\\\
&=\sum_{(b,c)\in P_{a}}\langle(-b+c+H_{c})\cap S_{i-1}\rangle\\\
&=\sum_{(b,c)\in P_{a}}(\langle-b+c\rangle+H_{c})\cap S_{i-1}\end{split}$

where in the first step, we plug in the definition of $L_{c}$ and in the
second step, we apply Lemma 7.11. Here, the sum on the right only uses those
$(b,c)\in P_{a}$ for which $(\langle-b+c\rangle+H_{c})\cap
S_{i-1}\neq\emptyset$. Now, each $\langle-b+c\rangle$ is a group for which we
can create a gate with an explicit representation.

We also need to express $K_{a}$ in terms of sum and intersection. First note
that for $b\in R_{i+1}$,

(7) $\begin{split}\langle-b+M_{b}\rangle&=\langle-b+((b+H_{b})\cap
S^{\prime}_{i+1})\rangle\\\ &=\langle(-b+S^{\prime}_{i+1})\cap H_{b}\rangle\\\
&=H_{b}\cap\langle-b+S^{\prime}_{i+1}\rangle\end{split}$

provided that $(-b+S^{\prime}_{i+1})\cap H_{b}\neq\emptyset$; otherwise,
$\langle-b+M_{b}\rangle$ is the trivial group $\\{\mathbf{0}\\}$. In the first
equality, we plug in the definition of $M_{b}$. The second is due to the
definition of $S^{\prime}_{i+1}$, and the third applies Lemma 7.11, relying on
$(-b+S^{\prime}_{i+1})\cap H_{b}$ being non-empty. This implies that for $a\in
N_{i}$,

(8) $\begin{split}K_{a}&=(L_{a}+\langle-b+M_{b}\mid b\in
R_{i+1},a\mathrel{\mathop{\leadsto}\limits^{\vbox
to0.0pt{\kern-2.0pt\hbox{$\scriptstyle*$}\vss}}}b\rangle)\cap S_{i+1}\\\
&=\left(L_{a}+\sum_{b\in R_{i+1},a\mathrel{\mathop{\leadsto}\limits^{\vbox
to0.0pt{\kern-2.0pt\hbox{$\scriptstyle*$}\vss}}}b}\langle-b+M_{b}\rangle\right)\cap
S_{i+1}\\\ &=\left(L_{a}+\sum_{b\in
R_{i+1},a\mathrel{\mathop{\leadsto}\limits^{\vbox
to0.0pt{\kern-2.0pt\hbox{$\scriptstyle*$}\vss}}}b}H_{b}\cap\langle-b+S^{\prime}_{i+1}\rangle\right)\cap
S_{i+1},\end{split}$

where the last sum only uses those
$H_{b}\cap\langle-b+S^{\prime}_{i+1}\rangle$ for which
$(-b+S^{\prime}_{i+1})\cap H_{b}\neq\emptyset$. The equality follows from the
definition of $K_{a}$ and Eq. 7. Note that for $-b+S^{\prime}_{i+1}$, it is
again easy to construct a matrix representation.

Finally, observe that all these coset definitions rely on the relation
$\leadsto$. On $N_{0}$, we can compute $\leadsto$ directly. On $N_{[1,k]}$, we
have to rely on cosets. To this, note that for $a,b\in N_{i}$, we have
$a\leadsto b$ if and only if there is a $c\in R_{i-1}$ with a production $a\to
c$ and some $\mathbf{u}\in L_{c}$ with $\mathbf{u}(b)=1$. In other words, if
and only if $L_{c}\cap O_{b}\neq\emptyset$, where $O_{b}$ is the coset
$\\{\mathbf{u}\in\mathbb{Z}^{N\cup T}\mid\mathbf{u}(b)=1\\}$.

Input : Bidirected $k$-grammar $G=(N,T,P)$

Create gates for $S_{i}$, $S^{\prime}_{i}$, $O_{a}$, and $\langle-a+b\rangle$
for each $i\in[1,k]$, $a,b\in N$

Compute $\leadsto$ on $N_{0}$

Create gates for $H_{a}$, $L_{a}$, and $M_{a}$ for each $a\in R_{0}$

Create gates for $K_{a\to\mathbf{u}}$ for productions $a\to\mathbf{u}$, $a\in
N_{0}$, $\mathbf{u}\in\mathbb{N}^{N_{0}}+\mathbb{Z}^{T}$

for  _$i=1,\ldots,k$_ do

Create gate for $L_{c}\cap O_{b}$ for each $c\in R_{i-1}$, $b\in N_{i}$

Compute the relation $\leadsto$ on $N_{i}$ based on non-emptiness of
$L_{c}\cap O_{b}$ with $c\in N_{i-1}$, $b\in N_{i}$

Compute $\mathrel{\mathop{\leadsto}\limits^{\vbox
to0.0pt{\kern-2.0pt\hbox{$\scriptstyle*$}\vss}}}$ on $N_{i}$ and then $P_{a}$
for each $a\in N_{i}$

Create gate for $H_{a}$, then for $L_{a}$, then for $M_{a}$ for each $a\in
R_{i}$ according to Eqs. 6, 2 and 8

Create gate for $K_{a}$ for each $a\in R_{i-1}$

Algorithm 1 Construction of coset circuit for a bidirected $k$-grammar

The exact order in which the gates are constructed is given in Algorithm 1. We
observe that the constructed coset circuit has depth $\leq ck$ for some
constant $c$: The gates for $H_{a}$, $L_{a}$, $M_{a}$ only depend on gates
created in the last iteration of the for-loop. Moreover, each of them only
adds a constant depth to the gates produced before. The gates $K_{a}$ depend
on gates $H_{b}$ created in the same iteration, thus also adding only constant
depth. Finally, note that the entries in the matrices in the labels of the
leaves require at most polynomially many bits: The gates for $S_{i}$,
$S^{\prime}_{i}$, $O_{a}$, $\langle-a+b\rangle$ and for $H_{a}$, $L_{a}$, and
$M_{a}$ for $a\in R_{0}$ are obtained directly from the productions of $G$.
The numbers in those, in turn, have at most polynomially many bits as they are
computed using Theorem 6.5.

### From coset circuits to equations

In each of our three algorithms for $\mathsf{BIREACH}$, we check emptiness of
coset circuits by translating them into integer linear equation systems. Let
$n=|Y|$. We compute, for each gate $g$, a matrix
$\mathbf{A}_{g}\in\mathbb{Z}^{s_{g}\times t_{g}}$ and a vector
$\mathbf{b}_{g}\in\mathbb{Z}^{s_{g}}$ such that
$C(g)=\\{\pi_{n}(\mathbf{x})\mid\mathbf{x}\in\mathbb{Z}^{t_{g}},~{}\mathbf{A}_{g}\mathbf{x}=\mathbf{b}_{g}\\}$,
where for any $r\in\mathbb{N}$, by $\pi_{n}$, we denote the projection
$\pi_{n}\colon\mathbb{Z}^{r}\to\mathbb{Z}^{n}$ onto the last $n$ coordinates
for any $r\geq n$. If $g$ has in-degree $0$, then $g$ is already labeled with
such a matrix $\mathbf{A}$ and vector $\mathbf{b}$. Now suppose $g$ has
incoming gates $g_{1},\ldots,g_{r}$. Let
$\mathbf{A}_{1},\ldots,\mathbf{A}_{r}$ and
$\mathbf{b}_{1},\ldots,\mathbf{b}_{r}$ with
$\mathbf{A}_{i}\in\mathbb{Z}^{s_{i}\times t_{i}}$,
$\mathbf{b}\in\mathbb{Z}^{s_{i}}$, denote the matrices and vectors constructed
for the gates $g_{1},\ldots,g_{r}$. Then the matrix
$\mathbf{A}\in\mathbb{Z}^{s\times t}$ and $\mathbf{b}\in\mathbb{Z}^{s}$ for
$g$ have the shape

$\displaystyle\mathbf{A}=\left(\begin{array}[]{c|c}\begin{array}[]{ccc}\mathbf{A}_{1}&&\\\
&\ddots&\\\ &&\mathbf{A}_{r}\end{array}&\mathbf{0}\\\
\hline\cr\mathbf{B}&\mathbf{C}\end{array}\right),$
$\displaystyle\mathbf{b}=\left(\begin{array}[]{c}\mathbf{b}_{1}\\\ \vdots\\\
\mathbf{b}_{r}\\\ \mathbf{0}\end{array}\right)$

where $\mathbf{B}$ and $\mathbf{C}$ are chosen depending on whether $g$ is
labeled with $+$ or $\cap$. If the label is $+$, then
$\mathbf{B}\in\mathbb{Z}^{n\times(t_{1}+\cdots+t_{r})},\mathbf{C}\in\mathbb{Z}^{n\times
n}$, are chosen so that $\mathbf{B}\mathbf{x}=\mathbf{c}$ expresses that in
$\mathbf{x}$, the last $n$ coordinates are the sum of
$\mathbf{y}_{1}+\cdots+\mathbf{y}_{r}$, where for each $i\in[1,r]$, the vector
$\mathbf{y}_{i}\in\mathbb{Z}^{n}$ contains the coordinates
$t_{1}+\cdots+t_{i}-n,\ldots,t_{1}+\cdots+t_{i}$, i.e. the last $n$
coordinates corresponding to $\mathbf{A}_{i}$. Hence, we have
$s=s_{1}+\cdots+s_{r}+n$ and $t=t_{1}+\cdots+t_{r}+n$. If the label is $\cap$,
then
$\mathbf{B}\in\mathbb{Z}^{rn\times(t_{1}+\cdots+t_{r})},\mathbf{C}\in\mathbb{Z}^{rn\times
n}$ are chosen so that $\mathbf{B}\mathbf{x}=\mathbf{c}$ expresses that for
each $i\in[1,r]$, the last $n$ coordinates of $\mathbf{x}$ agree with
coordinates $t_{1}+\cdots+t_{i}-n,\ldots,t_{1}+\cdots+t_{i}$ of $\mathbf{x}$,
i.e. the last $n$ coordinates corresponding to $\mathbf{A}_{i}$. Thus, we
obtain $s=s_{1}+\cdots+s_{r}+rn$ and $t=t_{1}+\cdots+t_{r}+n$.

Thus, in any case, we have
$\max\\{s,t\\}\leq(r+1)\cdot\max_{i}\max\\{s_{i},t_{i}\\}$. If $\mathbf{A}$ is
a matrix, then we define its _norm_ , denoted $\|\mathbf{A}\|$, as the maximal
absolute value of any entry. Observe that the norm in the above constructions
does not grow at all: We have $\|\mathbf{A}\|\leq\max\\{\|\mathbf{A}_{i}\|\mid
i\in[1,r]\\}$ and $\|\mathbf{b}\|\leq\max\\{\|\mathbf{b}_{i}\|\mid
i\in[1,r]\\}$. Suppose $m$ is an upper bound on the number of rows and columns
of the matrices in the leafs of $C$, and $M$ is an upper bound on their norm.
Then for any gate $g$ of depth $i$, the resulting matrix
$\mathbf{A}_{g}\in\mathbb{Z}^{s_{g}\times t_{g}}$ and vector
$\mathbf{b}_{g}\in\mathbb{Z}^{s_{g}}$ satisfy
$\max\\{s_{g},t_{g}\\}\leq(r+1)^{i}\cdot m$ and
$\|\mathbf{A}_{g}\|,\|\mathbf{b}_{g}\|\leq M$. Hence, the dimensions of the
matrices grow exponentially in the depth of the circuit, but polynomially for
fixed depth. Moreover, their entries require no more bits than the matrices in
the leaves.

###### Proposition 7.12.

(1) For every fixed number $d\in\mathbb{N}$, the problem
$\mathsf{BIREACH}(\mathsf{SC}^{\pm}_{d})$ is in $\mathsf{EXP}$. (2) If
$\ell\in\mathbb{N}$ is fixed as well, then
$\mathsf{BIREACH}(\mathsf{SC}^{\pm}_{d,\ell})$ is in $\mathsf{P}$. (3)
$\mathsf{BIREACH}(\mathsf{SC}^{\pm})$ is in $\mathsf{EXPSPACE}$.

###### Proof sketch.

We begin with (1) and (2). According to Proposition 7.1, we need to show that
emptiness for bidirected $k$-grammars is in $\mathsf{EXP}$, and in
$\mathsf{P}$ for fixed $k$.

Given a bidirected $k$-grammar, we construct a coset circuit $C$ as described
in Algorithm 1 by alternating emptiness checks for gates and building new
gates. To check gates for emptiness, recall that the circuit has depth $\leq
ck$ for some constant $c\in\mathbb{N}$. Thus, it remains to decide emptiness
of a gate $g$ in exponential time, resp. in polynomial time for bounded depth
circuits. For each gate $g$ in this coset circuit, we compute a matrix
representation for the coset $C(g)$. As argued above, the resulting matrix
$\mathbf{A}\in\mathbb{Z}^{s\times t}$ and vector $\mathbf{b}\in\mathbb{Z}^{s}$
will satisfy $s,t\leq(r+1)^{ck}$, where $r$ is the largest in-degree of a gate
in $C$. The norm of $\mathbf{A}$ and $\mathbf{b}$ is at most the norm of the
matrices in the leaves of $C$, which means the entries of $\mathbf{A}$ and
$\mathbf{b}$ only require polynomially many bits. Therefore, the size of
$\mathbf{A}$ and $\mathbf{b}$ is polynomial in $(r+1)^{ck}$. Hence, by Theorem
3.1, we can decide emptiness of $C(g)$ in time polynomial in $(r+1)^{ck}$.
Hence, Theorem 3.1 yields the desired algorithms.

For (3), we proceed slightly differently. Instead of Proposition 7.1, we use a
variant with an exponential space reduction. The resulting grammars still use
polynomially many productions, but the occurring numbers can be doubly
exponential. Our matrix encoding thus yields matrices with exponential
dimension and their entries have exponentially many bits. This still allows us
to check for emptiness of coset circuits in exponential time, resulting in an
$\mathsf{EXPSPACE}$ algorithm overall. ∎

pages0 pages

## References

  * (1) Eric Allender, Robert Beals and Mitsunori Ogihara  “The Complexity of Matrix Rank and Feasible Systems of Linear Equations”  In _Comput. Complex._ 8.2, 1999, pp. 99–126  DOI: 10.1007/s000370050023
  * (2) Carme Àlvarez and Raymond Greenlaw  “A compendium of problems complete for symmetric logarithmic space”  In _Comput. Complex._ 9.2, 2000, pp. 123–145  DOI: 10.1007/PL00001603
  * (3) Jürgen Avenhaus and Klaus Madlener  “The Nielsen reduction and P-complete problems in free groups”  In _Theoretical Computer Science_ 32.1-2 Elsevier, 1984, pp. 61–76
  * (4) Norman Biggs  “Algebraic potential theory on graphs”  In _Bulletin of the London Mathematical Society_ 29.6 Cambridge University Press, 1997, pp. 641–682
  * (5) Rémi Bonnet  “The Reachability Problem for Vector Addition System with One Zero-Test”  In _Mathematical Foundations of Computer Science 2011 - 36th International Symposium, MFCS 2011, Warsaw, Poland, August 22-26, 2011. Proceedings_ 6907, Lecture Notes in Computer Science  Springer, 2011, pp. 145–157  DOI: 10.1007/978-3-642-22993-0“˙16
  * (6) P. Buckheister and Georg Zetzsche  “Semilinearity and Context-Freeness of Languages Accepted by Valence Automata”  In _Proc. of the 38th International Symposium on Mathematical Foundations of Computer Science (MFCS 2013)_ 8087, LNCS  Berlin Heidelberg: Springer, 2013, pp. 231–242  DOI: 10.1007/978-3-642-40313-2˙22
  * (7) Krishnendu Chatterjee, Bhavya Choudhary and Andreas Pavlogiannis  “Optimal Dyck Reachability for Data-Dependence and Alias Analysis”  In _Proc. ACM Program. Lang._ 2.POPL New York, NY, USA: Association for Computing Machinery, 2018  DOI: 10.1145/3158118
  * (8) Swarat Chaudhuri  “Subcubic algorithms for recursive state machines”  In _POPL ’08_ ACM, 2008, pp. 159–169
  * (9) Tsu-Wu J. Chou and George E. Collins  “Algorithms for the Solution of Systems of Linear Diophantine Equations”  In _SIAM J. Comput._ 11.4, 1982, pp. 687–708  DOI: 10.1137/0211057
  * (10) Wojciech Czerwiński and Łukasz Orlikowski  “Reachability in Vector Addition Systems is Ackermann-complete”  In _62nd IEEE Annual Symposium on Foundations of Computer Science, FOCS 2021, Denver, CO, USA, February 7-10, 2022_ IEEE, 2021, pp. 1229–1240  DOI: 10.1109/FOCS52979.2021.00120
  * (11) Emanuele D’Osualdo, Roland Meyer and Georg Zetzsche  “First-order logic with reachability for infinite-state systems”  In _Proc. of the Thirty-First Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2016)_ New York, NY, USA: ACM, 2016, pp. 457–466
  * (12) Volker Diekert and Anca Muscholl  “Solvability of Equations in Graph Groups Is Decidable”  In _Int. J. Algebra Comput._ 16.6, 2006, pp. 1047–1070  DOI: 10.1142/S0218196706003372
  * (13) Michael Elberfeld, Andreas Jakoby and Till Tantau  “Algorithmic Meta Theorems for Circuit Classes of Constant and Logarithmic Depth”  In _29th International Symposium on Theoretical Aspects of Computer Science, STACS 2012, February 29th - March 3rd, 2012, Paris, France_ 14, LIPIcs  Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2012, pp. 66–77  DOI: 10.4230/LIPIcs.STACS.2012.66
  * (14) Christoph Haase and Simon Halfon  “Integer Vector Addition Systems with States”  In _Reachability Problems - 8th International Workshop, RP 2014, Oxford, UK, September 22-24, 2014. Proceedings_ 8762, Lecture Notes in Computer Science  Springer, 2014, pp. 112–124  DOI: 10.1007/978-3-319-11439-2“˙9
  * (15) Christoph Haase and Georg Zetzsche  “Presburger arithmetic with stars, rational subsets of graph groups, and nested zero tests”  In _34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019, Vancouver, BC, Canada, June 24-27, 2019_ IEEE, 2019, pp. 1–14  DOI: 10.1109/LICS.2019.8785850
  * (16) Matthew Hague and Anthony Widjaja Lin  “Model Checking Recursive Programs with Numeric Data Types”  In _Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings_ 6806, Lecture Notes in Computer Science  Springer, 2011, pp. 743–759  DOI: 10.1007/978-3-642-22110-1“˙60
  * (17) Ilya Kapovich, Richard Weidmann and Alexei Myasnikov  “Foldings, graphs of groups and the membership problem”  In _International Journal of Algebra and Computation_ 15.01 World Scientific, 2005, pp. 95–128
  * (18) Adam Husted Kjelstrøm and Andreas Pavlogiannis  “The decidability and complexity of interleaved bidirected Dyck reachability”  In _Proc. ACM Program. Lang._ 6.POPL, 2022, pp. 1–26  DOI: 10.1145/3498673
  * (19) Ulla Koppenhagen and Ernst W. Mayr  “The Complexity of the Coverability, the Containment, and the Equivalence Problems for Commutative Semigroups”  In _Fundamentals of Computation Theory, 11th International Symposium, FCT ’97, Kraków, Poland, September 1-3, 1997, Proceedings_ 1279, Lecture Notes in Computer Science  Springer, 1997, pp. 257–268  DOI: 10.1007/BFb0036189
  * (20) Serge Lang  “Algebra”  Springer-Verlag, 2005
  * (21) Jérôme Leroux  “The Reachability Problem for Petri Nets is Not Primitive Recursive”  In _62nd IEEE Annual Symposium on Foundations of Computer Science, FOCS 2021, Denver, CO, USA, February 7-10, 2022_ IEEE, 2021, pp. 1241–1252  DOI: 10.1109/FOCS52979.2021.00121
  * (22) Jérôme Leroux, Grégoire Sutre and Patrick Totzke  “On the Coverability Problem for Pushdown Vector Addition Systems in One Dimension”  In _Automata, Languages, and Programming - 42nd International Colloquium, ICALP 2015, Kyoto, Japan, July 6-10, 2015, Proceedings, Part II_ 9135, Lecture Notes in Computer Science  Springer, 2015, pp. 324–336  DOI: 10.1007/978-3-662-47666-6“˙26
  * (23) Yuanbo Li, Qirun Zhang and Thomas W. Reps  “Fast graph simplification for interleaved Dyck-reachability”  In _Proceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2020, London, UK, June 15-20, 2020_ ACM, 2020, pp. 780–793  DOI: 10.1145/3385412.3386021
  * (24) Yuanbo Li, Qirun Zhang and Thomas W. Reps  “On the complexity of bidirected interleaved Dyck-reachability”  In _Proc. ACM Program. Lang._ 5.POPL, 2021, pp. 1–28  DOI: 10.1145/3434340
  * (25) Markus Lohrey  “The rational subset membership problem for groups: a survey”  In _Groups St Andrews_ 422, 2013, pp. 368–389
  * (26) Markus Lohrey and Géraud Sénizergues  “When is a graph product of groups virtually-free?”  In _Communications in Algebra®_ 35.2 Taylor & Francis, 2007, pp. 617–621
  * (27) Markus Lohrey and Benjamin Steinberg  “An automata theoretic approach to the generalized word problem in graphs of groups”  In _Proceedings of the American Mathematical Society_ 138.2, 2010, pp. 445–453
  * (28) Markus Lohrey and Benjamin Steinberg  “The submonoid and rational subset membership problems for graph groups”  In _Journal of Algebra_ 320.2 Elsevier, 2008, pp. 728–755
  * (29) Markus Lohrey and Georg Zetzsche  “Knapsack in Graph Groups”  In _Theory Comput. Syst._ 62.1, 2018, pp. 192–246  DOI: 10.1007/s00224-017-9808-3
  * (30) Roger C Lyndon and Paul E Schupp  “Combinatorial Group Theory”  Springer-Verlag, 1977
  * (31) Ernst W Mayr and Albert R Meyer  “The complexity of the word problems for commutative semigroups and polynomial ideals”  In _Advances in Mathematics_ 46.3, 1982, pp. 305–329  DOI: https://doi.org/10.1016/0001-8708(82)90048-2
  * (32) Roland Meyer, Sebastian Muskalla and Georg Zetzsche  “Bounded Context Switching for Valence Systems”  In _Proc. of the 29th International Conference on Concurrency Theory (CONCUR 2018)_ 118, LIPIcs  Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 2018, pp. 12:1–12:18  DOI: 10.4230/LIPIcs.CONCUR.2018.12
  * (33) K.. Mikhailova  “The occurrence problem for direct products of groups”  In _Matematicheskii Sbornik (Novaya Seriya)_ 70(112), 1966, pp. 241–251
  * (34) Omer Reingold  “Undirected connectivity in log-space”  In _J. ACM_ 55.4, 2008, pp. 17:1–17:24  DOI: 10.1145/1391289.1391291
  * (35) Klaus Reinhardt  “Reachability in Petri nets with inhibitor arcs”  In _Electronic Notes in Theoretical Computer Science_ 223 Elsevier, 2008, pp. 239–264
  * (36) Aneesh Shetty, Krishna S. and Georg Zetzsche  “Scope-Bounded Reachability in Valence Systems”  In _Proc. of the 32nd International Conference on Concurrency Theory (CONCUR 2021)_ 118, LIPIcs  Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 2021  DOI: 10.4230/LIPIcs.CONCUR.2021.29
  * (37) Kumar Neeraj Verma, Helmut Seidl and Thomas Schwentick  “On the Complexity of Equational Horn Clauses”  In _Automated Deduction - CADE-20, 20th International Conference on Automated Deduction, Tallinn, Estonia, July 22-27, 2005, Proceedings_ 3632, Lecture Notes in Computer Science  Springer, 2005, pp. 337–352  DOI: 10.1007/11532231“˙25
  * (38) D. Wise  “From Riches to RAAGs: 3-maniforld, right-angled Artin groups, and cubical geometry”  American Mathematical Society, 2012
  * (39) Guoqing Xu, Atanas Rountev and Manu Sridharan  “Scaling CFL-Reachability-Based Points-To Analysis Using Context-Sensitive Must-Not-Alias Analysis”  In _ECOOP 2009 - Object-Oriented Programming, 23rd European Conference, Genoa, Italy, July 6-10, 2009. Proceedings_ 5653, Lecture Notes in Computer Science  Springer, 2009, pp. 98–122  DOI: 10.1007/978-3-642-03013-0“˙6
  * (40) Dacong Yan, Guoqing Xu and Atanas Rountev  “Demand-driven context-sensitive alias analysis for Java”  In _Proceedings of the 20th International Symposium on Software Testing and Analysis, ISSTA 2011, Toronto, ON, Canada, July 17-21, 2011_ ACM, 2011, pp. 155–165  DOI: 10.1145/2001420.2001440
  * (41) Georg Zetzsche  “Computing downward closures for stacked counter automata”  In _Proc. of the 32nd International Symposium on Theoretical Aspects of Computer Science (STACS 2015)_ 30, Leibniz International Proceedings in Informatics (LIPIcs)  Dagstuhl, Germany: Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 2015, pp. 743–756  DOI: 10.4230/LIPIcs.STACS.2015.743
  * (42) Georg Zetzsche  “Monoids as Storage Mechanisms”, 2016
  * (43) Georg Zetzsche  “Monoids as Storage Mechanisms”  In _Bull. EATCS_ 120, 2016  URL: http://eatcs.org/beatcs/index.php/beatcs/article/view/459