One-Counter Nets (OCNs) are finite-state machines equipped with an integer counter that
cannot decrease below zero and cannot be explicitly tested for zero.


An OCN $A$ over alphabet $\sum$ accepts a word $w \in \sum^\*$ from initial counter value $c\in\mathbb{N}$ if there is a run of $A$ on $w$ from an initial state to an accepting state in which the counter,starting from value $c$, does not become negative. Thus, for every counter value $c\in\mathbb{N}$ the OCN $A$ defines a language $L(A,c) \subseteq \sum^\*$.


As is the case with many computational models, certain decision problems for deterministic OCNs (OCNs that admit a single legal transition for each state $q$ and letter $\sigma$), denoted DOCNs, are computationally easier than for nondeterministic OCNs.


A one-counter net (OCN) is a finite automaton whose transitions are labelled both by letters and by integer weights. Formally, an OCN is a tuple $A = \langle \sum, Q, s\_0, \delta, F\rangle$ where $\sum$ is a finite alphabet, $Q$ is a finite set of states, $s\_0 \in Q$ is the initial state, $\delta \subseteq Q × \sum × \mathbb{Z} × Q$ is the set of transitions, and $F \subseteq Q$ are the accepting states. We say that an OCN is **deterministic** if for every $s \in Q, \delta \in \sum,$ there is at most one transition $(s, \sigma, e, s′)$ for some $e ∈ \mathbb{Z}$ and $s′ \in Q$.
For a transition $t = (s, \sigma, e, s′)\in \delta$ we define ***eff***$(t) = e$ to be its (counter) effect.


A path in the OCN is a sequence $\pi= (s\_1, \sigma\_1, e\_1, s\_2)(s\_2, \sigma\_2, e\_2, s\_3)\dots(s\_k, \sigma\_k, e\_k, s\_{k+1})\delta^\*.$


Such a path $\pi$ is a cycle if $s\_1 = s\_{k+1}$, and is a simple cycle if no other cycle is a proper infix of it. We say that the path $\pi$ reads the word $\sigma\_1\sigma\_2\dots\sigma\_k \in \sum^∗.$


The effect of $\pi$ is ***eff***$(\pi) =\Sigma\_{i=1}^k e\_i$, and its *nadir*, denoted ***nadir***$(\pi)$, is the minimal effect of any prefix of $\pi$(note that the nadir is non-positive, since ***eff***$(\epsilon) = 0)$.
A configuration of an OCN is a pair $(s, v) \in Q × \mathbb{N}$ comprising a state and a non-negative integer. For a letter $\sigma \in \sum$ and configurations $(s, v),(s′, v′)$ we write $(s,v)\xrightarrow{\sigma}(s′, v′)$ if there exists $d\in\mathbb{Z}$ such that $v′ = v + d$ and $(s, \sigma, d, s′)\in\delta$.
A run of $A$ from initial counter $c$ on a word $w = \sigma\_1\sigma\_2\dots\sigma\_k\in\sum^\*$is a sequence of configurations $\rho = (q\_0, v\_0),(s\_1, v\_1)\dots(s\_k, v\_k)$ such that $v\_0 = c$ and for every $1 \leq i \leq k$ it holds that $(s\_{i−1}, v\_{i−1})\xrightarrow{\sigma\_i}(s\_i, v\_i)$. Since configurations may only have a non-negative counter, this enforces that the counter does not become negative.


**My question**:  

Is the following problem decidable? (does there exist an algorithm that solves it for all instances)


* Input: Given an OCN $A$ and a DOCN $D$,
* Question: is $L(A,0)=L(D,0)$?


**References**
(<https://drops.dagstuhl.de/opus/volltexte/2022/17081/pdf/LIPIcs-CONCUR-2022-18.pdf>)


Piotr Hofman, Patrick Totzke "[Trace Inclusion for One-Counter Nets Revisited](https://arxiv.org/abs/1404.5157)".


Piotr Hofman, Richard Mayr, Patrick Totzke "[Decidability of Weak Simulation on One-counter Nets](https://arxiv.org/abs/1304.4104)".



Equivalence between deterministic and non-deterministic counter net
The short answer is that as far as I'm aware, this question is open.
It is however very close to ones that are settled. I provide some more detail below.


As you've correctly pointed out, the decidability status of decision problems relating to counter automata
often depends on the presence of non-determinism, but also on the acceptance criterion.
The initial counter value should not matter as long as it is fixed (you can always build another automaton in the same class that sets the initial value via some initial chain of states. This will change the language of the automaton but will not change the decidability status of most decision problems). I will assume below that the initial counter is $0$ always.


There are three natural ways to define accepting runs, and thus the language of the automaton:


1. **Trace semantics**: A run is accepting if the effect of every prefix is greater equal to $0$. So you simply don't starve. Let's write $T(A)$ for the set of words in $\Sigma^\*$ so that the automaton $A$ (with some fixed initial state) has some accepting run on them. This is the semantics your original is about.
2. **Coverability semantics**: A run is accepting if it does not (starve as above) and ends in a "final" state. This is a designated subset of the control states, fixed as part of the automaton's definition. Let's write $C(A)$ for the resulting coverability language of $A$.
3. **Reachability semantics**: A run is accepting if it satisfies 1), 2) and ends in counter value $0$. Let's write $R(A)$ for the corresponding language of $A$.


#### Let's consider the reachability semantics first.


Here, the language universality problem ($R(A) = \Sigma^\*$?) is already undecidable ([0], theorem 10).
Since you can easily build a *deterministic* finite automaton, and therefore OCN, with $\Sigma^\*$, the undecidability of universality transfers to both inclusion and equivalence.


#### For the coverability and trace semantics,


universality remains decidable [1,2], yet inclusion is not [3].
In fact, [2,3] are written solely in terms of trace semantics but the argument for the upper bounds (decidability and complexity) in [2] works the same for coverability semantics, and the undecidability in [3] trivially transfers from the easier trace inclusion ($T(A)\subseteq T(B)$?) to coverability language inclusion ($C(A)\subseteq C(B)$?) by making all states final.
The argument for the undecidability of trace inclusion also works if the system $A$ on the left is deterministic, but *not* if $B$ on the RHS is deterministic.


You can reduce inclusion to equivalence by a small trick:
to check if $T(A)\subseteq T(B)$ you can equivalently check if $T(A') = T(B')$ for the modified automata where
$A' \rightarrow A$,
$A' \rightarrow B$
and $B'\rightarrow B$.
(after one step, $B'$ continues as $B$ and $A'$ can continue either as $A$ or $B$).
This will *make* $A'$ non-deterministic. It shows that trace (and thus cover) equivalence $T(A)=T(B)$ is undecidable for two non-deterministic OCN.


#### Your question


Trace equivalence ($T(A) = T(B)$?) between a OCN $A$ and a DOCN $B$, is open as fact as I'm aware.
Notice that you **cannot** decide it by checking two-way inclusion
because, as argued above, the inclusion $T(B)\subseteq T(A)$ is undecidable.


**Remark 1:**
The inclusion $T(A)\subseteq T(B)$ is in fact decidable if $B$ is deterministic. This can be shown in several ways, for example by checking simulation preorder [4] (if the RHS is deterministic then language inclusion coincides with simulation).
Alternatively, you can complement $B$ into a one-counter *automaton* $B'$ (that has explicit zero-testing transitions) then checking emptiness for $A\times B'$ via [5].
This will also work for a slightly larger class of "history-deterministic" automaton the RHS [6].


**Remark 2:**
If you consider languages of infinite words,
these are significantly more complex, both topologically and in terms of decision problems.
The languages recognised by OCN accepting by infinitely often visiting final states,
are not even Borel [7] and have and undecidable universality problem [8].
So in this case again, the equivalence of infinite trace languages is undecidable.


I hope this is useful; thanks for the very interesting question! Best wishes, P.




---


[0]: *Petri nets and regular languages*. Rüdiger Valk, Guy Vidal-Naquet
<https://doi.org/10.1016/0022-0000(81)90067-2>


[1]: *Petri Nets and Regular Processes* Petr Jančar, Javier Esparza, Faron Moller; <https://doi.org/10.1006/jcss.1999.1643>


[2]: *Trace inclusion for one-counter nets revisited* Piotr Hofman, and Patrick Totzke <https://doi.org/10.1016/j.tcs.2017.05.009>


[3]: *Decidability of Weak Simulation on One-Counter Nets*. Piotr Hofman, Richard Mayr, and Patrick Totzke. <http://doi.org/10.1109/LICS.2013.26>


[4]: *Simulation Over One-Counter Nets*. Piotr Hofman, Sławomir Lasota, Richard Mayr, and Patrick Totzke
(The paper appeared in LMCS, I cannot post more than 7 links apparently, sorry)


[5]: *Reachability in Petri nets with inhibitor arcs.* Klaus Reinhardt. <https://doi.org/10.1016/j.entcs.2008.12.042>


[6]: *On History-Deterministic One-Counter Nets*. Adityaf Prakash & K. S. Thejaswini
<https://link.springer.com/chapter/10.1007/978-3-031-30829-1_11>


[7]: *Büchi VASS recognise w-languages that are $\Sigmaˆ1\_1$-complete*. Michal Skrzypczak. <https://arxiv.org/abs/1708.09658>


[8]: *On Büchi One-Counter Automata*.
Böhm, Stanislav; Göller, Stefan; Halfon, Simon ;Hofman, Piotr
<https://drops.dagstuhl.de/opus/volltexte/2017/7019/>


