We show certificates of size O(n²), with subcubic verification algorithms, for language emptiness and non-emptiness of pushdown automata on n states. As a consequence, fine-grained reductions from SAT are unlikely to explain the cubic bottleneck for CFL reachability.

Conversion from OCA to Parikh-equivalent NFA requires a quasi-polynomial growth in description size. To prove this, we define and study a one-player game akin to pebbling.

Imagine a “blind” Turing machine that cannot read bits written on the tape, but can increment a decrement them. The content of the tape is interpreted as the binary expansion of a rational number, and increments and decrements simply add and subtract (possibly negative) powers of two. What sets of numbers do these machines accept?

Every one-counter automaton with n states accepts a word of length at most 14n², unless its language is empty.

We propose a definition of synchronizing words for nested word automata.

What happens with reachability and coverability sets of VASS where counters can go negative and support reset? Also, a Π₂P lower bound on the inclusion problem for linear sets.

The downward and upward closure of one-counter languages have small NFA. So does the Parikh image if the alphabet has fixed size.

How many states does a {OCA, DPDA, Turing machine} need to have in order to accept the singleton language {aⁿ} ?

DPDA equivalence is in P for unary (singleton) input alphabet. This relies on algorithmics for grammar-compressed strings. Also, deciding if a CFG generates words of all lengths is Π₂P-complete.

Schützenberger’s construction for the uniformization of rational relations extends to nested words.