lemthm lem propthm prop rmkthm rmk

# The Emptiness Problem for Valence Automata over Graph Monoids

Georg Zetzsche<EMAIL_ADDRESS>LSV, CNRS & ENS Paris-Saclay, France

###### Abstract.

This work studies which storage mechanisms in automata permit decidability of
the emptiness problem. The question is formalized using valence automata, an
abstract model of automata in which the storage mechanism is given by a
monoid. For each of a variety of storage mechanisms, one can choose a
(typically infinite) monoid $M$ such that valence automata over $M$ are
equivalent to (one-way) automata with this type of storage. In fact, many
important storage mechanisms can be realized by monoids defined by finite
graphs, called graph monoids. Examples include pushdown stacks, partially
blind counters (which behave like Petri net places), blind counters (which may
attain negative values), and combinations thereof.

Hence, we study for which graph monoids the emptiness problem for valence
automata is decidable. A particular model realized by graph monoids is that of
Petri nets with a pushdown stack. For these, decidability is a long-standing
open question and we do not answer it here.

However, if one excludes subgraphs corresponding to this model, a
characterization can be achieved. Moreover, we provide a description of those
storage mechanisms for which decidability remains open. This leads to a model
that naturally generalizes both pushdown Petri nets and the priority
multicounter machines introduced by Reinhardt.

The cases that are proven decidable constitute a natural and apparently new
extension of Petri nets with decidable reachability. It is finally shown that
this model can be combined with another such extension by Atig and Ganty: We
present a further decidability result that subsumes both of these Petri net
extensions.

The author is supported by a fellowship within the Postdoc-Program of the
German Academic Exchange Service (DAAD) and by Labex DigiCosme, Univ. Paris-
Saclay, project VERICONISS.

##  1\. Introduction

For each storage mechanism in one-way automata, it is an important question
whether the emptiness problem is decidable. It therefore seems prudent to aim
for general insights into which properties of storage mechanisms are
responsible for decidability or undecidability.

Our approach to obtain such insights is the model of valence automata. These
feature a finite-state control and a (typically infinite) monoid that
represents a storage mechanism. The edge inscriptions consist of an input word
and an element of the monoid. Then, a computation is accepting if it arrives
in a final state and composing the encountered monoid elements yields the
neutral element. This way, by choosing a suitable monoid, one can realize a
variety of storage mechanisms. Hence, our question becomes: _For which monoids
$M$ is the emptiness problem for valence automata over $M$ decidable?_

We address this question for a class of monoids that was introduced in [19]
and accommodates a number of storage mechanisms that have been studied in
automata theory. Examples include _pushdown stacks_ , _partially blind
counters_ (which behave like Petri net places), and _blind counters_ (which
may attain negative values; these are in most situations interchangeable with
reversal-bounded counters), and combinations thereof. See [22, 23] for an
overview. These monoids are defined by graphs and thus called _graph monoids_
111They are not to be confused with the closely related, but different concept
of _trace monoids_ [5], i.e. monoids of Mazurkiewicz traces, which some
authors also call graph monoids..

A particular type of storage mechanism that can be realized by graph monoids
are partially blind counters that can be used simultaneously with a pushdown
stack. Automata with such a storage are equivalent to _pushdown Petri nets
(PPN)_ , i.e. Petri nets where the transitions can also operate on a pushdown
stack. This means, a complete characterization of graph monoids with a
decidable emptiness problem would entail an answer to the long-standing open
question of whether reachability is decidable for this Petri net extension
[15]. Partial solutions have recently been obtained by Atig and Ganty [2] and
by Leroux, Sutre, and Totzke [12].

### Contribution

While this work does not answer this open question concerning PPN, it does
provide a characterization among all graph monoids that avoid this elusive
storage type. More precisely, we identify a set of graphs, ‘PPN-graphs’, each
of which corresponds precisely to PPN with one Petri net place. Then, among
all graphs $\Gamma$ avoiding PPN-graphs as induced subgraphs, we characterize
those for which the graph monoid $\mathbb{M}\Gamma$ results in a decidable
emptiness problem. Furthermore, we provide a simple, more mechanical (as
opposed to algebraic) description of

  1. (i)

the storage mechanism emerging as the most general decidable case and

  2. (ii)

a type of mechanism equivalent to the cases we leave open.

The model (i) is a new extension of partially blind counter automata (i.e.
Petri nets). While the decidability proof employs a reduction to Reinhardt’s
priority multicounter machines [15], the model (i) seems to be expressively
incomparable to Reinhardt’s model. The model (ii) is a class of mechanisms
whose simplest instance are the pushdown Petri nets and which also naturally
subsumes priority multicounter machines (see also Section 3).

Another recent extension of the decidability of reachability of Petri nets has
been obtained by Atig and Ganty [2]. In fact, it is a partial solution to the
reachability problem for PPN. Their proof also relies on priority multicounter
machines. They show that given a _finite-index_ context-free language $K$ and
a language $L$ generated by a Petri net, it is decidable whether the
intersection $K\cap L$ is empty. Note that without the finite-index
requirement, this would be equivalent to the reachability problem for PPN. Our
final contribution is a decidability result that subsumes both the
decidability of model (i) and the result of Atig and Ganty. We present a
natural language class that contains both the intersections considered by Atig
and Ganty and the languages of model (i) and still has a decidable emptiness
problem. To this end, we employ a slightly stronger (and perhaps simpler)
version of Atig and Ganty’s reduction.

Hence, the perspective of valence automata allows us to identify natural
storage mechanisms that  (i) push the frontier of decidable emptiness (and
hence reachability) and  (ii) let us naturally interpret PPN and priority
multicounter machines as special cases of a more powerful model that might
enjoy decidability , respectively.

The paper is structured as follows. We present the main results in Section 3
and prove them in Sections 4, 5 and 6. Section 4 presents the undecidability
part, Section 5 treats the decidable cases, and Section 6 shows the expressive
equivalence with the more mechanical descriptions. In Section 7, we present
the enhanced decidability result that also subsumes the one by Atig and Ganty.

This work is an extended version of the paper [21]. This version provides
proofs of the results of [21] and the enhanced decidability result. Moreover,
it contains proofs of some results that first appeared in [19, 20], but have
not yet undergone journal peer review.

##  2\. Preliminaries

A _monoid_ is a set $M$ together with a binary associative operation such that
$M$ contains a neutral element. Unless the monoid at hand warrants a different
notation, we will denote the neutral element by $1$ and the product of $x,y\in
M$ by $xy$. If $X$ is a set of symbols, $X^{*}$ denoted the set of words over
$X$. The length of the word $w\in X^{*}$ is denoted $|w|$. An _alphabet_ is a
finite set of symbols. The empty word is denoted by $\varepsilon\in X^{*}$.
Let $P\subseteq X\times X$ is a set of pairs of symbols, then the _semi-Dyck
language_ over $P$, denoted $D_{P}^{*}$ is the smallest subset of $X^{*}$ such
that $\varepsilon\in D_{P}^{*}$ and whenever $uv\in\mathcal{D}_{P}^{*}$, then
also $ua\bar{a}v\in D_{P}^{*}$ for every $(a,\bar{a})\in P$. If
$P=\\{(a_{i},\bar{a}_{i})\mid i\in\\{1,\ldots,n\\}\\}$, then we also write
$D_{n}^{*}$ instead of $D_{P}^{*}$. Moreover, if $P=\\{(a,b)\\}$, then the
words in $D_{P}^{*}$ are called _semi-Dyck words over $a,b$_. If $w\in X^{*}$
is a word with $w=x_{1}\cdots x_{n}$ for $x_{1},\ldots,x_{n}\in X$, then
$w^{R}$ denotes $w$ in reverse, i.e. $w^{R}=x_{n}\cdots x_{1}$.

For an alphabet $X$ and languages $L,K\subseteq X^{*}$, the _shuffle product_
$L\shuffle K$ is the set of all words $u_{0}v_{1}u_{1}\cdots v_{n}u_{n}$ where
$u_{0},\ldots,u_{n},v_{1},\ldots,v_{n}\in X^{*}$, $u_{0}\cdots u_{n}\in L$,
and $v_{1}\cdots v_{n}\in K$. For a subset $Y\subseteq X$, we define the
_projection morphism_ $\pi_{Y}\colon X^{*}\to Y^{*}$ by $\pi_{Y}(y)=y$ for
$y\in Y$ and $\pi_{Y}(x)=\varepsilon$ for $x\in X\setminus Y$. Moreover, we
define $|w|_{Y}=|\pi_{Y}(w)|$ and for $x\in X$, we set
$|w|_{x}=|w|_{\\{x\\}}$.

### Valence automata

As a framework for studying which storage mechanisms permit decidability of
the emptiness problem, we employ valence automata. They feature a monoid that
dictates which computations are valid. Hence, by an appropriate choice of the
monoid, valence automata can be instantiated to be equivalent to a concrete
automata model with storage. For the purposes of this work, _equivalent_ is
meant with respect to accepted languages. Therefore, we regard valence
automata as language accepting devices.

Let $M$ be a monoid and $X$ an alphabet. A _valence automaton over $M$_ is a
tuple $\mathcal{A}=(Q,X,M,E,q_{0},F)$, in which  (i) $Q$is a finite set of
_states_ ,  (ii) $E$is a finite subset of $Q\times X^{*}\times M\times Q$,
called the set of _edges_ ,  (iii) $q_{0}\in Q$is the _initial state_ , and
(iv) $F\subseteq Q$is the set of _final states_.  For $q,q^{\prime}\in Q$,
$w,w^{\prime}\in X^{*}$, and $m,m^{\prime}\in M$, we write
$(q,w,m)\rightarrow_{\mathcal{A}}(q^{\prime},w^{\prime},m^{\prime})$ if there
is an edge $(q,v,n,q^{\prime})\in E$ such that $w^{\prime}=wv$ and
$m^{\prime}=mn$. The language _accepted_ by $\mathcal{A}$ is then

$\mathsf{L}(\mathcal{A})=\\{w\in
X^{*}\mid(q_{0},\varepsilon,1)\rightarrow^{*}_{\mathcal{A}}(f,w,1)~{}\text{for
some $f\in F$}\\}.$

The class of languages accepted by valence automata over $M$ is denoted by
$\mathsf{VA}(M)$. If $\mathcal{M}$ is a class of monoids, we write
$\mathsf{VA}(\mathcal{M})$ for $\bigcup_{M\in\mathcal{M}}\mathsf{VA}(M)$.

### Graphs

A _graph_ is a pair $\Gamma=(V,E)$ where $V$ is a finite set and $E$ is a
subset of $\\{S\subseteq V\mid 1\leq|S|\leq 2\\}$. The elements of $V$ are
called _vertices_ and those of $E$ are called _edges_. Vertices $v,w\in V$ are
_adjacent_ if $\\{v,w\\}\in E$. If $\\{v\\}\in E$ for some $v\in V$, then $v$
is called a _looped_ vertex, otherwise it is _unlooped_. A _subgraph_ of
$\Gamma$ is a graph $(V^{\prime},E^{\prime})$ with $V^{\prime}\subseteq V$ and
$E^{\prime}\subseteq E$. Such a subgraph is called _induced (by $V^{\prime}$)_
if $E^{\prime}=\\{S\in E\mid S\subseteq V^{\prime}\\}$, i.e. $E^{\prime}$
contains all edges from $E$ incident to vertices in $V^{\prime}$. By
$\Gamma\setminus\\{v\\}$, for $v\in V$, we denote the subgraph of $\Gamma$
induced by $V\setminus\\{v\\}$. By $\mathsf{C4}{}$ ($\mathsf{P4}{}$), we
denote a graph that is a cycle (path) on four vertices; see Fig. 1. Moreover,
$\Gamma^{-}$ denotes the graph obtained from $\Gamma$ by deleting all loops:
We have $\Gamma^{-}=(V,E^{-})$, where $E^{-}=\\{S\in E\mid|S|=2\\}$. The graph
$\Gamma$ is _loop-free_ if $\Gamma^{-}=\Gamma$. Finally, a _clique_ is a loop-
free graph in which any two distinct vertices are adjacent.

(a) $\mathsf{P4}$

(b) $\mathsf{C4}{}$

Figure 1. Graphs $\mathsf{C4}{}$ and $\mathsf{P4}{}$.

### Products and presentations

If $M$, $N$ are monoids, then $M\times N$ denotes their _direct product_ ,
whose set of elements is the cartesian product of $M$ and $N$ and composition
is defined component-wise. By $M^{n}$, we denote the $n$-fold direct product,
i.e. $M\times\cdots\times M$ with $n$ factors.

Let $A$ be a (not necessarily finite) set of symbols and $R$ be a subset of
$A^{*}\times A^{*}$. The pair $(A,R)$ is called a _(monoid) presentation_. The
smallest congruence of the free monoid $A^{*}$ containing $R$ is denoted by
$\equiv_{R}$ and we will write $[w]_{R}$ for the congruence class of $w\in
A^{*}$. The _monoid presented by $(A,R)$_ is defined as
$A^{*}/\mathord{\equiv_{R}}$. Note that since we did not impose a finiteness
restriction on $A$, up to isomorphism, every monoid has a presentation. If
$A=\\{a_{1},\ldots,a_{n}\\}$ and $R=\\{(r_{i},\bar{r}_{i})\mid
i\in\\{1,\ldots,k\\}\\}$, we also use the shorthand $\langle
a_{1},\ldots,a_{n}\mid r_{1}=\bar{r}_{1},\ldots,r_{k}=\bar{r}_{k}\rangle$ to
denote the monoid presented by $(A,R)$.

Furthermore, for monoids $M_{1}$, $M_{2}$ we can find presentations
$(A_{1},R_{1})$ and $(A_{2},R_{2})$ such that $A_{1}\cap A_{2}=\emptyset$. We
define the _free product_ $M_{1}*M_{2}$ to be presented by $(A_{1}\cup
A_{2},R_{1}\cup R_{2})$. Note that $M_{1}*M_{2}$ is well-defined up to
isomorphism. In analogy to the $n$-fold direct product, we write $M^{(n)}$ for
the $n$-fold free product of $M$.

### Graph monoids

A presentation $(A,R)$ in which $A$ is a finite alphabet is a _Thue system_.
To each graph $\Gamma=(V,E)$, we associate the Thue system
$T_{\Gamma}=(X_{\Gamma},R_{\Gamma})$ over the alphabet
$X_{\Gamma}=\\{a_{v},\bar{a}_{v}\mid v\in V\\}$. $R_{\Gamma}$ is defined as

$R_{\Gamma}=\\{(a_{v}\bar{a}_{v},\varepsilon)\mid v\in V\\}\cup\\{(xy,yx)\mid
x\in\\{a_{v},\bar{a}_{v}\\},~{}y\in\\{a_{w},\bar{a}_{w}\\},~{}\\{v,w\\}\in
E\\}.$

In particular, we have $(a_{v}\bar{a}_{v},\bar{a}_{v}a_{v})\in R_{\Gamma}$
whenever $\\{v\\}\in E$. To simplify notation, the congruence
$\equiv_{R_{\Gamma}}$ is then also denoted by $\equiv_{\Gamma}$. We are now
ready to define graph monoids. To each graph $\Gamma$, we associate the monoid

$\mathbb{M}\Gamma~{}~{}=~{}~{}X^{*}_{\Gamma}/\mathord{\equiv_{\Gamma}}.$

The monoids of the form $\mathbb{M}\Gamma$ are called _graph monoids_.

### Storage mechanisms as graph monoids

Let us briefly discuss how to realize storage mechanisms by graph monoids.
First, suppose $\Gamma_{0}$ and $\Gamma_{1}$ are disjoint graphs. If $\Gamma$
is the union of $\Gamma_{0}$ and $\Gamma_{1}$, then
$\mathbb{M}\Gamma\cong\mathbb{M}\Gamma_{0}*\mathbb{M}\Gamma_{1}$ by
definition. Moreover, if $\Gamma$ is obtained from $\Gamma_{0}$ and
$\Gamma_{1}$ by drawing an edge between each vertex of $\Gamma_{0}$ and each
vertex of $\Gamma_{1}$, then
$\mathbb{M}\Gamma\cong\mathbb{M}\Gamma_{0}\times\mathbb{M}\Gamma_{1}$.

If $\Gamma$ consists of one vertex $v$ and has no edges, the only rule in the
Thue system is $(a_{v}\bar{a}_{v},\varepsilon)$. In this case,
$\mathbb{M}\Gamma$ is also denoted as $\mathbb{B}$ and we will refer to it as
the _bicyclic monoid_. The generators $a_{v}$ and $\bar{a}_{v}$ are then also
written $a$ and $\bar{a}$, respectively. It is not hard to see that
$\mathbb{B}$ corresponds to a _partially blind counter_ , i.e. one that
attains only non-negative values and has to be zero at the end of the
computation. Moreover, if $\Gamma$ consists of one looped vertex, then
$\mathbb{M}\Gamma$ is isomorphic to $\mathbb{Z}$ and thus realizes a _blind
counter_ , which can go below zero and is zero-tested in the end.

If one storage mechanism is realized by a monoid $M$, then the monoid
$\mathbb{B}*M$ corresponds to the mechanism that _builds stacks_ : A
configuration of this new mechanism consists of a sequence $c_{0}ac_{1}\cdots
ac_{n}$, where $c_{0},\ldots,c_{n}$ are configurations of the mechanism
realized by $M$. We interpret this as a stack with the entries
$c_{0},\ldots,c_{n}$. One can open a new stack entry on top (by multiplying
$a\in\mathbb{B}$), remove the topmost entry if empty (by multiplying
$\bar{a}\in\mathbb{B}$) and operate on the topmost entry using the old
mechanism (by multiplying elements from $M$). In particular,
$\mathbb{B}*\mathbb{B}$ describes a pushdown stack with two stack symbols. See
[22] for more examples and [23] for more details.

As a final example, suppose $\Gamma$ is one edge short of being a clique, then
$\mathbb{M}\Gamma\cong\mathbb{B}^{(2)}\times\mathbb{B}^{n-2}$, where $n$ is
the number of vertices in $\Gamma$. Then, by the observations above, valence
automata over $\mathbb{M}\Gamma$ are equivalent to Petri nets with $n-2$
unbounded places and access to a pushdown stack. Hence, for our purposes, a
_pushdown Petri net_ is a valence automaton over
$\mathbb{B}^{(2)}\times\mathbb{B}^{n}$ for some $n\in\mathbb{N}$.

##  3\. Results

As a first step, we exhibit graphs $\Gamma$ for which
$\mathsf{VA}(\mathbb{M}\Gamma)$ includes the recursively enumerable languages.

######  Theorem 3.1.

Let $\Gamma$ be a graph such that $\Gamma^{-}$ contains $\mathsf{C4}$ or
$\mathsf{P4}$ as an induced subgraph. Then $\mathsf{VA}(\mathbb{M}\Gamma)$ is
the class of recursively enumerable languages. In particular, the emptiness
problem is undecidable for valence automata over $\mathbb{M}\Gamma$.

This unifies and slightly strengthens a few undecidability results concerning
valence automata over graph monoids. The case that all vertices are looped was
shown by Lohrey and Steinberg [14] (see also the discussion of Theorem 3.3).
Another case appeared in [19]. We prove Theorem 3.1 in Section 4.

It is not clear whether Theorem 3.1 describes all $\Gamma$ for which
$\mathsf{VA}(\mathbb{M}\Gamma)$ exhausts the recursively enumerable languages.
For example, as mentioned above, if $\Gamma$ is one edge short of being a
clique, then valence automata over $\mathbb{M}\Gamma$ are pushdown Petri nets.
In particular, the emptiness problem for valence automata is equivalent to the
reachability problem of this model, for which decidability is a long-standing
open question [15]. In fact, it is already open whether reachability is
decidable in the case of $\mathbb{B}^{(2)}\times\mathbb{B}$, although Leroux,
Sutre, and Totzke have recently made progress on this case [12]. Therefore,
characterizing those $\Gamma$ with a decidable emptiness problem for valence
automata over $\mathbb{M}\Gamma$ would very likely settle these open
questions222Strictly speaking, it is conceivable that there is a decision
procedure for each $\mathbb{B}^{(2)}\times\mathbb{B}^{n}$, but no uniform one
that works for all $n$. However, this seems unlikely..

However, we will show that if we steer clear of pushdown Petri nets, we can
achieve a characterization. More precisely, we will present a set of graphs
that entail the behavior of pushdown Petri nets. Then, we show that among
those graphs that do not contain these as induced subgraphs, the absence of
$\mathsf{P4}{}$ and $\mathsf{C4}{}$ already characterizes decidability.

### PPN-graphs

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

We say that the graph $\Gamma$ is _PPN-free_ if it has no PPN-graph as an
induced subgraph. Observe that a graph $\Gamma$ is PPN-free if and only if in
the neighborhood of each unlooped vertex, any two vertices are adjacent.

Of course, the abbreviation ‘PPN’ refers to ‘pushdown Petri nets’. This is
justified by the following fact. It is proven in Section 5 (page 5).

######  Proposition .

If $\Gamma$ is a PPN-graph, then
$\mathsf{VA}(\mathbb{M}\Gamma)=\mathsf{VA}(\mathbb{B}^{(2)}\times\mathbb{B})$.

### Transitive forests

In order to exploit the absence of $\mathsf{P4}{}$ and $\mathsf{C4}{}$ as
induced subgraphs, we will employ a characterization of such graphs as
transitive forests. The _comparability graph_ of a tree $t$ is a simple graph
with the same vertices as $t$, but has an edge between two vertices whenever
one is a descendant of the other in $t$. A graph $\Gamma$ is a _transitive
forest_ if the simple graph $\Gamma^{-}$ is a disjoint union of comparability
graphs of trees. For an example of a transitive forest, see Fig. 2.

Figure 2. Example of a transitive forest. The solid edges are part of the
trees whose comparability graphs make up the graph. The transitive forest
consists of both the solid and the dashed edges.

Let $\mathsf{DEC}$ denote the smallest isomorphism-closed class of monoids
such that

  1. 1.

for each $n\geq 0$, we have $\mathbb{B}^{n}\in\mathsf{DEC}$ and

  2. 2.

for $M,N\in\mathsf{DEC}$, we also have $M*N\in\mathsf{DEC}$ and
$M\times\mathbb{Z}\in\mathsf{DEC}$.

Our main result characterizes those PPN-free $\Gamma$ for which valence
automata over $\mathbb{M}\Gamma$ have a decidable emptiness problem.

######  Theorem 3.2.

Let $\Gamma$ be PPN-free. Then the following conditions are equivalent:

  1. 1.

Emptiness is decidable for valence automata over $\mathbb{M}\Gamma$.

  2. 2.

$\Gamma^{-}$ contains neither $\mathsf{C4}{}$ nor $\mathsf{P4}{}$ as an
induced subgraph.

  3. 3.

$\Gamma$ is a transitive forest.

  4. 4.

$\mathbb{M}\Gamma\in\mathsf{DEC}$.

We present the proof in Section 5. Note that this generalizes the fact that
emptiness is decidable for pushdown automata (i.e. graphs with no edges) and
partially blind multicounter automata (i.e. cliques), or equivalently,
reachability in Petri nets.

Note that if $\Gamma$ has a loop on every vertex, then $\mathbb{M}\Gamma$ is a
group. Groups that arise in this way are called _graph groups_. In general, if
a monoid $M$ is a group, then emptiness for valence automata over $M$ is
decidable if and only if the _rational subset membership problem_ is decidable
for $M$ [11]. The latter problem asks, given a rational set $R$ over $M$ and
an element $m\in M$, whether $m\in R$; see [13] for more information.
Therefore, Theorem 3.2 extends the following result of Lohrey and Steinberg
[14], which characterizes those graph groups for which the rational subset
membership problem is decidable.

######  Theorem 3.3 (Lohrey and Steinberg [14]).

Let $\Gamma$ be a graph in which every vertex is looped. Then the rational
subset membership problem for the group $\mathbb{M}\Gamma$ is decidable if and
only if $\Gamma$ is a transitive forest.

Lohrey and Steinberg show decidability by essentially proving that in their
case, the languages in $\mathsf{VA}(\mathbb{M}\Gamma)$ have semilinear Parikh
images (although they use different terminology). Here, we extend this
argument by showing that in the equivalent cases of Theorem 3.2, the Parikh
images of $\mathsf{VA}(\mathbb{M}\Gamma)$ are those of languages accepted by
priority multicounter machines. The latter were introduced and shown to have a
decidable reachability problem by Reinhardt [15].

### Intuition for decidable cases

In order to provide an intuition for those storage mechanisms (not containing
a pushdown Petri net) with a decidable emptiness problem, we present an
equally expressive class of monoids for which the corresponding storage
mechanisms are easier to grasp. Let $\mathsf{SC}^{\pm}$ be the smallest
isomorphism-closed class of monoids with

  1. 1.

for each $n\in\mathbb{N}$, we have $\mathbb{B}^{n}\in\mathsf{SC}^{\pm}$,

  2. 2.

for each $M\in\mathsf{SC}^{\pm}$, we also have
$\mathbb{B}*M\in\mathsf{SC}^{\pm}$ and
$M\times\mathbb{Z}\in\mathsf{SC}^{\pm}$.

Thus, $\mathsf{SC}^{\pm}$ realizes those storage mechanisms that can be
constructed from a finite set of _partially blind counters_ ($\mathbb{B}^{n}$)
by _building stacks_ ($M\mapsto\mathbb{B}*M$) and _adding blind counters_
($M\mapsto M\times\mathbb{Z}$). Then, in fact, the monoids in
$\mathsf{SC}^{\pm}$ produce the same languages as those in $\mathsf{DEC}$.

######  Proposition .

$\mathsf{VA}(\mathsf{DEC})=\mathsf{VA}(\mathsf{SC}^{\pm})$.

Section 3 is proven in Section 6. While our decidability proof for
$\mathsf{SC}^{\pm}$ will be a reduction to priority multicounter machines (see
Section 5 for a definition), it seems likely that these two models are
incomparable in terms of expressiveness (see the remarks after Theorem 5.3).

### Intersections with finite-index languages

This work exhibits valence automata over $\mathsf{SC}^{\pm}$ as an extension
of Petri nets that features a type of stack but retains decidability of the
emptiness problem. Another recent result of this kind has been obtained by
Atig and Ganty [2]. They showed that given a finite-index context-free
language $K$ and a Petri net language $L$, it is decidable whether $K\cap L$
is empty. Moreover, they also employ a reduction to priority multicounter
machines. This raises the question of how the two results relate to each
other. In Section 7, we present a natural language class that subsumes both
the languages of Atig and Ganty and those of $\mathsf{VA}(\mathsf{SC}^{\pm})$
and prove that emptiness is still decidable. Intuitively, this class is
obtained by taking languages of Atig and Ganty and then applying operators
corresponding to _building stacks_ and _adding blind counters_. The precise
definition and the result can be found in Section 7.

### Intuition for open cases

We also want to provide an intuition for the remaining storage mechanisms,
i.e. those defined by monoids $\mathbb{M}\Gamma$ about which Theorems 3.1 and
3.2 make no statement. To this end, we describe a class of monoids that are
expressively equivalent to these remaining cases. The remaining cases are
given by those graphs $\Gamma$ where $\Gamma^{-}$ does not contain
$\mathsf{C4}{}$ or $\mathsf{P4}{}$, but $\Gamma$ contains a PPN-graph. Let
$\mathsf{REM}$ denote the class of monoids $\mathbb{M}\Gamma$, where $\Gamma$
is such a graph. Let $\mathsf{SC^{+}}$ be the smallest isomorphism-closed
class of monoids with

  1. 1.

$\mathbb{B}^{(2)}\times\mathbb{B}\in\mathsf{SC^{+}}$ and

  2. 2.

for each $M\in\mathsf{SC^{+}}$, we also have $\mathbb{B}*M\in\mathsf{SC^{+}}$
and $M\times\mathbb{B}\in\mathsf{SC^{+}}$.

This means, $\mathsf{SC^{+}}$ realizes those storage mechanisms that are
obtained from _a pushdown stack, together with one partially blind counter_
($\mathbb{B}^{(2)}\times\mathbb{B}$) by the transformations of _building
stacks_ ($M\mapsto\mathbb{B}*M$) and _adding partially blind counters_
($M\mapsto M\times\mathbb{B}$).

######  Proposition .

$\mathsf{VA}(\mathsf{REM})=\mathsf{VA}(\mathsf{SC^{+}})$.

We prove Section 3 in Section 6. Of course, $\mathsf{SC^{+}}$ generalizes
pushdown Petri nets, which correspond to monoids
$\mathbb{B}^{(2)}\times\mathbb{B}^{n}$ for $n\in\mathbb{N}$. Moreover,
$\mathsf{SC^{+}}$ also subsumes priority multicounter machines (see p. 5 for a
definition) in a straightforward way: Every time we build stacks, we can use
the new pop operation to realize a zero test on all the counters we have added
so far. Let $M_{0}=\mathbf{1}$ and
$M_{k+1}=\mathbb{B}*(M_{k}\times\mathbb{B})$. Then, priority $k$-counter
machines correspond to valence automata over $M_{k}$ where the stack heights
never exceed $1$.

######  Remark .

Priority multicounter machines are already subsumed by pushdown Petri nets
alone: Atig and Ganty [2, Lemma 7] show implicitly that for each priority
multicounter machine, one can construct a pushdown Petri net that accepts the
same language. Hence, valence automata over $\mathsf{SC^{+}}$ are not the
first perhaps-decidable generalization of both pushdown Petri nets and
priority multicounter machines, but they generalize both in a natural way.

##  4\. Undecidability

In this section, we prove Theorem 3.1. It should be mentioned that a result
similar to Theorem 3.1 was shown by Lohrey and Steinberg [14]: They proved
that if every vertex in $\Gamma$ is looped and $\Gamma^{-}$ contains
$\mathsf{C4}$ or $\mathsf{P4}$ as an induced subgraph, then the rational
subset membership problem is undecidable for $\mathbb{M}\Gamma$. Their proof
adapts a construction of Aalbersberg and Hoogeboom [1], which shows that the
disjointness problem for rational sets of traces is undecidable when the
independence relation has $\mathsf{P4}$ or $\mathsf{C4}$ as an induced
subgraph. An inspection of the proof presented here, together with its
prerequisites (Theorems 4.1 and 4.2), reveals that the employed ideas are very
similar to the combination of Lohrey and Steinberg’s and Aalbersberg and
Hoogeboom’s proof.

A _language class_ is a collection of languages that contains at least one
non-empty language. In this work, for each language class, there is a way to
finitely represent each member of the class. Moreover, an inclusion
$\mathcal{C}\subseteq\mathcal{D}$ between language classes $\mathcal{C}$ and
$\mathcal{D}$ is always meant to be _effective_ , in other words: Given a
representation of a language in $\mathcal{C}$, we can compute a representation
of that language in $\mathcal{D}$. The same holds for equalities between
language classes.

Let $X$ and $Y$ be alphabets. A relation $T\subseteq X^{*}\times Y^{*}$ is
called a _rational transduction_ if there is an alphabet $W$, a regular
language $R\subseteq W^{*}$, and morphisms $g\colon W^{*}\to X^{*}$ and
$h\colon W^{*}\to Y^{*}$ such that $T=\\{(g(w),h(w))\mid w\in R\\}$ (see [3]).
For a language $L\subseteq X^{*}$, we define $TL=\\{v\in Y^{*}\mid\exists u\in
L\colon(u,v)\in T\\}$. A language class $\mathcal{C}$ is a _full trio_ if for
every language $L$ in $\mathcal{C}$, the language $TL$ is effectively
contained in $\mathcal{C}$ as well. Here, “effectively” means again that given
a representation of a language $L$ from $\mathcal{C}$ and a description of
$T$, one can effectively compute a representation of $TL$. For a language $L$,
we denote by $\mathcal{T}(L)$ the smallest full trio containing $L$. Note that
if $L\neq\emptyset$, the class $\mathcal{T}(L)$ contains precisely the
languages $TL$ for rational transductions $T$. For example, it is well-known
that for every monoid $M$, the class $\mathsf{VA}(M)$ is a full trio [6]. A
_full AFL_ is a full trio that is also closed under Kleene iteration, i.e. for
each member $L$, the language $L^{*}$ is effectively a member as well.

Here, we use the following fact. We denote the recursively enumerable
languages by $\mathsf{RE}$.

######  Lemma .

Let $X=\\{a_{1},\bar{a}_{1},b_{1},a_{2},\bar{a}_{2},b_{2}\\}$ and let
$B_{2}\subseteq X^{*}$ be defined as

$B_{2}=(\\{a_{1}^{n}\bar{a}_{1}^{n}\mid n\geq
0\\}b_{1})^{*}\shuffle(\\{a_{2}^{n}\bar{a}_{2}^{n}\mid n\geq 0\\}b_{2})^{*}.$

Then $\mathsf{RE}$ equals $\mathcal{T}(B_{2})$, the smallest full trio
containing $B_{2}$.

Section 4 is essentially due to Hartmanis and Hopcroft, who stated it in
slightly different terms:

######  Theorem 4.1 (Hartmanis and Hopcroft [9]).

Let $\mathcal{C}$ be the smallest full AFL containing $\\{a^{n}b^{n}\mid n\geq
0\\}$. Every recursively enumerable language is the homomorphic image of the
intersection of two languages in $\mathcal{C}$.

By the following auxiliary result of Ginsburg and Greibach [8, Theorem 3.2a],
Section 4 will follow from Theorem 4.1.

######  Theorem 4.2 (Ginsburg and Greibach [8]).

Let $L\subseteq X^{*}$ and $c\notin X$. The smallest full AFL containing $L$
equals $\mathcal{T}((Lc)^{*})$.

As announced, Section 4 now follows.

######  Section 4.

author=R1]I am not fully convinced of the interest of sharing the symbols
$a_{1}$ and $a_{2}$ between $X$ and $X_{\Gamma}$, since the proof uses
homomorphisms liberally. Since clearly
$\mathcal{T}(B_{2})\subseteq\mathsf{RE}$, it suffices to show
$\mathsf{RE}\subseteq\mathcal{T}(B_{2})$. According to Theorem 4.1, this
amounts to showing that $L_{1}\cap L_{2}\in\mathcal{T}(B_{2})$ for any $L_{1}$
and $L_{2}$ in $\mathcal{C}$, where $\mathcal{C}$ is the smallest full AFL
containing the language $S=\\{a^{n}b^{n}\mid n\geq 0\\}$. Hence, let
$L_{1},L_{2}\in\mathcal{C}$. By Theorem 4.2, $L_{1}$ and $L_{2}$ belong to
$\mathcal{C}=\mathcal{T}((Sc)^{*})$. This means we have
$L_{i}=T_{i}(\\{a_{i}^{n}\bar{a}_{i}^{n}\mid n\geq 0\\}b_{i})^{*}$ for some
rational transduction $T_{i}$ for $i=1,2$. Using a product construction, it is
now easy to obtain a rational transduction $T$ with $TB_{2}=L_{1}\cap L_{2}$.∎

The proof of Theorem 3.1 will require one more auxiliary lemma. In the
following, $[w]_{\Gamma}$ denotes the congruence class of $w\in
X_{\Gamma}^{*}$ with respect to $\equiv_{\Gamma}$.

######  Lemma .

Let $\Gamma=(V,E)$ be a graph, let $W\subseteq V$ be a subset of vertices, and
let $Y\subseteq X_{\Gamma}$ be defined as $Y=\\{a_{w},\bar{a}_{w}\mid w\in
W\\}$. Then $u\equiv_{\Gamma}v$ implies $\pi_{Y}(u)\equiv_{\Gamma}\pi_{Y}(v)$
for $u,v\in X_{\Gamma}^{*}$.

###### Proof.

An inspection of the rules in the Thue system $T_{\Gamma}$ reveals that if
$(u,v)\in R_{\Gamma}$, then either $(\pi_{Y}(u),\pi_{Y}(v))=(u,v)$ or
$\pi_{Y}(u)=\pi_{Y}(v)$. In any case, $\pi_{Y}(u)\equiv_{\Gamma}\pi_{Y}(v)$.
Since $\equiv_{\Gamma}$ is a congruence and $\pi_{Y}$ a morphism, this implies
the Section.∎

Note that the foregoing Section does not hold for arbitrary alphabets
$Y\subseteq X_{\Gamma}$. For example, if $V=\\{1\\}$,
$X_{\Gamma}=\\{a_{1},\bar{a}_{1}\\}$, and $Y=\\{a_{1}\\}$, then
$a_{1}\bar{a}_{1}\equiv_{\Gamma}\varepsilon$, but
$a_{1}\not\equiv_{\Gamma}\varepsilon$.

We are now ready to prove Theorem 3.1.

######  Theorem 3.1.

Observe that $w\equiv_{\Gamma}\varepsilon$ if and only if $w$ can be
transformed into $\varepsilon$ by finitely many times replacing an infix $u$
with an infix $v$ for some $(u,v)\in R_{\Gamma}$. Since $R_{\Gamma}$ is
finite, this implies that the set of all $w\in X_{\Gamma}^{*}$ with
$w\equiv_{\Gamma}\varepsilon$ is recursively enumerable. (In fact, whether
$w\equiv_{\Gamma}\varepsilon$ can be decided in polynomial time [19, 23].) In
particular, one can recursively enumerate runs of valence automata over
$\mathsf{VA}(\mathbb{M}\Gamma)$ and hence
$\mathsf{VA}(\mathbb{M}\Gamma)\subseteq\mathsf{RE}$. For the other inclusion,
recall that $\mathsf{VA}(M)$ is a full trio for any monoid $M$. Furthermore,
if $\Delta$ is an induced subgraph of $\Gamma$, then $\mathbb{M}\Delta$ embeds
into $\mathbb{M}\Gamma$, meaning
$\mathsf{VA}(\mathbb{M}\Delta)\subseteq\mathsf{VA}(\mathbb{M}\Gamma)$. Hence,
according to Section 4, it suffices to show that
$B_{2}\in\mathsf{VA}(\mathbb{M}\Gamma)$ if $\Gamma^{-}$ equals $\mathsf{C4}$
or $\mathsf{P4}$.

$2$$4$$3$$1$ Figure 3. Graphs $\Gamma$ where $\Gamma^{-}$ is $\mathsf{C4}$ or
$\mathsf{P4}$. Dotted lines represent edges that may or may not exist in
$\Gamma$.

Let $X=\\{a_{1},\bar{a}_{1},b_{1},a_{2},\bar{a}_{2},b_{2}\\}$. and
$\Gamma=(V,E)$. If $\Gamma^{-}$ equals $\mathsf{C4}$ or $\mathsf{P4}$, then
$V=\\{1,2,3,4\\}$ with $\\{3,1\\},\\{1,2\\},\\{2,4\\}\in E$ and
$\\{1,4\\},\\{2,3\\}\notin E$. See Fig. 3. We construct a valence automaton
$\mathcal{A}$ over $\mathbb{M}\Gamma$ for $B_{2}\subseteq X^{*}$ as follows.
First, $\mathcal{A}$ reads a word in
$R=((a_{1}^{*}\bar{a}_{1}^{*})b_{1})^{*}\shuffle((a_{2}^{*}\bar{a}_{2}^{*})b_{2})^{*}$.
Here, when reading $a_{i}$ or $\bar{a}_{i}$, it multiplies $[a_{i}]$ or
$[\bar{a}_{i}]$, respectively, to the storage monoid. When reading $b_{1}$ or
$b_{2}$, it multiplies $[a_{4}]$ or $[a_{3}]$, respectively. After this,
$\mathcal{A}$ switches to another state and nondeterministically multiplies an
element from $\\{[\bar{a}_{4}],[\bar{a}_{3}]\\}^{*}$. Then it changes into an
accepting state. We shall prove that $\mathcal{A}$ accepts $B_{2}$. Let the
morphism $h\colon X^{*}\to\\{a_{i},\bar{a}_{i}\mid 1\leq i\leq 4\\}^{*}$ be
defined by $h(a_{i})=a_{i}$ and $h(\bar{a}_{i})=\bar{a}_{i}$ for $i=1,2$ and
$h(b_{1})=a_{4}$ and $h(b_{2})=a_{3}$.

Suppose $w\in\mathsf{L}(\mathcal{A})$. Then $w\in R$ and there is a
$v\in\\{\bar{a}_{4},\bar{a}_{3}\\}^{*}$ with
$[h(w)v]_{\Gamma}=[\varepsilon]_{\Gamma}$. Let
$w_{i}=\pi_{\\{a_{i},\bar{a}_{i},b_{i}\\}}(w)$. If we can show
$w_{i}\in(\\{a_{i}^{n}\bar{a}_{i}^{n}\mid n\geq 0\\}^{*}b_{i})^{*}$ for
$i=1,2$, then clearly $w\in B_{2}$. For symmetry reasons, it suffices to prove
this for $i=1$. Let $Y=\\{a_{1},\bar{a}_{1},a_{4},\bar{a}_{4}\\}$. Since
$[h(w)v]_{\Gamma}=[\varepsilon]_{\Gamma}$, we have in particular
$[\pi_{Y}(h(w)v)]_{\Gamma}=[\varepsilon]_{\Gamma}$ by Section 4. Moreover,

$\pi_{Y}(h(w)v)=a_{1}^{n_{1}}\bar{a}_{1}^{\bar{n}_{1}}a_{4}\cdots
a_{1}^{n_{k}}\bar{a}_{1}^{\bar{n}_{k}}a_{4}\bar{a}_{4}^{m}$

for some $n_{1},\ldots,n_{k},\bar{n}_{1},\ldots,\bar{n}_{k},m\in\mathbb{N}$.
Again, by projecting to $\\{a_{4},\bar{a}_{4}\\}^{*}$, we obtain
$[a_{4}^{k}\bar{a}_{4}^{m}]_{\Gamma}=[\varepsilon]_{\Gamma}$ and hence $k=m$.
If $n_{k}\neq\bar{n}_{k}$, then it is easy to see that $\pi_{Y}(h(w)v)$ cannot
be reduced to $\varepsilon$, since there is no edge $\\{1,4\\}$ in $\Gamma$.
Therefore, we have $n_{k}=\bar{n}_{k}$. It follows inductively that
$n_{i}=\bar{n}_{i}$ for all $1\leq i\leq k$. Since
$w_{i}=a_{1}^{n_{1}}\bar{a}_{1}^{\bar{n}_{1}}b_{1}\cdots
a_{1}^{n_{k}}\bar{a}_{1}^{\bar{n}_{k}}b_{1}$, this implies
$w_{i}\in(\\{a_{1}^{n}\bar{a}_{1}^{n}\mid n\geq 0\\}b_{1})^{*}$.

We shall now prove $B_{2}\subseteq\mathsf{L}(\mathcal{A})$. Let $g\colon
X^{*}\to\\{\bar{a}_{3},\bar{a}_{4}\\}$ be the morphism defined by
$g(a_{i})=g(\bar{a}_{i})=\varepsilon$ and $g(b_{1})=\bar{a}_{4}$ and
$g(b_{2})=\bar{a}_{3}$. We show by induction on $|w|$ that $w\in B_{2}$
implies $[h(w){g(w)}^{R}]_{\Gamma}=[\varepsilon]_{\Gamma}$. Since for each
$w\in B_{2}$, $\mathcal{A}$ clearly has a run that puts
$[h(w){g(w)}^{R}]_{\Gamma}$ into the storage, this establishes
$B_{2}\subseteq\mathsf{L}(\mathcal{A})$. Suppose $\pi_{\\{b_{1},b_{2}\\}}(w)$
ends in $b_{1}$. Then $w=rsb_{1}$ for some $r\in X^{*}$,
$s\in(a_{1}^{n}\bar{a}_{1}^{n})\shuffle t$ with $n\in\mathbb{N}$ and
$t\in\\{a_{2},\bar{a}_{2},b_{2}\\}^{*}$. Note that then $rt\in B_{2}$. Since
there are edges $\\{1,2\\},\\{1,3\\}$ in $\Gamma$, we have
$[h(s)]_{\Gamma}=[h(ta_{1}^{n}\bar{a}_{1}^{n})]_{\Gamma}$. Moreover, since $g$
deletes $a_{1}$ and $\bar{a}_{1}$, we have $g(s)=g(t)$. Therefore,

$\displaystyle[h(w){g(w)}^{R}]_{\Gamma}$
$\displaystyle=[h(rsb_{1}){g(rsb_{1})}^{R}]_{\Gamma}=[h(rta_{1}^{n}\bar{a}_{1}^{n}b_{1}){g(rtb_{1})}^{R}]_{\Gamma}$
$\displaystyle=[h(rt)a_{1}^{n}\bar{a}_{1}^{n}a_{4}\bar{a}_{4}{g(rt)}^{R}]_{\Gamma}=[h(rt){g(rt)}^{R}]_{\Gamma}.$

By induction, we have $[h(rt){g(rt)}^{R}]_{\Gamma}=[\varepsilon]_{\Gamma}$ and
hence $[h(w){g(w)}^{R}]_{\Gamma}=[\varepsilon]_{\Gamma}$. If
$\pi_{\\{b_{1},b_{2}\\}}(w)$ ends in $b_{2}$, then one can show
$[h(w){g(w)}^{R}]_{\Gamma}=[\varepsilon]_{\Gamma}$ completely analogously.
This proves $B_{2}\subseteq\mathsf{L}(\mathcal{A})$ and hence the Theorem.∎

##  5\. Decidability

In this Section, we prove Theorem 3.2 and Section 3. First, we mention
existing results that are ingredients to our proofs.

Let $\mathcal{C}$ be a class of languages. A _$\mathcal{C}$ -grammar_ is a
quadruple $G=(N,T,P,S)$ where $N$ and $T$ are disjoint alphabets and $S\in N$.
$P$ is a finite set of pairs $(A,M)$ with $A\in N$ and $M\subseteq(N\cup
T)^{*}$, $M\in\mathcal{C}$. A pair $(A,M)\in P$ is called a _production of
$G$_. We write $x\Rightarrow_{G}y$ if $x=uAv$ and $y=uwv$ for some
$u,v,w\in(N\cup T)^{*}$ and $(A,M)\in P$ with $w\in M$. Moreover,
$x\Rightarrow^{n}_{G}y$ means that there are $x_{0},\ldots,x_{n}\in(N\cup
T)^{*}$ with $x_{i-1}\Rightarrow_{G}x_{i}$ for $1\leq i\leq n$ and $x_{0}=x$
and $x_{n}=y$. Furthermore, we have $x\Rightarrow^{*}_{G}y$ if
$x\Rightarrow^{n}_{G}y$ for some $n\geq 0$. The _language generated by $G$_ is
$\mathsf{L}(G)=\\{w\in T^{*}\mid S\Rightarrow^{*}_{G}w\\}$. The class of all
languages that are generated by $\mathcal{C}$-grammars is called the
_algebraic extension of $\mathcal{C}$_ and is denoted
$\mathsf{Alg}(\mathcal{C})$. Of course, if $\mathcal{C}\subseteq\mathcal{D}$,
then $\mathsf{Alg}(\mathcal{C})\subseteq\mathsf{Alg}(\mathcal{D})$. Moreover,
it is easy to see that if $\mathcal{C}\subseteq\mathsf{Alg}(\mathcal{D})$,
then $\mathsf{Alg}(\mathcal{C}\cup\mathcal{D})=\mathsf{Alg}(\mathcal{D})$.

The following is easy to show in the same way one shows that the context-free
languages constitute a full trio [3]. A proof can be found in [23].

######  Lemma .

If $\mathcal{C}$ is a full trio, then $\mathsf{Alg}(\mathcal{C})$ is a full
trio as well.

A monoid $M$ is called _finitely generated_ if there is a finite subset
$F\subseteq M$ such that every element of $M$ can be written as a product of
elements of $F$. A language $I\subseteq X^{*}$ is called an _identity language
for $M$_ if there is a surjective morphism $\varphi\colon X^{*}\to M$ with
$I=\varphi^{-1}(1)$. We will also use the following well-known fact about
valence automata. A proof can be found, e.g., in [23, 10].

######  Proposition .

Let $M$ be a finitely generated monoid. Then:

  1. (1)

$\mathsf{VA}(M)$ is the smallest full trio containing all identity languages
of $M$.

  2. (2)

If $L$ is any identity language of $M$, then $\mathsf{VA}(M)$ is the smallest
full trio containing $L$.

The well-known theorem of Chomsky and Schützenberger [3], expressed in terms
of valence automata, states that $\mathsf{VA}(\mathbb{Z}*\mathbb{Z})$ is the
class of context-free languages. This formulation, along with a new proof, is
due to Kambites [10]. Let $\mathsf{Reg}$ and $\mathsf{CF}$ denote the class of
regular and context-free languages, respectively. Then we have
$\mathsf{Reg}=\mathsf{VA}(\mathbf{1})$ and
$\mathsf{CF}=\mathsf{Alg}(\mathsf{Reg})$. Here, $\mathbf{1}$ denotes the
trivial monoid $\\{1\\}$. Moreover, notice that
$\mathsf{Alg}(\mathsf{Alg}(\mathcal{C}))=\mathsf{Alg}(\mathcal{C})$ for every
language class $\mathcal{C}$. Since furthermore valence automata over
$\mathbb{B}*\mathbb{B}$ are equivalent to pushdown automata, we have in
summary:

(1)
$\mathsf{CF}=\mathsf{VA}(\mathbb{B}*\mathbb{B})=\mathsf{Alg}(\mathsf{VA}(\mathbf{1}))=\mathsf{Alg}(\mathsf{CF})=\mathsf{VA}(\mathbb{Z}*\mathbb{Z}).$

In order to work with general free products, we use the following result,
which expresses the languages in $\mathsf{VA}(M_{0}*M_{1})$ in terms of
$\mathsf{VA}(M_{0})$ and $\mathsf{VA}(M_{1})$. It was first shown in [19]. In
[4], it was extended to more general products. For the convenience of the
reader, we include a proof.

######  Proposition  ([19]).

Let $M_{0}$ and $M_{1}$ be monoids. Then $\mathsf{VA}(M_{0}*M_{1})$ is
included in $\mathsf{Alg}(\mathsf{VA}(M_{0})\cup\mathsf{VA}(M_{1}))$.

###### Proof.

For every monoid $M$, we have $\mathsf{VA}(M)=\bigcup_{N}\mathsf{VA}(N)$,
where $N$ ranges over the finitely generated submonoids of $M$. Moreover,
every finitely generated submonoid of $M_{0}*M_{1}$ is included in some
$N_{0}*N_{1}$, where $N_{i}$ is a finitely generated submonoid of $M_{i}$, for
$i=0,1$. Therefore, we have
$\mathsf{VA}(M_{0}*M_{1})=\bigcup_{N_{0},N_{1}}\mathsf{VA}(N_{0}*N_{1})$,
where $N_{i}$ ranges over the finitely generated submonoids of $M_{i}$, for
$i=0,1$. Thus, it suffices to show the Section in the case that $M_{0}$ and
$M_{1}$ are finitely generated.

For $i=0,1$, let $(A_{i},R_{i})$ be a presentation of $M_{i}$ such that
$A_{i}$ is finite. Then $M_{0}*M_{1}$ is presented by $(A_{0}\cup
A_{1},R_{0}\cup R_{1})$. Consider the languages $L_{i}=\\{w\in A_{i}^{*}\mid
w\equiv_{R_{i}}\varepsilon\\}$ for $i\in\\{0,1\\}$. Then $L_{i}$ is an
identity language of $M_{i}$ and hence contained in $\mathsf{VA}(M_{i})$.
Moreover, by definition of $M_{0}*M_{1}$, the language $L=\\{w\in(A_{0}\cup
A_{1})^{*}\mid w\equiv_{R_{0}\cup R_{1}}\varepsilon\\}$ is an identity
language of $M_{0}*M_{1}$.

According to Section 5, the class
$\mathsf{Alg}(\mathsf{VA}(M_{0})\cup\mathsf{VA}(M_{1}))$ is a full trio. Thus,
Section 5 tells us that it suffices to show that the identity language $L$ of
$M_{0}*M_{1}$ is contained in
$\mathsf{Alg}(\mathsf{VA}(M_{0})\cup\mathsf{VA}(M_{1}))$.

Consider the binary relation $\rightharpoonup$ on $(A_{0}\cup A_{1})^{*}$
where $u\rightharpoonup v$ if and only if for some $i\in\\{0,1\\}$, there are
$x,z\in(A_{0}\cup A_{1})^{*}$, $y\in A_{i}^{*}$, such that $u=xz$, $v=xyz$,
and $y\equiv_{R_{i}}\varepsilon$. It is now easy to see that
$w\equiv_{R_{0}\cup R_{1}}\varepsilon$ if and only if
$\varepsilon\rightharpoonup^{*}w$.

This allows us to construct a
$\mathsf{VA}(M_{0})\cup\mathsf{VA}(M_{1})$-grammar for $L$. Let
$G=(N,A_{0}\cup A_{1},P,S)$, where $N=\\{S\\}$. In order to describe the
productions, we need to define two languages. For $i\in\\{0,1\\}$, let

$K_{i}=\\{Sa_{1}S\cdots a_{n}S\mid a_{1},\ldots,a_{n}\in
A_{i},~{}~{}a_{1}\cdots a_{n}\in L_{i}\\}.$

Then $K_{i}$ can be obtained from $L_{i}$ using full trio operations and is
thus contained in $\mathsf{VA}(M_{i})$. Our grammar contains only three
productions: $S\to K_{0}$, $S\to K_{1}$, and $S\to\\{\varepsilon\\}$ (recall
that as a regular language, $\\{\varepsilon\\}$ belongs to each
$\mathsf{VA}(M_{i})$). Then, it is immediate that $w\in\mathsf{L}(G)$ if and
only if $\varepsilon\rightharpoonup^{*}w$ and hence $\mathsf{L}(G)=L$.∎

Section 5 tells us that the languages in $\mathsf{VA}(M_{0}*M_{1})$ are
confined to the algebraic extension of
$\mathsf{VA}(M_{0})\cup\mathsf{VA}(M_{1})$. Our next ingredient, Section 5,
will complement Section 5 by describing monoids $N$ such that the algebraic
extension of $\mathsf{VA}(M)$ is confined to $\mathsf{VA}(N)$. We need two
auxiliary lemmas, for which the following notation will be convenient. We
write $M\hookrightarrow N$ for monoids $M,N$ if there is a morphism
$\varphi\colon M\to N$ such that $\varphi^{-1}(1)=\\{1\\}$. Clearly, if
$M\hookrightarrow N$, then $\mathsf{VA}(M)\subseteq\mathsf{VA}(N)$: Replacing
in a valence automaton over $M$ all elements $m\in M$ with $\varphi(m)$ yields
a valence automaton over $N$ that accepts the same language.

######  Lemma .

If $M\hookrightarrow M^{\prime}$ and $N\hookrightarrow N^{\prime}$, then we
have $M*N\hookrightarrow M^{\prime}*N^{\prime}$.

###### Proof.

Let $\varphi\colon M\to M^{\prime}$ and $\psi\colon N\to N^{\prime}$ be
morphisms with $\varphi^{-1}(1)=\\{1\\}$ and $\psi^{-1}(1)=\\{1\\}$. Then
defining $\kappa\colon M*N\to M^{\prime}*N^{\prime}$ as the morphism with
$\kappa|_{M}=\varphi$ and $\kappa|_{N}=\psi$ clearly yields
$\kappa^{-1}(1)=1$.∎

For a monoid $M$, we define $R_{1}(M)=\\{x\in M\mid\exists y\in M\colon
xy=1\\}$. Observe that the set $R_{1}(M)$ can be thought of as the storage
contents that can occur in a valid run of a valence automaton over $M$. The
following result appeared first in [20]. We include a proof for the
convenience of the reader.

######  Lemma  ([20]).

Let $M$ be a monoid with $R_{1}(M)\neq\\{1\\}$. Then we have
$\mathbb{B}^{(n)}*M\hookrightarrow\mathbb{B}*M$ for every $n\geq 1$. In
particular, $\mathsf{VA}(\mathbb{B}*M)=\mathsf{VA}(\mathbb{B}^{(n)}*M)$ for
every $n\geq 1$.

###### Proof.

Observe that if $\mathbb{B}^{(n)}*M\hookrightarrow\mathbb{B}*M$ and
$\mathbb{B}*\mathbb{B}*M\hookrightarrow\mathbb{B}*M$, then

$\mathbb{B}^{(n+1)}*M\cong\mathbb{B}*(\mathbb{B}^{(n)}*M)\hookrightarrow\mathbb{B}*(\mathbb{B}*M)\hookrightarrow\mathbb{B}*M.$

Therefore, it suffices to prove
$\mathbb{B}*\mathbb{B}*M\hookrightarrow\mathbb{B}*M$.

Let $\mathbb{B}_{s}=\langle s,\bar{s}\mid s\bar{s}=1\rangle$ for
$s\in\\{p,q,r\\}$. We show
$\mathbb{B}_{p}*\mathbb{B}_{q}*M\hookrightarrow\mathbb{B}_{r}*M$. Suppose $M$
is presented by $(X,R)$. We regard the monoids
$\mathbb{B}_{p}*\mathbb{B}_{q}*M$ and $\mathbb{B}_{r}*M$ as embedded into
$\mathbb{B}_{p}*\mathbb{B}_{q}*\mathbb{B}_{r}*M$, which by definition of the
free product, has a presentation $(Y,S)$, where
$Y=\\{p,\bar{p},q,\bar{q},r,\bar{r}\\}\cup X$ and $S$ consists of $R$ and the
equations $s\bar{s}=1$ for $s\in\\{p,q,r\\}$. For $w\in Y^{*}$, we write $[w]$
for the class of $w$ in the congruence generated by $S$. Since
$R_{1}(M)\neq\\{1\\}$, we find $u,v\in X^{*}$ with $[uv]=1$ and $[u]\neq 1$.

Observe that then for any $f,g\in(\\{r,\bar{r}\\}\cup X)^{*}$, we have
$[frv\bar{r}g]\neq 1$: By induction on the number of rewriting steps, one can
show that every word in $[frv\bar{r}g]$ is of the form
$f^{\prime}rv^{\prime}\bar{r}g^{\prime}$ for
$f^{\prime},g^{\prime}\in(\\{r,\bar{r}\\}\cup X)^{*}$ and $v^{\prime}\in
X^{*}$ with $v^{\prime}\equiv_{R}v$. By the same argument, we have
$[fru\bar{r}g]\neq 1$ for any $f,g\in(\\{r,\bar{r}\\}\cup X)^{*}$.

Let $\varphi\colon(\\{p,\bar{p},q,\bar{q}\\}\cup X)^{*}\to(\\{r,\bar{r}\\}\cup
X)^{*}$ be the morphism with $\varphi(x)=x$ for $x\in X$ and

$\displaystyle p$ $\displaystyle\mapsto rr,$ $\displaystyle\bar{p}$
$\displaystyle\mapsto\bar{r}\bar{r},$ $\displaystyle q$ $\displaystyle\mapsto
rur,$ $\displaystyle\bar{q}$ $\displaystyle\mapsto\bar{r}v\bar{r}.$

We show by induction on $|w|$ that $[\varphi(w)]=1$ implies $[w]=1$. Since
this is trivial for $w=\varepsilon$, we assume $|w|\geq 1$. Now suppose
$[\varphi(w)]=[\varepsilon]$ for some $w\in(\\{p,\bar{p},q,\bar{q}\\}\cup
X)^{*}$. If $w\in X^{*}$, then $[\varphi(w)]=[w]$ and hence $[w]=1$.
Otherwise, we have $\varphi(w)=xry\bar{r}z$ for some $y\in X^{*}$ with $[y]=1$
and $[xz]=1$. This means $w=fsy\overline{s^{\prime}}g$ for
$s,s^{\prime}\in\\{p,q\\}$ with $\varphi(fs)=xr$ and
$\varphi(\overline{s^{\prime}}g)=\bar{r}z$. If $s\neq s^{\prime}$, then $s=p$
and $s^{\prime}=q$; or $s=q$ and $s^{\prime}=p$. In the former case

$[\varphi(w)]=[\varphi(f)~{}rr~{}y~{}\bar{r}v\bar{r}~{}\varphi(g)]=[\varphi(f)rv\bar{r}\varphi(g)]\neq
1$

by our observation above and in the latter

$[\varphi(w)]=[\varphi(f)~{}rur~{}y~{}\bar{r}\bar{r}~{}\varphi(g)]=[\varphi(f)ru\bar{r}\varphi(g)]\neq
1,$

again by our observation. Hence $s=s^{\prime}$. This means
$[w]=[fsy\bar{s}g]=[fg]$ and also $1=[\varphi(w)]=[\varphi(fg)]$ and since
$|fg|<|w|$, induction yields $[w]=[fg]=1$.

Hence, we have shown that $[\varphi(w)]=1$ implies $[w]=1$. Since, on the
other hand, $[u]=[v]$ implies $[\varphi(u)]=[\varphi(v)]$ for all
$u,v\in(\\{p,\bar{p},q,\bar{q}\\}\cup X)^{*}$, we can lift $\varphi$ to a
morphism witnessing
$\mathbb{B}_{p}*\mathbb{B}_{q}*M\hookrightarrow\mathbb{B}_{r}*M$.∎

As a partial converse to Section 5, we have the following. It was first shown
in [20]. Since valence automata over $\mathbb{B}*\mathbb{B}$ are essentially
pushdown automata and since
$\mathsf{Alg}(\mathsf{VA}(\mathbf{1}))=\mathsf{Alg}(\mathsf{Reg})=\mathsf{CF}$,
the equality
$\mathsf{VA}(\mathbb{B}*\mathbb{B}*M)=\mathsf{Alg}(\mathsf{VA}(M))$
generalizes the equivalence between pushdown automata and context-free
grammars.

######  Proposition  ([20]).

For every monoid $M$,
$\mathsf{VA}(\mathbb{B}*\mathbb{B}*M)=\mathsf{Alg}(\mathsf{VA}(M))$. Moreover,
if $R_{1}(M)\neq\\{1\\}$, then
$\mathsf{VA}(\mathbb{B}*M)=\mathsf{Alg}(\mathsf{VA}(M))$.

###### Proof.

It suffices to prove the first statement: If $R_{1}(M)\neq\\{1\\}$, then
Section 5 implies
$\mathsf{VA}(\mathbb{B}*M)=\mathsf{VA}(\mathbb{B}*\mathbb{B}*M)$. Observe that
if $\mathcal{C}$ is a language class with $\mathcal{C}\subseteq\mathsf{CF}$,
then
$\mathsf{Alg}(\mathcal{C}\cup\mathsf{VA}(N))=\mathsf{Alg}(\mathsf{VA}(N))$ for
every monoid $N$: For each production $A\to L$ in a
$(\mathcal{C}\cup\mathsf{VA}(N))$-grammar $G$ with $L$ from $\mathcal{C}$, we
can take a context-free grammar $G^{\prime}$ generating $L$ (with fresh non-
terminals) and replace the production $A\to L$ with the productions of
$G^{\prime}$. This is yields a $\mathsf{VA}(N)$-grammar because all singleton
sets are contained in $\mathsf{VA}(N)$. Therefore, since the languages in
$\mathsf{VA}(\mathbb{B})$ are effectively context-free, Section 5 yields

$\mathsf{VA}(\mathbb{B}*N)\subseteq\mathsf{Alg}(\mathsf{VA}(\mathbb{B})\cup\mathsf{VA}(N))=\mathsf{Alg}(\mathsf{VA}(N))$

for every monoid $N$. Therefore,

$\mathsf{VA}(\mathbb{B}*\mathbb{B}*M)\subseteq\mathsf{Alg}(\mathsf{VA}(\mathbb{B}*M))\subseteq\mathsf{Alg}(\mathsf{Alg}(\mathsf{VA}(M)))=\mathsf{Alg}(\mathsf{VA}(M)).$

It remains to be shown that
$\mathsf{Alg}(\mathsf{VA}(M))\subseteq\mathsf{VA}(\mathbb{B}*\mathbb{B}*M)$.

Suppose $G=(N,T,P,S)$ is a $\mathsf{VA}(M)$-grammar and let $X=N\cup T$. Since
$\mathsf{VA}(M)$ is closed under union, we may assume that for each $B\in N$,
there is precisely one production $B\to L_{B}$ in $P$. For each nonterminal
$B\in N$, there is a valence automaton
$\mathcal{A}_{B}=(Q_{B},X,M,E_{B},q^{B}_{0},F_{B})$ over $M$ with
$\mathsf{L}(\mathcal{A}_{B})=L_{B}$. We may clearly assume that $Q_{B}\cap
Q_{C}=\emptyset$ for $B\neq C$ and that for each $(p,w,m,q)\in E_{B}$, we have
$|w|\leq 1$.

In order to simplify the correctness proof, we modify $G$. Let $\lfloor$ and
$\rfloor$ be new symbols and let $G^{\prime}$ be the grammar
$G^{\prime}=(N,T\cup\\{\lfloor,\rfloor\\},P^{\prime},S)$, where $P^{\prime}$
consists of the productions $B\to\lfloor L\rfloor$ for $B\to L\in P$.
Moreover, let

$K=\\{v\in(N\cup T\cup\\{\lfloor,\rfloor\\})^{*}\mid
u\Rightarrow^{*}_{G^{\prime}}v,~{}u\in L_{S}\\}.$

Then $\mathsf{L}(G)=\pi_{T}(K\cap(T\cup\\{\lfloor,\rfloor\\})^{*})$ and it
suffices to show $K\in\mathsf{VA}(\mathbb{B}*\mathbb{B}*M)$.

Let $Q=\bigcup_{B\in N}Q_{B}$. For each $q\in Q$, let $\mathbb{B}_{q}=\langle
q,\bar{q}\mid q\bar{q}=1\rangle$ be an isomorphic copy of $\mathbb{B}$. Let
$M^{\prime}=\mathbb{B}_{q_{1}}*\cdots*\mathbb{B}_{q_{n}}*M$, where
$Q=\\{q_{1},\ldots,q_{n}\\}$. We shall prove $K\in\mathsf{VA}(M^{\prime})$,
which implies $K\in\mathsf{VA}(\mathbb{B}*\mathbb{B}*M)$ by Section 5 since
$R_{1}(\mathbb{B}*M)\neq\\{1\\}$.

Let $E=\bigcup_{B\in N}E_{B}$, $F=\bigcup_{B\in N}F_{B}$. The new set
$E^{\prime}$ consists of the following transitions:

(2) $\displaystyle(p,x,m,q)$ for $(p,x,m,q)\in E$, (3)
$\displaystyle(p,\lfloor,mq,q^{B}_{0})$ for $(p,B,m,q)\in E$, $B\in N$, (4)
$\displaystyle(p,\rfloor,\bar{q},q)$ for $p\in F$, $q\in Q$.

We claim that with $\mathcal{A}^{\prime}=(Q,N\cup
T\cup\\{\lfloor,\rfloor\\},M^{\prime},E^{\prime},q_{0}^{S},F)$, we have
$\mathsf{L}(\mathcal{A}^{\prime})=K$.

Let $v\in K$, where $u\Rightarrow^{n}_{G^{\prime}}v$ for some $u\in L_{S}$. We
show $v\in\mathsf{L}(\mathcal{A}^{\prime})$ by induction on $n$. For $n=0$, we
have $v\in L_{S}$ and can use transitions of type 2 inherited from
$\mathcal{A}_{S}$ to accept $v$. If $n\geq 1$, let
$u\Rightarrow^{n-1}_{G^{\prime}}v^{\prime}\Rightarrow_{G^{\prime}}v$. Then
$v^{\prime}\in\mathsf{L}(\mathcal{A}^{\prime})$ and $v^{\prime}=xBy$,
$v=x\lfloor w\rfloor y$ for some $B\in N$, $w\in L_{B}$. The run for
$v^{\prime}$ uses a transition $(p,B,m,q)\in E$. Instead of using this
transition, we can use $(p,\lfloor,mq,q_{0}^{B})$, then execute the 2-type
transitions for $w\in L_{B}$, and finally use $(f,\rfloor,\bar{q},q)$, where
$f$ is the final state in the run for $w$. This has the effect of reading
$\lfloor w\rfloor$ from the input and multiplying $mq1\bar{q}=m$ to the
storage monoid. Hence, the new run is valid and accepts $v$. Hence,
$v\in\mathsf{L}(\mathcal{A}^{\prime})$. This proves
$K\subseteq\mathsf{L}(\mathcal{A}^{\prime})$.

In order to show $\mathsf{L}(\mathcal{A}^{\prime})\subseteq K$, consider the
morphisms $\varphi\colon(T\cup\\{\lfloor,\rfloor\\})^{*}\to\mathbb{B}$,
$\psi\colon M^{\prime}\to\mathbb{B}$ with $\varphi(x)=1$ for $x\in T$,
$\varphi(\lfloor)=a$, $\varphi(\rfloor)=\bar{a}$, $\psi(q)=a$ for $q\in Q$,
$\psi(\bar{q})=\bar{a}$, and $\psi(m)=1$ for $m\in M$. The transitions of
$\mathcal{A}^{\prime}$ are constructed such that
$(p,\varepsilon,1)\rightarrow^{*}_{\mathcal{A}^{\prime}}(q,w,m)$ implies
$\varphi(w)=\psi(m)$. In particular, if
$v\in\mathsf{L}(\mathcal{A}^{\prime})$, then $\pi_{\\{\lfloor,\rfloor\\}}(v)$
is a semi-Dyck word with respect to $\lfloor$ and $\rfloor$.

Let $v\in\mathsf{L}(\mathcal{A}^{\prime})$ and let $n=|w|_{\lfloor}$. We show
$v\in K$ by induction on $n$. If $n=0$, then the run for $v$ only used
transitions of type 2 and hence $v\in L_{S}$. If $n\geq 1$, since
$\pi_{\\{\lfloor,\rfloor\\}}(v)$ is a semi-Dyck word, we can write $v=x\lfloor
w\rfloor y$ for some $w\in(N\cup T)^{*}$. Since $\lfloor$ and $\rfloor$ can
only be produced by transitions of the form 3 and 4, respectively, the run for
$v$ has to be of the form

$\displaystyle(q_{0}^{S},\varepsilon,1)$
$\displaystyle\rightarrow^{*}_{\mathcal{A}^{\prime}}(p,x,r)$
$\displaystyle\rightarrow_{\mathcal{A}^{\prime}}(q_{0}^{B},x\lfloor,rmq)$
$\displaystyle\rightarrow^{*}_{\mathcal{A}^{\prime}}(f,x\lfloor w,rmqs)$
$\displaystyle\rightarrow_{\mathcal{A}^{\prime}}(q^{\prime},x\lfloor
w\rfloor,rmqs\overline{q^{\prime}})$
$\displaystyle\rightarrow^{*}_{\mathcal{A}^{\prime}}(f^{\prime},x\lfloor
w\rfloor y,rmqs\overline{q^{\prime}}t)$

for some $p,q,q^{\prime}\in Q$, $B\in N$, $(p,B,m,q)\in E$, $f,f^{\prime}\in
F$, $r,t\in M^{\prime}$, and $s\in M$ and with $rmqs\overline{q^{\prime}}t=1$.
This last condition implies $s=1$ and $q=q^{\prime}$, which in turn entails
$rmt=1$. This also means $(p,B,m,q^{\prime})=(p,B,m,q)\in E$ and
$(q_{0}^{B},\varepsilon,1)\rightarrow^{*}_{\mathcal{A}^{\prime}}(f,w,s)=(f,w,1)$
and hence $w\in L_{B}$. Using the transition $(p,B,m,q^{\prime})\in E$, we
have

$\displaystyle(q_{0}^{S},\varepsilon,1)$
$\displaystyle\rightarrow^{*}_{\mathcal{A}^{\prime}}(p,x,r)$
$\displaystyle\rightarrow_{\mathcal{A}^{\prime}}(q^{\prime},xB,rm)$
$\displaystyle\rightarrow^{*}_{\mathcal{A}^{\prime}}(f^{\prime},xBy,rmt).$

Hence $xBy\in\mathsf{L}(\mathcal{A}^{\prime})$ and
$|xBy|_{\lfloor}<|v|_{\lfloor}$. Thus, induction yields $xBy\in K$ and since
$xBy\Rightarrow_{G^{\prime}}x\lfloor w\rfloor y$, we have $v=x\lfloor w\rfloor
y\in K$. This proves $\mathsf{L}(\mathcal{A}^{\prime})=K$.∎

For two language classes $\mathcal{C}$ and $\mathcal{D}$, we will consider the
languages obtained by intersecting a language from $\mathcal{C}$ with a
language in $\mathcal{D}$. Since the class of these intersections might not be
well-behaved, we use a slight extension. By $\mathcal{C}\sqcap\mathcal{D}$, we
denote the class of all languages $h(K\cap L)$ where $K\subseteq X^{*}$
belongs to $\mathcal{C}$ and $L\subseteq X^{*}$ is a member of $\mathcal{D}$
and $h\colon X^{*}\to Y^{*}$ is a morphism. This allows us to state the
following characterization of $\mathsf{VA}(M\times N)$ in terms of
$\mathsf{VA}(M)$ and $\mathsf{VA}(N)$ by Kambites [10].

######  Proposition .

If $M,N$ are monoids, then $\mathsf{VA}(M\times
N)=\mathsf{VA}(M)\sqcap\mathsf{VA}(N)$.

This implies in particular that if
$\mathsf{VA}(M_{i})\subseteq\mathsf{VA}(N_{i})$ for $i\in\\{0,1\\}$, then we
also have the inclusion $\mathsf{VA}(M_{0}\times
M_{1})\subseteq\mathsf{VA}(N_{0}\times N_{1})$. Of course, this also means
that if $\mathsf{VA}(M_{i})=\mathsf{VA}(N_{i})$ for $i\in\\{0,1\\}$, then
$\mathsf{VA}(M_{0}\times M_{1})=\mathsf{VA}(N_{0}\times N_{1})$. We are now
ready to prove Section 3.

######  Section 3.

By definition, we have $\mathbb{M}\Gamma\cong\mathbb{B}\times(M_{0}*M_{1})$,
where $M_{i}\cong\mathbb{B}$ or $M_{i}\cong\mathbb{Z}$ for $i\in\\{0,1\\}$. We
show that $\mathsf{VA}(M_{0}*M_{1})=\mathsf{VA}(\mathbb{B}*\mathbb{B})$ in any
case. This suffices, since it clearly implies
$\mathsf{VA}(\mathbb{M}\Gamma)=\mathsf{VA}(\mathbb{B}^{(2)}\times\mathbb{B})$
according to Section 5. If $M_{0}\cong M_{1}\cong\mathbb{B}$, the equality
$\mathsf{VA}(M_{0}*M_{1})=\mathsf{VA}(\mathbb{B}*\mathbb{B})$ is trivial, so
we may assume $M_{0}\cong\mathbb{Z}$.

If $M_{1}\cong\mathbb{Z}$, then $M_{0}*M_{1}\cong\mathbb{Z}*\mathbb{Z}$,
meaning that $\mathsf{VA}(M_{0}*M_{1})$ is the class of context-free languages
(see Eq. 1) and thus
$\mathsf{VA}(M_{0}*M_{1})=\mathsf{VA}(\mathbb{B}*\mathbb{B})$.

If $M_{1}\cong\mathbb{B}$, then
$\mathsf{VA}(\mathbb{Z}*\mathbb{B})=\mathsf{Alg}(\mathsf{VA}(\mathbb{Z}))$ by
Section 5. Since $\mathsf{VA}(\mathbb{Z})$ is included in the context-free
languages, we have
$\mathsf{Alg}(\mathsf{VA}(\mathbb{Z}))=\mathsf{VA}(\mathbb{B}*\mathbb{B})$.∎

We shall now prove Theorem 3.2. Note that the implication “1 $\Rightarrow$ 2”
immediately follows from Theorem 3.1. The implication “2 $\Rightarrow$ 3” is
an old graph-theoretic result of Wolk.

######  Theorem 5.1 (Wolk [18]).

A simple graph is a transitive forest if and only if it does not contain
$\mathsf{C4}$ or $\mathsf{P4}$ as an induced subgraph.

The implication “3 $\Rightarrow$ 4” is a simple combinatorial observation. An
analogous fact is part of Lohrey and Steinberg’s proof of Theorem 3.3.

######  Lemma .

If $\Gamma$ is a PPN-free transitive forest, then
$\mathbb{M}\Gamma\in\mathsf{DEC}$.

###### Proof.

Let $\Gamma=(V,E)$. We proceed by induction on $|V|$. If $\Gamma$ is empty,
then $\mathbb{M}\Gamma\cong\mathbf{1}\cong\mathbb{B}^{0}\in\mathsf{DEC}$.
Hence, we assume that $\Gamma$ is non-empty. If $\Gamma$ is not connected,
then $\Gamma$ is the disjoint union of PPN-free transitive forests
$\Gamma_{1},\Gamma_{2}$, for which
$\mathbb{M}\Gamma_{1},\mathbb{M}\Gamma_{2}\in\mathsf{DEC}$ by induction.
Hence,
$\mathbb{M}\Gamma\cong\mathbb{M}\Gamma_{1}*\mathbb{M}\Gamma_{2}\in\mathsf{DEC}$.

Suppose $\Gamma$ is connected. Since $\Gamma$ is a transitive forest, there is
a vertex $v\in V$ such that $\Gamma\setminus v$ is a PPN-free transitive
forest and $v$ is adjacent to every vertex in $V\setminus\\{v\\}$. We
distinguish two cases.

  * 1

If $v$ is a looped vertex, then
$\mathbb{M}\Gamma\cong\mathbb{Z}\times\mathbb{M}(\Gamma\setminus v)$, and
$\mathbb{M}(\Gamma\setminus v)\in\mathsf{DEC}$ by induction.

  * 2

If $v$ is an unlooped vertex, then $\Gamma$ being PPN-free means that in
$\Gamma\setminus v$, any two distinct vertices are adjacent. Hence,
$\mathbb{M}\Gamma\cong\mathbb{B}^{m}\times\mathbb{Z}^{n}$, where $m$ and $n$
are the number of unlooped and looped vertices in $\Gamma$, respectively.
Therefore, $\mathbb{M}\Gamma\in\mathsf{DEC}$.

∎

For establishing Theorem 3.2, our remaining task is to prove the implication
“4 $\Rightarrow$ 1”. In light of Theorems 3.1, 5.1 and 5, this amounts to
showing that emptiness is decidable for valence automata over monoids in
$\mathsf{DEC}$. This will involve two facts (Theorem 5.2 and Section 5) about
the languages arising from monoids in $\mathsf{DEC}$.

The following generalization of Parikh’s theorem by van Leeuwen will allow us
to exploit our description of free products by algebraic extensions. If $X$ is
an alphabet, $X^{\oplus}$ denotes the set of maps $\alpha\colon
X\to\mathbb{N}$. The elements of $X^{\oplus}$ are called _multisets_. The
_Parikh map_ is the map $\Psi\colon X^{*}\to X^{\oplus}$ where
$\Psi\left(w\right)(x)$ is the number of occurrences of $x$ in $w$. By
$\mathcal{P}({S})$, we denote the power set of the set $S$. A _substitution_
is a map $\sigma\colon X\to\mathcal{P}({Y^{*}})$, where $X$ and $Y$ are
alphabets. Given $L\subseteq X^{*}$, we write $\sigma(L)$ for the set of all
words $v_{1}\cdots v_{n}$, where $v_{i}\in\sigma(x_{i})$, $1\leq i\leq n$, for
$x_{1}\cdots x_{n}\in L$ and $x_{1},\ldots,x_{n}\in X$. If $\sigma(x)$ belongs
to $\mathcal{C}$ for each $x\in X$, then $\sigma$ is a _$\mathcal{C}$
-substitution_. The class $\mathcal{C}$ is said to be _substitution closed_ if
$\sigma(L)\in\mathcal{C}$ for every member $L$ of $\mathcal{C}$ and every
$\mathcal{C}$-substitution $\sigma$.

######  Theorem 5.2 (van Leeuwen [17]).

For each substitution closed full trio $\mathcal{C}$, we have
$\Psi\left(\mathsf{Alg}(\mathcal{C})\right)=\Psi\left(\mathcal{C}\right)$.

For $\alpha,\beta\in X^{\oplus}$, let $\alpha+\beta\in X^{\oplus}$ be defined
by $(\alpha+\beta)(x)=\alpha(x)+\beta(x)$. With this operation, $X^{\oplus}$
is a monoid. For a subset $S\subseteq X^{\oplus}$, we write $S^{\oplus}$ for
the smallest submonoid of $X^{\oplus}$ containing $S$. A subset of the form
$\mu+F^{\oplus}$ for $\mu\in X^{\oplus}$ and a finite $F\subseteq X^{\oplus}$
is called _linear_. A finite union of linear sets is called _semilinear_. By
$\mathsf{SLI}(\mathcal{C})$ we denote the class of languages
$h(L\cap\Psi^{-1}(S))$, where $h\colon X^{*}\to Y^{*}$ is a morphism, $L$
belongs to $\mathcal{C}$, and $S\subseteq X^{\oplus}$ is semilinear.

######  Proposition  ([20]).

For each monoid $M$, we have

$\mathsf{SLI}(\mathsf{VA}(M))=\bigcup_{i\geq
0}\mathsf{VA}(M\times\mathbb{Z}^{i}).$

We will prove decidability for $\mathsf{DEC}$ by reducing the problem to the
reachability problem of priority multicounter machines, whose decidability has
been established by Reinhardt [15]. Priority multicounter machines are an
extension of Petri nets with one inhibitor arc. Intuitively, a priority
multicounter machine is a partially blind multicounter machine with the
additional capability of restricted zero tests: The counters are numbered from
$1$ to $k$ and for each $\ell\in\\{1,\ldots,k\\}$, there is a zero test
instruction that checks whether counters $1$ through $\ell$ are zero. Let us
define priority multicounter machines formally.

A _priority $k$-counter machine_ is a tuple $\mathcal{A}=(Q,X,E,q_{0},F)$,
where  (i) $X$is an alphabet,  (ii) $Q$is a finite set of states,  (iii) $E$is
a finite subset of $Q\times
X^{*}\times\\{0,\ldots,k\\}\times\mathbb{Z}^{k}\times Q$, and its elements are
called _edges_ or _transitions_ ,  (iv) $q_{0}\in Q$is the _initial state_ ,
and  (v) $F\subseteq Q$is the set of _final states_.  For
$\ell\in\\{0,\ldots,k\\}$, let

$\mathbb{N}^{k}_{\ell}=\\{(\mu_{1},\ldots,\mu_{k})\in\mathbb{N}^{k}\mid\mu_{1}=\ldots=\mu_{\ell}=0\\}.$

We are now ready to defines the semantics of priority counter machines. A
_configuration_ of $\mathcal{A}$ is a pair $(q,\mu)\in Q\times\mathbb{N}^{k}$.
For configurations $(q,\mu)$ and $(q^{\prime},\mu^{\prime})$, we write
$(q,\mu)\xrightarrow{w}_{\mathcal{A}}(q^{\prime},\mu^{\prime})$ if there are
$(q_{0},\mu_{0}),\ldots,(q_{n},\mu_{n})\in Q\times\mathbb{N}^{k}$ such that

  1. (i)

$(q,\mu)=(q_{0},\mu_{0})$ and $(q^{\prime},\mu^{\prime})=(q_{n},\mu_{n})$,

  2. (ii)

for each $i\in\\{1,\ldots,n\\}$, there is a transition
$(q_{i-1},w_{i},\ell,\nu,q_{i})\in E$ such that
$\mu_{i-1}\in\mathbb{N}^{k}_{\ell}$ and $\mu_{i}=\mu_{i-1}+\nu$, and
$w=w_{1}\cdots w_{n}$.

The _language accepted by $\mathcal{A}$_ is defined as

$\mathsf{L}(\mathcal{A})=\\{w\in
X^{*}\mid(q_{0},0)\xrightarrow{w}_{\mathcal{A}}(f,0)~{}~{}\text{for some $f\in
F$}\\}.$

A _priority multicounter machine_ is a priority $k$-counter machine for some
$k\in\mathbb{N}$. The class of languages accepted by priority multicounter
machines is denoted by $\mathsf{Prio}$. Reinhardt has shown that the
reachability problem for priority multicounter machines is decidable [15],
which can be reformulated as follows.

######  Theorem 5.3 (Reinhardt [15]).

The emptiness problem is decidable for priority multicounter machines.

Although the decidability proof for the emptiness problem for valence automata
over $\mathsf{SC}^{\pm}$ employs a reduction to priority multicounter
machines, it should be stressed that the mechanisms realized by
$\mathsf{SC}^{\pm}$ are quite different from priority counters and very likely
not subsumed by them in terms of accepted languages. For example,
$\mathsf{SC}^{\pm}$ contains pushdown stacks ($\mathbb{B}*\mathbb{B}$)—if the
priority multicounter machines could accept all context-free languages (or
even just the semi-Dyck language $D_{2}^{*}$), this would easily imply
decidability of the emptiness problem for pushdown Petri nets. Indeed,
$\mathsf{SC}^{\pm}$ can even realize stacks where each entry consists of $n$
partially blind counters (since
$\mathbb{B}*(\mathbb{B}^{n})\in\mathsf{SC}^{\pm}$). On the other hand,
priority multicounter machines do not seem to be subsumed by
$\mathsf{SC}^{\pm}$ either: After building stacks once, $\mathsf{SC}^{\pm}$
only allows adding _blind_ counters (and building stacks again). It therefore
seems unlikely that a mechanism in $\mathsf{SC}^{\pm}$ can accept the
languages even of a priority $2$-counter machine.

The idea of the proof of “4 $\Rightarrow$ 1” is, given a valence automaton
over some $M\in\mathsf{DEC}$, to construct a Parikh-equivalent priority
multicounter machine. This construction makes use of the following simple
fact. A full trio $\mathcal{C}$ is said to be _Presburger closed_ if
$\mathsf{SLI}(\mathcal{C})\subseteq\mathcal{C}$.

######  Lemma .

$\mathsf{Prio}$ is a Presburger closed full trio and closed under
substitutions.

###### Proof.

The fact that $\mathsf{Prio}$ is a full trio can be shown by standard automata
constructions. Given a priority multicounter machine $\mathcal{A}$ and a
semilinear set $S\subseteq X^{\oplus}$, we add $|X|$ counters to $\mathcal{A}$
that ensure that the input is contained in
$\mathsf{L}(\mathcal{A})\cap\Psi^{-1}(S)$. This proves that $\mathsf{Prio}$ is
Presburger closed.

Suppose $\sigma\colon X\to\mathcal{P}({Y^{*}})$ is a
$\mathsf{Prio}$-substitution. Furthermore, let $\mathcal{A}$ be a priority
$k$-counter machine and let $\sigma(x)$ be given by a priority $\ell$-counter
machine for each $x\in X$. We construct a priority $(\ell+k)$-counter machine
$\mathcal{B}$ from $\mathcal{A}$ by adding $\ell$ counters. $\mathcal{B}$
simulates $\mathcal{A}$ on counters $\ell+1,\ldots,\ell+k$. Whenever
$\mathcal{A}$ reads $x$, $\mathcal{B}$ uses the first $\ell$ counters to
simulate the priority $\ell$-counter machine for $\sigma(x)$. Using the zero
test on the first $\ell$ counters, it makes sure that the machine for
$\sigma(x)$ indeed ends up in a final configuration. Then clearly
$\mathsf{L}(\mathcal{B})=\sigma(\mathsf{L}(\mathcal{A}))$.∎

######  Lemma .

We have the effective inclusion
$\Psi\left(\mathsf{VA}(\mathsf{DEC})\right)\subseteq\Psi\left(\mathsf{Prio}\right)$.
More precisely, given $M\in\mathsf{DEC}$ and $L\in\mathsf{VA}(M)$, one can
construct an $L^{\prime}\in\mathsf{Prio}$ with
$\Psi\left(L^{\prime}\right)=\Psi\left(L\right)$.

###### Proof.

We proceed by induction with respect to the definition of $\mathsf{DEC}$. In
the case $M=\mathbb{B}^{n}$, we have $\mathsf{VA}(M)\subseteq\mathsf{Prio}$,
because priority multicounter machines generalize partially blind multicounter
machines.

Suppose $M=N\times\mathbb{Z}$ and
$\Psi\left(\mathsf{VA}(N)\right)\subseteq\Psi\left(\mathsf{Prio}\right)$ and
let $L\in\mathsf{VA}(M)$. By Section 5, we have $L=h(K\cap\Psi^{-1}(S))$ for
some semilinear set $S$, a morphism $h$, and $K\in\mathsf{VA}(N)$. Hence,
there is a $\bar{K}\in\mathsf{Prio}$ with
$\Psi\left(\bar{K}\right)=\Psi\left(K\right)$. With this, we have
$\Psi\left(L\right)=\Psi\left(h(\bar{K}\cap\Psi^{-1}(S))\right)$ and since
$\mathsf{Prio}$ is Presburger closed, we have
$h(\bar{K}\cap\Psi^{-1}(S))\in\mathsf{Prio}$ and thus
$\Psi\left(L\right)\in\Psi\left(\mathsf{Prio}\right)$.

Suppose $M=M_{0}*M_{1}$ and
$\Psi\left(\mathsf{VA}(M_{i})\right)\subseteq\Psi\left(\mathsf{Prio}\right)$
for $i\in\\{0,1\\}$. Let $L$ be a member of $\mathsf{VA}(M)$. According to
Section 5, this means $L$ belongs to
$\mathsf{Alg}(\mathsf{VA}(M_{0})\cup\mathsf{VA}(M_{1}))$. Since
$\Psi\left(\mathsf{VA}(M_{0})\cup\mathsf{VA}(M_{1})\right)\subseteq\Psi\left(\mathsf{Prio}\right)$,
we can construct a $\mathsf{Prio}$-grammar $G$ with
$\Psi\left(\mathsf{L}(G)\right)=\Psi\left(L\right)$. By Theorem 5.2 and
Section 5, this implies
$\Psi\left(L\right)\in\Psi\left(\mathsf{Prio}\right)$.∎

The following Section is a direct consequence of Section 5 and Theorem 5.3:
Given a valence automaton over $M$ with $M\in\mathsf{DEC}$, we construct a
priority multicounter machine accepting a Parikh-equivalent language. The
latter can then be checked for emptiness.

######  Lemma .

For each $M\in\mathsf{DEC}$, the emptiness problem for valence automata over
$M$ is decidable.

This completes the proof of “4 $\Rightarrow$ 1” of Theorem 3.2 and hence
concludes the proof of Theorem 3.2.

##  6\. Expressive equivalences

We now turn to the proof of Sections 3 and 3, which characterize the
expressiveness of valence automata over $\mathsf{SC}^{\pm}$ and
$\mathsf{REM}$, respectively.

######  Section 3.

Since $\mathsf{SC}^{\pm}\subseteq\mathsf{DEC}$, the inclusion “$\supseteq$” is
immediate. We show by induction with respect to the definition of
$\mathsf{DEC}$ that for each $M\in\mathsf{DEC}$, there is an
$M^{\prime}\in\mathsf{SC}^{\pm}$ with
$\mathsf{VA}(M)\subseteq\mathsf{VA}(M^{\prime})$. This is trivial if
$M=\mathbb{B}^{n}$, so suppose
$\mathsf{VA}(M)\subseteq\mathsf{VA}(M^{\prime})$ and
$\mathsf{VA}(N)\subseteq\mathsf{VA}(N^{\prime})$ for $M,N\in\mathsf{DEC}$ and
$M^{\prime},N^{\prime}\in\mathsf{SC}^{\pm}$. Observe that by induction on the
definition of $\mathsf{SC}^{\pm}$, one can show that there is a common
$P\in\mathsf{SC}^{\pm}$ with $\mathsf{VA}(M^{\prime})\subseteq\mathsf{VA}(P)$
and $\mathsf{VA}(N^{\prime})\subseteq\mathsf{VA}(P)$. Of course, we may assume
that $R_{1}(P)\neq\\{1\\}$. Then we have

$\displaystyle\mathsf{VA}(M*N)$
$\displaystyle\subseteq\mathsf{Alg}(\mathsf{VA}(M)\cup\mathsf{VA}(N))\subseteq\mathsf{Alg}(\mathsf{VA}(M^{\prime})\cup\mathsf{VA}(N^{\prime}))$
$\displaystyle\subseteq\mathsf{Alg}(\mathsf{VA}(P))=\mathsf{VA}(\mathbb{B}*P),$

in which the first inclusion is due to Section 5 and the equality in the end
is provided by Section 5. Since $\mathbb{B}*P\in\mathsf{SC}^{\pm}$, this
completes the proof for $M*N$. Moreover,
$\mathsf{VA}(M)\subseteq\mathsf{VA}(M^{\prime})$ implies
$\mathsf{VA}(M\times\mathbb{Z})\subseteq\mathsf{VA}(M^{\prime}\times\mathbb{Z})$
and we have $M^{\prime}\times\mathbb{Z}\in\mathsf{SC}^{\pm}$.∎

######  Section 3.

By induction, it is easy to see that each $M\in\mathsf{SC^{+}}$ is isomorphic
to some $\mathbb{M}\Gamma$ where $\Gamma$ contains a PPN-graph and
$\Gamma^{-}$ is a transitive forest. By Theorem 5.1, this means $\Gamma^{-}$
contains neither $\mathsf{C4}{}$ nor $\mathsf{P4}{}$. This proves the
inclusion “$\supseteq$”.

Because of Theorem 5.1, for the inclusion “$\subseteq$”, it suffices to show
that if $\Gamma^{-}$ is a transitive forest, then there is some
$M\in\mathsf{SC^{+}}$ with
$\mathsf{VA}(\mathbb{M}\Gamma)\subseteq\mathsf{VA}(M)$. We prove this by
induction on the number of vertices in $\Gamma=(V,E)$. As in the proof of
Section 5, we may assume that for every induced proper subgraph $\Delta$ of
$\Gamma$, we find an $M\in\mathsf{SC^{+}}$ with
$\mathsf{VA}(\mathbb{M}\Gamma)\subseteq\mathsf{VA}(M)$. If $\Gamma$ is empty,
then $\mathbb{M}\Gamma\cong\mathbf{1}$ and
$\mathsf{VA}(\mathbb{M}\Gamma)\subseteq\mathsf{VA}(\mathbb{B}^{(2)}\times\mathbb{B})$.
Hence, we may assume that $\Gamma$ is non-empty.

If $\Gamma$ is not connected, then $\Gamma=\Gamma_{1}\uplus\Gamma_{2}$ with
non-empty graphs $\Gamma_{1},\Gamma_{2}$. This implies that there are
$M_{1},M_{2}\in\mathsf{SC^{+}}$ with
$\mathsf{VA}(\mathbb{M}\Gamma_{i})\subseteq\mathsf{VA}(M_{i})$ for
$i\in\\{1,2\\}$. By induction with respect to the definition of
$\mathsf{SC^{+}}$, one can show that there is a common $N\in\mathsf{SC^{+}}$
with $\mathsf{VA}(M_{i})\subseteq\mathsf{VA}(N)$ for $i\in\\{1,2\\}$. Here,
$N$ can clearly be chosen with $R_{1}(N)\neq\\{1\\}$. Then, we have

$\displaystyle\mathsf{VA}(\mathbb{M}\Gamma)$
$\displaystyle=\mathsf{VA}(\mathbb{M}\Gamma_{1}*\mathbb{M}\Gamma_{2})\subseteq\mathsf{Alg}(\mathsf{VA}(\mathbb{M}\Gamma_{1})\cup\mathsf{VA}(\mathbb{M}\Gamma_{2}))$
$\displaystyle\subseteq\mathsf{Alg}(\mathsf{VA}(M_{1})\cup\mathsf{VA}(M_{2}))\subseteq\mathsf{Alg}(\mathsf{VA}(N))=\mathsf{VA}(\mathbb{B}*N)$

and $\mathbb{B}*N\in\mathsf{SC^{+}}$ as in the proof of Section 3.

Suppose $\Gamma$ is connected. Since $\Gamma^{-}$ is a transitive forest,
there is a vertex $v\in V$ that is adjacent to every vertex in
$V\setminus\\{v\\}$. By induction, there is an $M\in\mathsf{SC^{+}}$ with
$\mathsf{VA}(\mathbb{M}(\Gamma\setminus v))\subseteq\mathsf{VA}(M)$. Depending
on whether $v$ is looped or not, we have
$\mathbb{M}\Gamma\cong\mathbb{M}(\Gamma\setminus v)\times\mathbb{Z}$ or
$\mathbb{M}\Gamma\cong\mathbb{M}(\Gamma\setminus v)\times\mathbb{B}$. Since
$\mathsf{VA}(\mathbb{Z})\subseteq\mathsf{VA}(\mathbb{B}\times\mathbb{B})$ (one
blind counter can easily be simulated by two partially blind counters), this
yields
$\mathsf{VA}(\mathbb{M}\Gamma)\subseteq\mathsf{VA}(\mathbb{M}(\Gamma\setminus
v)\times\mathbb{B}\times\mathbb{B})\subseteq\mathsf{VA}(M\times\mathbb{B}\times\mathbb{B})$
and the fact that $M\times\mathbb{B}\times\mathbb{B}\in\mathsf{SC^{+}}$
completes the proof.∎

##  7\. Finite-index languages and Petri nets

We have seen in the previous sections that valence automata over
$\mathsf{SC}^{\pm}$ constitute a model that (strictly) subsumes Petri nets and
has a decidable emptiness problem. Moreover, they feature a type of pushdown
stack. A similar result has been obtained by Atig and Ganty [2]. They proved
that given a finite-index context-free language and a Petri net language, it
is decidable whether their intersection is empty. Here, we present a common
generalization of these facts: We provide a language class that contains the
languages considered by Atig and Ganty and those in
$\mathsf{VA}(\mathsf{SC}^{\pm})$ and enjoys decidability of the emptiness
problem.

### Definitions

If $\mathcal{C}$ is the class of finite languages, a $\mathcal{C}$-grammar is
also called a _context-free grammar_. For a context-free grammar
$G=(N,T,P,S)$, we may assume that for each production $(A,M)$, the set $M$ is
a singleton and instead of $(A,\\{w\\})$, we write $A\to w$ for the
production. The grammar is said to be in _Chomsky normal form (CNF)_ if for
every production $A\to w$, we have $w\in N^{2}\cup T\cup\\{\varepsilon\\}$.

The finite-index restriction considered by Atig and Ganty places a budget
constraint on the nonterminal occurrences in sentential forms. This leads to a
restricted derivation relation. Suppose $G$ is in CNF. For $u,v\in(N\cup
T)^{*}$, we write $u\Rightarrow_{G,k}v$ if $|u|_{N},|v|_{N}\leq k$ and
$u\Rightarrow_{G}v$. Then, the _$k$ -approximation_ $\mathsf{L}_{k}(G)$ of
$\mathsf{L}(G)$ is defined as

$\mathsf{L}_{k}(G)=\\{w\in T^{*}\mid S\Rightarrow^{*}_{G,k}w\\}.$

For $k\geq 1$, we use $\mathsf{CF}_{k}$ to denote the class of languages of
the form $\mathsf{L}_{k}(G)$ for context-free grammars $G$. The languages in
$\mathsf{CF}_{k}$ are called _index- $k$ context-free languages_. It will
later be convenient to let $\mathsf{CF}_{0}$ denote the regular languages.
Moreover, $\mathsf{fiCF}$ is the union $\bigcup_{k\geq 1}\mathsf{CF}_{k}$. Its
members are called _finite-index context-free languages_. Note that although
clearly $\mathsf{L}(G)=\bigcup_{k\geq 1}\mathsf{L}_{k}(G)$ for every
individual grammar $G$, the class $\mathsf{fiCF}$ is strictly contained in
$\mathsf{CF}$: Salomaa has shown that $D_{1}^{*}$, the semi-Dyck language over
one pair of parentheses, is not contained in $\mathsf{fiCF}$ [16].

A _$d$ -dimensional (labeled) Petri net333This definition is closer to what is
known as a Vector Addition System, but these models are well-known to be
equivalent with respect to generated languages._ is a tuple
$N=(X,E,\mu_{0},F)$, where $X$ is an alphabet, $T$ is a finite subset of
$(X\cup\\{\varepsilon\\})\times\mathbb{Z}^{d}$ whose elements are called
_transitions_ , $\mu_{0}\in\mathbb{N}^{d}$ is the _initial marking_ , and
$F\subseteq\mathbb{N}^{d}$ is a finite set of _final markings_. For
$\mu,\mu^{\prime}\in\mathbb{N}^{d}$ and $w\in X^{*}$, we write
$\mu\xrightarrow{w}_{N}\mu^{\prime}$ if there are
$\mu_{0},\ldots,\mu_{n}\in\mathbb{N}^{d}$ and transitions
$(x_{1},\nu_{1}),\ldots,(x_{n},\nu_{n})\in T$ such that $w=x_{1}\cdots x_{n}$,
$\mu_{0}=\mu$, $\mu_{n}=\mu^{\prime}$, and $\mu_{i}=\mu_{i-1}+\nu_{i}$ for
$i\in\\{1,\ldots,n\\}$. Moreover, we define

$\displaystyle\mathsf{L}(N,\mu,\mu^{\prime})=\\{w\in
X^{*}\mid\mu\xrightarrow{w}_{N}\mu^{\prime}\\},$
$\displaystyle\mathsf{L}(N)=\bigcup_{\mu\in F}\mathsf{L}(N,\mu_{0},\mu).$

The language $\mathsf{L}(N)$ is said to be _generated by $N$_. A languages is
a _Petri net language_ if it is generated by some labeled Petri net. By
$\mathsf{P}$, we denote the class of all Petri net languages. Observe that we
have $\mathsf{P}=\bigcup_{n\geq 0}\mathsf{VA}(\mathbb{B}^{n})$.

The main result of this section involves the language class
$\mathsf{fiCF}\sqcap\mathsf{P}$. We will use the fact that this is a full
trio, which follows from the following classical result. See [7, Theorem
3.6.1] for a proof.

######  Proposition .

If $\mathcal{C}$ and $\mathcal{D}$ are full trios, then
$\mathcal{C}\sqcap\mathcal{D}$ is a full trio as well.

In our notation, the result of Atig and Ganty can be stated as follows.

######  Theorem 7.1 (Atig and Ganty [2]).

The class $\mathsf{fiCF}\sqcap\mathsf{P}$ has a decidable emptiness problem.

Here, we present a language class including both
$\mathsf{fiCF}\sqcap\mathsf{P}$ and $\mathsf{VA}(\mathsf{SC}^{\pm})$ where
emptiness is still decidable. First, consider the following hierarchy. Let

$\displaystyle\mathsf{F}_{0}=\mathsf{P},$
$\displaystyle\text{$\mathsf{F}_{i+1}=\mathsf{SLI}(\mathsf{Alg}(\mathsf{F}_{i}))$
for $i\geq 0$},$ $\displaystyle\mathsf{F}=\bigcup_{i\geq 0}\mathsf{F}_{i}.$

The class $\mathsf{F}$ captures the expressive power of valence automata over
monoids in $\mathsf{SC}^{\pm}$:

######  Proposition .

$\mathsf{VA}(\mathsf{SC}^{\pm})=\mathsf{F}$.

###### Proof.

For the inclusion “$\subseteq$”, we prove that for every
$M\in\mathsf{SC}^{\pm}$, we have $\mathsf{VA}(M)\subseteq\mathsf{F}_{i}$ for
some $i\geq 0$. Clearly, we have
$\mathsf{VA}(\mathbb{B}^{n})\subseteq\mathsf{F}_{0}$. Moreover, if
$\mathsf{VA}(M)\subseteq\mathsf{F}_{i}$, then

$\mathsf{VA}(M\times\mathbb{Z})\subseteq\mathsf{SLI}(\mathsf{VA}(M))\subseteq\mathsf{SLI}(\mathsf{F}_{i})\subseteq\mathsf{F}_{i+1},$

in which the first inclusion follows from Section 5. Finally, if
$\mathsf{VA}(M_{0})\subseteq\mathsf{F}_{i}$ and
$\mathsf{VA}(M_{1})\subseteq\mathsf{F}_{j}$, then
$\mathsf{VA}(M_{0}),\mathsf{VA}(M_{1})\subseteq\mathsf{F}_{k}$ for
$k=\max\\{i,j\\}$ and thus

$\mathsf{VA}(M_{0}*M_{1})\subseteq\mathsf{Alg}(\mathsf{VA}(M_{0})\cup\mathsf{VA}(M_{1}))\subseteq\mathsf{Alg}(\mathsf{F}_{k})\subseteq\mathsf{F}_{k+1},$

where the first inclusion is due to Section 5. This completes the proof of the
inclusion “$\subseteq$”.

For the inclusion “$\supseteq$”, we show by induction on $i$ that
$\mathsf{F}_{i}\subseteq\mathsf{VA}(\mathsf{DEC})$ for every $i\geq 0$. Since
$\mathsf{VA}(\mathsf{DEC})=\mathsf{VA}(\mathsf{SC}^{\pm})$ by Section 3, this
is sufficient. Clearly, the inclusion $\mathsf{F}_{0}=\bigcup_{n\geq
0}\mathsf{VA}(\mathbb{B}^{n})\subseteq\mathsf{VA}(\mathsf{DEC})$ holds. Now
suppose $\mathsf{F}_{i}\subseteq\mathsf{VA}(\mathsf{DEC})$ and let $L$ be a
member of $\mathsf{F}_{i+1}=\mathsf{SLI}(\mathsf{Alg}(\mathsf{F}_{i}))$. This
means we have $L=h(K\cap\Psi^{-1}(S))$ for some homomorphism $h$, a language
$K$ from $\mathsf{Alg}(\mathsf{F}_{i})$, and a semilinear set $S$. As a member
of $\mathsf{Alg}(\mathsf{F}_{i})$, the language $K$ is generated by an
$\mathsf{F}_{i}$-grammar $G$. Each right-hand side in $G$ is contained in
$\mathsf{F}_{i}$ and thus, by induction, in $\mathsf{VA}(\mathsf{DEC})$.
Hence, suppose the right-hand sides of $G$ are $K_{1},\ldots,K_{n}$ with
$K_{i}\in\mathsf{VA}(M_{i})$ for $M_{1},\ldots,M_{n}\in\mathsf{DEC}$. Consider
the monoid $M=M_{1}*\cdots*M_{n}$. Since each $M_{i}$ embeds into $M$, the
languages $K_{1},\ldots,K_{n}$ belong to $\mathsf{VA}(M)$. Thus, $K$ is a
member of $\mathsf{Alg}(\mathsf{VA}(M))$, which equals
$\mathsf{VA}(\mathbb{B}*\mathbb{B}*M)$ according to Section 5. According to
Section 5, this implies that $L$ belongs to
$\mathsf{VA}((\mathbb{B}*\mathbb{B}*M)\times\mathbb{Z}^{k})$ for some $k\geq
0$. Since $(\mathbb{B}*\mathbb{B}*M)\times\mathbb{Z}^{k}$ is a member of
$\mathsf{DEC}$, we know that $L$ belongs to $\mathsf{VA}(\mathsf{DEC})$. We
have thus shown $\mathsf{F}_{i+1}\subseteq\mathsf{VA}(\mathsf{DEC})$, which
establishes the inclusion “$\subseteq$”. ∎

Our new class is defined as follows. Let

$\displaystyle\mathsf{G}_{0}=\mathsf{fiCF}\sqcap\mathsf{P},$
$\displaystyle\text{$\mathsf{G}_{i+1}=\mathsf{SLI}(\mathsf{Alg}(\mathsf{G}_{i}))$~{}for
$i\geq 0$},$ $\displaystyle\mathsf{G}=\bigcup_{i\geq 0}\mathsf{G}_{i}.$

Then clearly $\mathsf{F}_{i}\subseteq\mathsf{G}_{i}$ for $i\geq 0$ and hence
$\mathsf{VA}(\mathsf{SC}^{\pm})=\mathsf{F}\subseteq\mathsf{G}$. Moreover, we
obviously have $\mathsf{fiCF}\sqcap\mathsf{P}\subseteq\mathsf{G}$. We shall
prove the following.

######  Theorem 7.2.

The class $\mathsf{G}$ has a decidable emptiness problem.

We show Theorem 7.2 by proving a slightly stronger version of Theorem 7.1:
Atig and Ganty reduce the emptiness problem of $\mathsf{fiCF}\sqcap\mathsf{P}$
to the emptiness problem for priority multicounter machines. We strengthen
this slightly and show that for each language $L$ in
$\mathsf{fiCF}\sqcap\mathsf{P}$, one can construct a priority multicounter
machine $\mathcal{A}$ with
$\Psi\left(\mathsf{L}(\mathcal{A})\right)=\Psi\left(L\right)$, in other words:
$\Psi\left(\mathsf{fiCF}\sqcap\mathsf{P}\right)\subseteq\Psi\left(\mathsf{Prio}\right)$.
This allows us to apply Theorem 5.2 and Section 5 to conclude that
$\Psi\left(\mathsf{G}\right)\subseteq\Psi\left(\mathsf{Prio}\right)$.

The following observation provides a decomposition of languages in
$\mathsf{fiCF}$. A context-free grammar $G=(N,T,P,S)$ is called _linear_ if
every production $A\to w$ in $G$ satisfies $|w|_{N}\leq 1$. A language is
called _linear context-free_ if it is generated by a linear context-free
grammar. Note that $\mathsf{CF}_{1}$ is precisely the class of linear context-
free languages.

######  Proposition .

Suppose $k\geq 1$. A language belongs to $\mathsf{CF}_{k}$ if and only if it
can be written as $\sigma(L)$ for a linear context-free language $L$ and a
$\mathsf{CF}_{k-1}$-substitution $\sigma$.

###### Proof.

We prove the statement by induction on $k$. For $k=1$, it essentially states
that linear context-free languages are closed under regular substitutions,
which is clearly true. For the induction step, we use a result of Atig and
Ganty. Let $G=(N,T,P,S)$ be a context-free grammar in CNF. For each $i\geq 0$,
let $A^{[i]}$ be a fresh symbol. For each $\ell\geq 0$, we define a grammar
$G^{[\ell]}$ as follows. We have
$G^{[\ell]}=(N^{[\ell]},T,P^{[\ell]},S^{[\ell]})$ with
$N^{[\ell]}=\\{A^{[i]}\mid A\in N,~{}0\leq i\leq\ell\\}$ and $P^{[\ell]}$ is
the smallest set of productions such that

  1. (1)

for each $A\to BC$ in $P$, we have $A^{[i]}\to B^{[i]}C^{[i-1]}$ and
$A^{[i]}\to B^{[i-1]}C^{[i]}$ in $P^{[\ell]}$ for every index
$i\in\\{1,\ldots,\ell\\}$,

  2. (2)

for each $A\to w$ in $P$ with $w\in T\cup\\{\varepsilon\\}$, we have
$A^{[i]}\to w$ in $P^{[\ell]}$ for every $i\in\\{0,\ldots,\ell\\}$.

For each nonterminal $A$ of $G$, we define

$\displaystyle\mathsf{L}(G,A)=\\{w\in T^{*}\mid A\Rightarrow^{*}_{G}w\\},$
$\displaystyle\mathsf{L}_{\ell}(G,A)=\\{w\in T^{*}\mid
A\Rightarrow^{*}_{G,\ell}w\\}.$

Atig and Ganty [2] show that for every $i\in\\{0,\ldots,\ell\\}$, one has

(5) $\mathsf{L}(G^{[\ell]},A^{[i]})=\mathsf{L}_{i+1}(G,A).$

Now suppose $K$ belongs to $\mathsf{CF}_{k+1}$ with $K=\mathsf{L}_{k+1}(G)$
where $G$ is in CNF. According to (5), we have $\mathsf{L}(G^{[k]})=K$. We now
construct a (linear) context-free grammar
$G^{\prime}=(N^{\prime},T^{\prime},P^{\prime},S^{\prime})$ (that is not
necessarily in CNF) as follows. It has terminal symbols
$T^{\prime}=T\cup\\{A^{[i]}\mid 0\leq i\leq k-1\\}$ and its nonterminal
symbols are $N^{\prime}=\\{A^{[k]}\mid A\in N\\}$. As productions, it contains
all those productions of $G$ whose left-hand side belongs to $N^{\prime}$.
Moreover, the substitution $\sigma\colon T^{\prime*}\to\mathcal{P}({T^{*}})$
is defined as follows: For $a\in T$, we set $\sigma(a)=\\{a\\}$. For
$A^{[i]}\in T^{\prime}$, we define
$\sigma(A^{[i]})=\mathsf{L}(G^{[k]},A^{[i]})$. Since for $A^{[i]}\in
T^{\prime}$, we have $i\leq k-1$, the equation (5) tells us that
$\sigma(A^{[i]})$ belongs to $\mathsf{CF}_{i+1}\subseteq\mathsf{CF}_{k}$.
Hence, $\sigma$ is a $\mathsf{CF}_{k}$-substitution. Moreover, an inspection
of the definition of $G^{[\ell]}$ yields that $G^{\prime}$ is clearly linear.
Finally, we have $K=\sigma(\mathsf{L}(G^{\prime}))$, so that with
$L=\mathsf{L}(G^{\prime})$, we have proven the “only if” direction of the
Section. The other direction is obvious.∎

We now turn to the key lemma (Section 7) of our slightly stronger version of
Atig and Ganty’s result. We want to show that given an index-$k$ context-free
language $K$ and a Petri net language $L$, one can construct a priority
multicounter machine $\mathcal{A}$ with
$\Psi\left(\mathsf{L}(\mathcal{A})\right)=\Psi\left(K\cap L\right)$. The proof
proceeds by induction on the index $k$, which warrants a strengthening of the
statement.

We need some terminology. For a vector
$\mu=(m_{1},\ldots,m_{d})\in\mathbb{N}^{d}$ and $k\geq d$, we denote by
$0|\mu$ the vector $(0,\ldots,0,m_{1},\ldots,m_{d})\in\mathbb{N}^{k}$. The
dimension $k$ will always be clear from the context. In order to make the
induction work, we need to construct priority counter machines with the
additional property that for a particular $d$, they never zero-test their $d$
topmost counters. Therefore, for a priority $k$-counter machine
$\mathcal{A}=(Q,X,E,q_{0},F)$ and $d\leq k$, we define $\mathcal{A}_{d}$ to be
the machine obtained from $\mathcal{A}$ removing all transitions
$(q,x,\ell,\nu,q^{\prime})$ with $\ell>d$. In other words, we remove all
transitions that perform a zero-test on a counter other than $1,\ldots,d$. We
define the language

$\mathsf{L}_{d}(\mathcal{A},q,\mu,q^{\prime},\mu^{\prime})=\\{w\in
X^{*}\mid(q,0|\mu)\xrightarrow{w}_{\mathcal{A}_{d}}(q^{\prime},0|\mu^{\prime})\\}.$

For a language $K\subseteq X^{*}$ and a $d$-dimensional Petri net
$N=(X,E,\mu_{0},F)$, we say that a priority $k$-counter machine $\mathcal{A}$
is a _$(K,N)$ -simulator_ if $k\geq d$ and there are two states $p$ and
$p^{\prime}$ in $\mathcal{A}$ such that for every
$\mu,\mu^{\prime}\in\mathbb{N}^{d}$, we have

(6)
$\Psi\left(\mathsf{L}_{d}(\mathcal{A},p,\mu,p^{\prime},\mu^{\prime})\right)=\Psi\left(K\cap\mathsf{L}(N,\mu,\mu^{\prime})\right).$

In this case, $p$ and $p^{\prime}$ are called _source_ and _target_ ,
respectively.

######  Lemma .

Given a language $K$ in $\mathsf{fiCF}$ and a labeled Petri net $N$, one can
construct a $(K,N)$-simulator.

###### Proof.

Let $N=(X,E,\mu_{0},F)$ be a $d$-dimensional Petri net and let $K$ belong to
$\mathsf{CF}_{k}$. We proceed by induction on $k$. If $k=0$, then $K$ is
accepted by some finite automaton $\mathcal{B}$. We may assume that
$\mathcal{B}$ has an initial state $p$ and one final state $p^{\prime}$. One
can construct a priority $d$-counter machine $\mathcal{A}$ by a product
construction from $N$ and $\mathcal{B}$ such that $\mathcal{A}$ has the same
state set as $\mathcal{B}$ and

$\mathsf{L}_{d}(\mathcal{A},p,\mu,p^{\prime},\mu^{\prime})=K\cap\mathsf{L}(N,\mu,\mu^{\prime}),$

meaning it is indeed a $(K,N)$-simulator.

For the induction step, suppose $k\geq 1$. According to Section 7, there is a
linear context-free language $L\subseteq Y^{*}$ and a
$\mathsf{CF}_{k-1}$-substitution $\sigma\colon Y\to\mathcal{P}({X^{*}})$ with
$K=\sigma(L)$. Let us begin with some explanation. Since $L$ is linear
context-free, it is given by a grammar $G=(\bar{N},Y,P,S)$ where every
production is of the form $A\to x_{1}Bx_{2}$ or $A\to\varepsilon$ with
$A,B\in\bar{N}$ and $x_{1},x_{2}\in Y\cup\\{\varepsilon\\}$. Let $D\subseteq
P^{*}$ be the regular language of production sequences that correspond to
derivations in $G$ and let $g_{1},g_{2}\colon P^{*}\to Y^{*}$ be the morphisms
where for $\pi=A\to x_{1}Bx_{2}$ (with $x_{1},x_{2}\in
Y\cup\\{\varepsilon\\}$), we set $g_{i}(\pi)=x_{i}$. Then, we have
$L=\\{g_{1}(w)g_{2}({w}^{R})\mid w\in D\\}$.

Therefore, if $\tau_{i}$ is the $\mathsf{CF}_{k-1}$-substitution with
$\tau_{i}(\pi)=\sigma(g_{i}(\pi))$ for $i=1,2$, then $K=\sigma(L)$ consists of
all words in $\tau_{1}(w)\tau_{2}({w}^{R})$ for $w\in D$. In other words, $K$
contains precisely those words of the form

(7) $u_{1}\cdots u_{n}v_{n}\cdots v_{1}$

such that there is a word $w=\pi_{1}\cdots\pi_{n}\in D$,
$\pi_{1},\ldots,\pi_{n}\in P$ with $u_{i}\in\tau_{1}(\pi_{i})$ and
$v_{i}\in\tau_{2}(\pi_{i})$ for $i\in\\{1,\ldots,n\\}$.

Our task is to construct a $(K,N)$-simulator $\mathcal{A}^{\prime}$. This
means, using a priority counter machine, we have to simulate—up to Parikh
image—all runs of $N$ with labels as in Eq. 7. By induction, we have a
$(\tau_{i}(\pi),N)$-simulator $\mathcal{A}_{\pi,i}$ for each $\pi\in P$ and
$i\in\\{1,2\\}$. Each of the machines $\mathcal{A}_{\pi,i}$ has $\geq d$
counters, so we may clearly assume that for some $\ell\geq 0$, they all have
$\ell+d$ counters. Moreover, by definition of a $(\tau_{i}(\pi),N)$-simulator,
these machines never perform a zero-test on the $d$ top-most counters.
Moreover, using a zero-test, we can guarantee that when $\mathcal{A}_{\pi,i}$
reaches its target state, its first $\ell$ counters are zero.

The basic idea is that $\mathcal{A}^{\prime}$ performs a run of an automaton
for $D$, which reads a word $w=\pi_{1}\cdots\pi_{n}$. For each $j=1,\ldots,n$,
it executes a computation of $\mathcal{A}_{\pi_{j},1}$ (reading $u_{j}$) and a
computation of $\mathcal{A}_{\pi_{j},2}$ (reading $v_{j}$). Hence,
$\mathcal{A}^{\prime}$ reads the word $u_{1}v_{1}u_{2}v_{2}\cdots u_{n}v_{n}$,
which is clearly Parikh-equivalent to $u_{1}\cdots u_{n}v_{n}\cdots v_{1}$.

We have to make sure that all these runs of the machines
$\mathcal{A}_{\pi_{j},i}$ are compatible in the sense that they can be
executed in the order prescribed by Eq. 7. To this end, all the executions of
$\mathcal{A}_{\pi_{1},1},\ldots,\mathcal{A}_{\pi_{n},1}$ share one set of
$\ell+d$ counters. The executions of
$\mathcal{A}_{\pi_{1},2},\ldots,\mathcal{A}_{\pi_{n},2}$ also share a set of
counters, but they are executed backwards. The counters for the backward
execution are also $\ell+d$ many, but since each execution of some
$\mathcal{A}_{\pi,i}$ leaves the first $\ell$ counters empty, the forward and
the backward simulation can share the first $\ell$ counters between them. This
leaves us with $\ell+2d$ counters: We use counters $1,\ldots,\ell+d$ to
simulate $\mathcal{A}_{\pi_{j},1}$ and we use counters $1,\ldots,\ell$ and
$\ell+d+1,\ldots,\ell+2d$ to simulate $\mathcal{A}_{\pi_{j},2}$ (backwards).
Therefore, we call counters $1,\ldots,\ell$ _auxiliary counters_ , whereas the
counters $\ell+1,\ldots,\ell+d$ are called _forward counters_. The counters
$\ell+d+1,\ldots,\ell+2d$ are dubbed _backward counters_.

In addition, we have to make sure that the executions of $N$ corresponding to
$v_{n}\cdots v_{1}$ can be executed after the executions corresponding to
$u_{1}\cdots u_{n}$. Therefore, after executing the run of the automaton for
$D$, $\mathcal{A}^{\prime}$ simultaneously counts down the forward and the
backward counters and then performs a zero-test on the counters
$1,\ldots,\ell+2d$.

Finally, in order to be a $(K,N)$-simulator, $\mathcal{A}^{\prime}$ must have
$d$ top-most counters so that the following holds: If we simulate the
computation $\mu\xrightarrow{u_{1}\cdots u_{n}v_{n}\cdots
v_{1}}_{N}\mu^{\prime}$ with $\mu,\mu^{\prime}\in\mathbb{N}^{d}$, then the $d$
top-most counters of $\mathcal{A}^{\prime}$ must contain $\mu$ in the
beginning and $\mu^{\prime}$ in the end. To this end, we add an additional set
of $d$ counters, called _global counters_. Hence, in total,
$\mathcal{A}^{\prime}$ has $\ell+3d$ counters:

$\underbrace{1,\ldots,\ell}_{\textrm{auxiliary}},~{}\underbrace{\ell+1,\ldots,\ell+d}_{\textrm{forward}},~{}\underbrace{\ell+d+1,\ldots,\ell+2d}_{\textrm{backward}},~{}\underbrace{\ell+2d+1,\ldots,\ell+3d}_{\textrm{global
}}.$

The global counters are used as follows. The machine $\mathcal{A}^{\prime}$
starts with counters $0|\mu\in\mathbb{N}^{\ell+3d}$. First, it
nondeterministically subtracts some vector $\nu_{1}\in\mathbb{N}^{d}$ from the
global counters and simultaneously adds it to the forward counters. Then, it
nondeterministically adds a vector $\nu_{2}^{\prime}\in\mathbb{N}^{d}$ to both
the global counters and the backward counters. After performing the simulation
of the $\mathcal{A}_{\pi_{1},1},\ldots,\mathcal{A}_{\pi_{n},1}$ and the
$\mathcal{A}_{\pi_{1},2},\ldots,\mathcal{A}_{\pi_{n},2}$, suppose the forward
counters contain $\nu_{1}^{\prime}\in\mathbb{N}^{d}$ and the backward counters
contain $\nu_{2}\in\mathbb{N}^{d}$. As described above, $\mathcal{A}^{\prime}$
afterwards compares the forward and backward counters, ensuring that
$\nu_{1}^{\prime}=\nu_{2}$ and thus:

$\nu_{1}\xrightarrow{u_{1}\cdots
u_{n}}_{N}\nu_{1}^{\prime}=\nu_{2}\xrightarrow{v_{n}\cdots
v_{1}}_{N}\nu^{\prime}_{2}.$

Observe that this guarantees that the global counters of
$\mathcal{A}^{\prime}$ reflect the counters of the simulated computation of
$N$: In the end, they are precisely $0|\mu^{\prime}\in\mathbb{N}^{\ell+3d}$,
where $\mu^{\prime}=\mu-\nu_{1}+\nu^{\prime}_{2}$, which means
$\mu\xrightarrow{u_{1}\cdots u_{n}v_{n}\cdots v_{1}}_{N}\mu^{\prime}$.

Let us make the description of $\mathcal{A}^{\prime}$ more precise.

  1. (i)

$\mathcal{A}^{\prime}$ has a state $p$, where it nondeterministically
subtracts tokens from the global counters and simultaneously adds them to the
forward counters.

  2. (ii)

Note that $D\subseteq P^{*}$ can be accepted by a finite automaton with state
set $\bar{N}$, the non-terminals of $G$. Therefore, from the state $p$,
$\mathcal{A}^{\prime}$ can enter the state $S\in\bar{N}$ to start simulating
the automaton for $D$.

  3. (iii)

In a state $A\in\bar{N}$, $\mathcal{A}^{\prime}$ selects a production
$\pi=A\to x_{1}Bx_{2}\in P$ and then executes a computation of
$\mathcal{A}_{\pi,1}$ in the auxiliary and the forward counters. Then, it
executes a computation of $\mathcal{A}_{\pi,2}$ backwards on the auxiliary and
backward counters. Then, it switches to state $B\in\bar{N}$.

  4. (iv)

If $\mathcal{A}^{\prime}$ is in state $A\in\bar{N}$ and there is a production
$A\to\varepsilon\in P$, then $\mathcal{A}^{\prime}$ switches to a state
$p^{\prime\prime}$, in which it simultaneously counts down the forward and the
backward counters. From $p^{\prime\prime}$ it non-deterministically switches
to $p^{\prime}$ while performing a zero-test on all counters
$1,\ldots,\ell+2d$.

In conclusion, it is clear that for $\mu,\mu^{\prime}\in\mathbb{N}^{d}$, we
have
$(p,0|\mu)\xrightarrow{w}_{\mathcal{A}^{\prime}}(p^{\prime},0|\mu^{\prime})$
if and only if $w=u_{1}v_{1}u_{2}v_{2}\cdots u_{n}v_{n}$ such that there is a
word $\pi_{1}\cdots\pi_{n}\in D$, $\pi_{1},\ldots,\pi_{n}\in P$, such that
$u_{j}\in\tau_{1}(\pi_{j})$ and $v_{j}\in\tau_{2}(\pi_{j})$. Thus,
$\mathcal{A}^{\prime}$ is a $(K,N)$-simulator.

∎

We are now ready to prove the slightly stronger version of the decidability
result of Atig and Ganty.

######  Theorem 7.3.

Given $K$ in $\mathsf{fiCF}\sqcap\mathsf{P}$, one can construct a priority
multicounter machine $\mathcal{A}$ with
$\Psi\left(\mathsf{L}(\mathcal{A})\right)=\Psi\left(K\right)$.

###### Proof.

Since the languages of priority multicounter machines are closed under
morphisms, we may assume that $K=C\cap P$, where $C$ is in $\mathsf{CF}_{k}$
and $P=\mathsf{L}(N)$ for a $d$-dimensional labeled Petri net
$N=(X,T,\mu_{0},F)$. Section 7 allows us to construct a $(C,N)$-simulator
$\mathcal{A}$ with source $p$ and target $p^{\prime}$. This means, for each
$\mu\in\mathbb{N}^{d}$, we have
$\Psi\left(\mathsf{L}_{d}(\mathcal{A},p,\mu_{0},p^{\prime},\mu)\right)=\Psi\left(C\cap\mathsf{L}(N,\mu_{0},\mu)\right)$
and in particular

$\Psi\left(\underbrace{\bigcup_{\mu\in
F}\mathsf{L}_{d}(\mathcal{A},p,\mu_{0},p^{\prime},\mu)}_{=:L}\right)=\Psi\left(\bigcup_{\mu\in
F}C\cap\mathsf{L}(N,\mu_{0},\mu)\right)=\Psi\left(C\cap P\right).$

Since we can clearly construct a priority multicounter machine for $L$, the
proof of the Theorem is complete.∎

This allows us to prove Theorem 7.2.

######  Theorem 7.2.

Given a language in $\mathsf{G}_{i}$, we can recursively construct a Parikh
equivalent priority multicounter machine. According to Theorem 7.3, this is
true of $\mathsf{G}_{0}=\mathsf{fiCF}\sqcap\mathsf{P}$. Furthermore, Theorem
5.2 and Section 5 tell us that if we can carry out such a construction for
$\mathsf{G}_{i}$, we can also do it for $\mathsf{G}_{i+1}$.∎

##  8\. Conclusion

Of course, an intriguing open question is whether the storage mechanisms
corresponding to $\mathsf{SC^{+}}$ have a decidable reachability problem.
First, since their simplest instance are pushdown Petri nets, this extends the
open question concerning the latter’s reachability. Second, they naturally
subsume the priority multicounter machines of Reinhardt. This makes them a
candidate for being a quite powerful model for which reachability might be
decidable.

Observe that if these storage mechanisms turn out to exhibit decidability,
this would mean that the characterization of Lohrey and Steinberg (Theorem
3.3) remains true for all graph monoids. This can be interpreted as evidence
for decidability.

### Acknowledgments

The author is grateful to the anonymous referees of both the conference and
the journal version. Their helpful comments have greatly improved the
presentation of this work.

## References

  * [1] I. J. Aalbersberg and H. J. Hoogeboom.  Characterizations of the decidability of some problems for regular trace languages.  Mathematical Systems Theory, 22(1):1–19, 1989.
  * [2] M. F. Atig and P. Ganty.  Approximating Petri net reachability along context-free traces.  In Proceedings of the 31st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011), volume 13 of Leibniz International Proceedings in Informatics (LIPIcs), pages 152–163, Dagstuhl, Germany, 2011. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik.
  * [3] J. Berstel.  Transductions and Context-Free Languages.  Teubner, 1979.
  * [4] P. Buckheister and G. Zetzsche.  Semilinearity and context-freeness of languages accepted by valence automata.  In K. Chatterjee and J. Sgall, editors, Proceedings of the 38th International Symposium on Mathematical Foundations of Computer Science (MFCS 2013), volume 8087 of Lecture Notes in Computer Science, pages 231–242, Berlin/Heidelberg, 2013. Springer-Verlag.
  * [5] V. Diekert and G. Rozenberg, editors.  The Book of Traces.  World Scientific, Singapore, 1995.
  * [6] H. Fernau and R. Stiebe.  Sequential grammars and automata with valences.  Theoretical Computer Science, 276:377–405, 2002.
  * [7] S. Ginsburg.  Algebraic and automata-theoretic properties of formal languages.  North-Holland Publishing Company Amsterdam, 1975.
  * [8] S. Ginsburg and S. Greibach.  Principal AFL.  Journal of Computer and System Sciences, 4(4):308–338, 1970.
  * [9] J. Hartmanis and J. E. Hopcroft.  What makes some language theory problems undecidable.  Journal of Computer and System Sciences, 4(4):368–376, 1970.
  * [10] M. Kambites.  Formal languages and groups as memory.  Communications in Algebra, 37:193–208, 2009.
  * [11] M. Kambites, P. V. Silva, and B. Steinberg.  On the rational subset problem for groups.  Journal of Algebra, 309:622–639, 2007.
  * [12] J. Leroux, G. Sutre, and P. Totzke.  On the coverability problem for pushdown vector addition systems in one dimension.  In Proceedings of the 42nd International Colloquium on Automata, Languages and Programming (ICALP 2015), pages 324–336, Berlin/Heidelberg, 2015\. Springer-Verlag.
  * [13] M. Lohrey.  The rational subset membership problem for groups: a survey.  In C. M. Campbell, M. R. Quick, E. F. Robertson, and C. M. Roney-Dougal, editors, Groups St Andrews 2013, volume 422 of London Mathematical Society Lecture Note Series, pages 368–389, Cambridge, United Kingdom, 2015. Cambridge University Press.
  * [14] M. Lohrey and B. Steinberg.  The submonoid and rational subset membership problems for graph groups.  Journal of Algebra, 320(2):728–755, 2008.
  * [15] K. Reinhardt.  Reachability in Petri nets with inhibitor arcs.  Electronic Notes in Theoretical Computer Science, 223:239–264, 2008\.  Proceedings of the Second Workshop on Reachability Problems in Computational Models (RP 2008).
  * [16] A. Salomaa.  On the index of a context-free grammar and language.  Information and Control, 14(5):474–477, 1969.
  * [17] J. van Leeuwen.  A generalisation of Parikh’s theorem in formal language theory.  In Proceedings of the 2nd International Colloquium on Automata, Languages and Programming (ICALP 1974), volume 14 of Lecture Notes in Computer Science, pages 17–26, Berlin/Heidelberg, 1974. Springer-Verlag.
  * [18] E. S. Wolk.  A note on "the comparability graph of a tree".  Proceedings of the American Mathematical Society, 16(1):17–20, 1965\.
  * [19] G. Zetzsche.  Silent transitions in automata with storage.  In Proc. of the 40th International Colloquium on Automata, Languages and Programming (ICALP 2013), volume 7966 of LNCS, pages 434–445, Berlin Heidelberg, 2013. Springer.
  * [20] G. Zetzsche.  Computing downward closures for stacked counter automata.  In Proceedings of the 32nd International Symposium on Theoretical Aspects of Computer Science (STACS 2015), Leibniz International Proceedings in Informatics (LIPIcs), pages 743–756, Dagstuhl, Germany, 2015. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik.
  * [21] G. Zetzsche.  The emptiness problem for valence automata or: Another decidable extension of Petri nets.  In Proceedings of the 9th International Workshop on Reachability Problems (RP 2015), volume 9328 of Lecture Notes in Computer Science, pages 166–178, Berlin/Heidelberg, 2015. Springer-Verlag.
  * [22] G. Zetzsche.  Monoids as storage mechanisms.  Bulletin of the EATCS, 120:237–249, 2016.
  * [23] G. Zetzsche.  Monoids as Storage Mechanisms.  PhD thesis, Technische Universität Kaiserslautern, 2016.