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

TL;DR

This paper investigates the boundedness and zero isolation problems for weighted automata over nonnegative rationals, showing decidability results under certain restrictions and introducing a new model called orthant vector addition systems.

Contribution

It proves boundedness is decidable for copyless linear weighted automata and introduces orthant VAS, linking zero isolation to universal coverability, with decidability results assuming Schanuel's conjecture.

Findings

Boundedness is decidable for copyless linear weighted automata.

Zero isolation reduces to universal coverability in orthant VAS.

Decidability of universal coverability in 3D OVAS under Schanuel's conjecture.

Abstract

We consider linear cost-register automata (equivalent to weighted automata) over the semiring of nonnegative rationals, which generalise probabilistic automata. The two problems of boundedness and zero isolation ask whether there is a sequence of words that converge to infinity and to zero, respectively. In the general model both problems are undecidable so we focus on the copyless linear 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 universal coverability of orthant vector addition systems (OVAS), a new model in the VAS family interesting on its own. In standard VAS runs are considered only in the positive orthant, while in OVAS every orthant has its own set of vectors that can be applied in that orthant. Assuming Schanuel's conjecture is true, we prove decidability of universal coverability for three-dimensional OVAS, which implies decidability of zero isolation in a model with at most three independent registers.