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
Shaull Almagor, Asaf Yeshurun Determinization of One-Counter Nets
Piotr Hofman, Patrick Totzke "Trace Inclusion for One-Counter Nets Revisited".
Piotr Hofman, Richard Mayr, Patrick Totzke "Decidability of Weak Simulation on One-counter Nets".
