2018/02/19 by Wojciech Czerwiński, Czerwiński, Wojciech, Piotr Hofman +3 · 1 citation
Computer Science · #Advanced Algebra and Logic #FOS: Computer and information sciences #Formal Languages and Automata Theory (cs.FL) #Logic, programming, and type systems #semigroups and automata theory
paper · pdf · doi:10.48550/arxiv.1802.06683
openalex publication_date 2018/02/19 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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 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 K with mild conditions on K, and (iii)~universality of the set of factors.