Shortest paths in one-counter systems

We show that any one-counter automaton with n states, if its language is non-empty, accepts some word of length at most O(n2). This closes the gap between the previously known upper bound of O(n3) and lower bound of Ω(n2). More generally, we prove a tight upper bound on the length of shortest paths between arbitrary configurations in one-counter transition systems (weaker bounds have previously appeared in the literature).