The boundedness and zero isolation problems for weighted automata over nonnegative rationals

We consider linear cost-register automata (equivalently, weighted automata) over the semiring of nonnegative rationals, which generalise probabilistic automata. The two problems boundedness and zero isolation ask whether there is a sequence of words that converge to infinity and zero, respectively. In the general model both problems are undecidable so we focus on the copyless restriction. There, we show that the boundedness problem is decidable. As for the zero isolation problem we need to further restrict the class. We obtain a model, where zero isolation becomes equivalent to coverability of orthant vector addition systems (OVAS), a new model in the VAS family interesting on its own. Assuming Schanuel’s conjecture is true, we prove decidability of coverability for three-dimensional OVAS, which gives decidability of zero isolation in a model with at most three registers. Joint work with Wojciech Czerwiński, Engel Lefaucheux, David Purser and Markus Whiteland.