
Clotilde Bizière (LaBRI) and Wojciech Czerwiński (University of Warsaw) have a paper accepted in the prestigious STOC conference to be held June 23-27, 2025, in Prague (Czech Republic).
We work on automata, mathematical objects used to model computation. In particular, we're interested in the problem of accessibility in stateful vector addition systems (or VASS) with stacks. These automata combine a stack, which models recursion (such as function calls), and counters, which model concurrency. The reachability problem consists in determining whether such a system can reach a given configuration.
This problem has been extensively studied in stack automata on the one hand, and in non-stack VASS on the other, but its decidability remains open in the case of stack VASS. In other words, we know how to treat recursion and concurrency separately, but their combination remains poorly understood.
Our paper makes a breakthrough on this issue by proposing an algorithm for stack VASS of dimension 1, i.e. automata with a stack and a single counter.
The preprint on arwiv, here.