A Selection of Recent Results in Automata with Counters

In this seminar, I will talk about an upper bounding technique that seemingly first appears in the details of the Rackoff's proof that unboundedness in VASS can be witnessed by doubly-exponential length runs. The idea, which can be called "cycle replacement", also appears in Lin's correction of Chrobak's proof that unary NFAs have a quadratic size normal form. In the last year, we have used this technique twice for relatively different problems. In the first part of this presentation, I will explain why reachability in 1-VASS extended with integer counters is in NP (regardless of whether unary or binary encoding is used). In the second part of this presentation, I will explain that unary weighted finite automata over the tropical semiring (min, +) also have quadratic size normal forms.

BASICS Ground Seminar
Shanghai Jiao Tong University, Shanghai, China
Henry Sinclair-Banks, 02/06/26