vector addition systems [@JEM1999] and Ackermann-complete for the special case of OCNs [@HT2017]. One-counter systems have received some attention in regards to checking bisimulation and simulation relations, which under-approximate language equivalence (and inclusion, respectively) and are computationally simpler. For OCAs/OCNs, bisimulation is -complete [@BGJ2010], while weak bisimulation is undecidable for OCNs [@Mayr2003]. Both strong and weak simulation are -complete for OCNs, and checking if an OCN simulates an OCA is decidable [@AAHMKT2014].

Universality problems for OCNs over single-letter alphabets are related to the termination problem for VASS, which asks if there exists an infinite run. Non-termination naturally corresponds to the property that $a^n \in \Lang{\initialstate,\vec{v_0}}$, i.e., all finite words are accepted, assuming that all states are accepting. Termination reduces to boundedness (finiteness of the reachability set) which is -complete [@Rac1978; @Dem2013] in general and -complete for systems with fixed dimensions [@RY1985]. In contrast, the *structural* termination problem (there exists no infinite run, regardless of the initial configuration) is equivalent to finding an executable cycle that is non-decreasing on all dimensions, and can be solved in polynomial time [@KS1988].

Finally, the idea to existentially quantify over some initial resource is commonplace in the formal verification literature. Examples include unknown initial-credit problems 