On Buchi One-Counter Automata

Equivalence of deterministic pushdown automata is a famous problem in theoretical computer science whose decidability has been shown by Senizergues. Our first result shows that decidability no longer holds when moving from finite words to infinite words. This solves an open problem that has recently been raised by Lading. In fact, we show that already the equivalence problem for deterministic Buchi one-counter automata is undecidable. Hence, the decidability border is rather tight when taking into account a recent result by Loding and Repke that equivalence of deterministic weak parity pushdown automata (a subclass of deterministic Biichi pushdown automata) is decidable. Another known result on finite words is that the universality problem for vector addition systems is decidable. We show undecidability when moving to infinite words. In fact, we prove that already the universality problem for nondeterministic Buchi one-counter nets (or equivalently vector addition systems with one unbounded dimension) is undecidable.