for energy games [@BFLMS2008; @AAHMKT2014] and R-Automata [@AKY2008], timed Petri nets [@AACMT2018], and inclusion problems for weighted automata [@DDGRT10; @ABK11].

We defer most proofs to the Appendix.

Preliminaries {#sec:preliminaries}
=============

##### One-Counter Nets. {#one-counter-nets. .unnumbered}

A *one-counter net* (OCN) is a finite directed graph where edges carry both an integer weight and a letter from a finite alphabet. We write $\sys{A}=\ocntuple$ for the net $\sys{A}$ where $\states$ is a finite set of *states*, $\alphabet$ is a finite set of *letters*, $\initialstate\in \states$ is an *initial state*, $\transitions\subseteq \states\x\alphabet\x\Z\x\states$ is the *transition* relation, and $\fstates\subseteq \states$ are the *accepting* states. For a transition $t=(s,a,e,s')\in\transitions$ we write $\effect{t}\eqdef e$ for its (counter) *effect*, and write $\norm{\delta}$ for the largest absolute effect among all transitions. By the *underlying automaton* of an OCN we mean the NFA obtained from the OCN by disregarding the transition effects. A path in the OCN is a sequence $\pi=(s_1,a_1,e_1,s_2)(s_2,a_2,e_2,s_3)\dots (s_{k},a_k,e_k,s_{k+1})\in\transitions^*$. 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 above *reads* word $a_1a_2\dots a_k\in\alphabet^*$ and is accepting if $s_{k+1}\in\fstates$. Its $\effect{\pi}\eqdef \sum_{i=1}^k e_i$ is the sum of its 