Unboundedness problems for languages of vector addition systems
Abstract
A vector addition system (VAS) with an initial and a final marking and transition labels induces a language. In part because the reachability problem in VAS remains far from being well-understood, it is difficult to devise decision procedures for such languages. This is especially true for checking properties that state the existence of infinitely many words of a particular shape. Informally, we call these \emph{unboundedness properties}. We present a simple set of axioms for predicates that can express unboundedness properties. Our main result is that such a predicate is decidable for VAS languages as soon as it is decidable for regular languages. Among other results, this allows us to show decidability of (i)~separability by bounded regular languages, (ii)~unboundedness of occurring factors from a language with mild conditions on , and (iii)~universality of the set of factors.
Cite
@article{arxiv.1802.06683,
title = {Unboundedness problems for languages of vector addition systems},
author = {Wojciech Czerwiński and Piotr Hofman and Georg Zetzsche},
journal= {arXiv preprint arXiv:1802.06683},
year = {2018}
}