Equivalence of Deterministic One-Counter Automata is NL-complete

We prove that language equivalence of deterministic one-counter automata is NL-complete. This improves the superpolynomial time complexity upper bound shown by Valiant and Paterson in 1975. Our main contribution is to prove that two deterministic one-counter automata are inequivalent if and only if they can be distinguished by a word of length polynomial in the size of the two input automata.