decidable, but Ackermann-complete [@HT2017], and the lower bound depends strongly on the assumption that we start with a fixed initial counter (and that its value is not bounded). The two new variants of the universality problem relax these assumptions in an attempt to allow efficient decision procedures via simple cycle analysis or similar.

##### Our Results. {#our-results. .unnumbered}

We show that both initial-value universality and bounded universality are undecidable (\[sec:nondet\]). The proofs use techniques from weighted automata [@DDGRT10; @ABK11], reducing the halting problem of two-counter machines to our setting. In light of these negative results, we proceed to study restricted classes of OCNs, for which the problems become decidable, as we elaborate below. In most cases, the complexity crucially depends on how transition updates are encoded: we consider both the case of “succinct”, binary-encoded updates, and the case of unary-encoded updates, which corresponds to systems where transitions can only update the counter by $\pm 1$.

The most intricate and interesting case is that of OCNs over a single-letter alphabet (\[sec:unary\]). In order to analyze this model, we split universality to criteria on “short” words, and on longer words that admit a cyclic behavior. In particular, we devise a canonical representation 