One-counter automata (OCA) are finite-state automata with a counter that supports increments, decrements, and tests for zero. They correspond to an intermediate class between regular and context-free languages and are suitable for modeling "counting'' phenomena. However, reasoning about OCA is often intractable: for example, language equivalence is undecidable for nondeterministic OCA, and for deterministic OCA it took 40 years to prove the existence of short distinguishing words.
In this talk, I will give a review of OCA and reasoning tasks for them and discuss two tractability results:
(1) shortest paths between configurations of OCA are of at most quadratic length;
(2) the Parikh (commutative) image and sub-/superword closures of the language are accepted by small nondeterministic finite automata.