发表机构
University of Bordeaux, CNRS, Bordeaux INP; University of Warsaw（波尔多大学; 华沙大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文研究分支VASS的可达性问题，证明其可达集是VASS的截面，并利用新的良拟序和融合性质，得出5维BVAS可达集有效半线性的结论。
AI 中文摘要
带状态的向量加法系统（VASS）是一种等价于Petri网的模型，它们是有限状态机，具有有限多个取值于自然数的计数器。VASS的可判定可达性问题在逻辑、自动机和验证中有许多应用。在本文中，我们研究了BVASS（VASS的分支推广）的可达性问题。我们证明BVASS的可达集与VASS的可达集非常相似，即它们是VASS的截面。我们的证明依赖于BVASS运行上的一种新的良拟序（wqo），该良拟序推广了VASS运行上众所周知的良拟序。通过利用一个融合性质，我们证明了每个BVASS运行都可以转化为一个具有有界分支复杂度的等价运行。这使我们能够推导出关于BVASS可达集几何形状的几个结果。作为一个应用，我们获得了5维BVAS的可达集是有效半线性的，正如5维VAS的情况一样。
英文摘要
Vectors addition systems with states (VASS), a model equivalent to Petri nets, are finite-state machines with finitely many counters ranging over the natural numbers. The decidable reachability problem for VASS has many applications in logic, automata, and verification. In this paper we study the reachability problem for BVASS, a branching generalization of VASS. We show that BVASS reachability sets are very similar to VASS reachability sets, namely that they are sections of VASS. Our proof relies on a new well-quasi-order (wqo) on BVASS runs that generalizes the well-known wqo on VASS runs. By leveraging an amalgamation property, we prove that every BVASS run can be transformed into an equivalent one of bounded branching complexity. This allows us to derive several results on the geometry of BVASS reachability sets. As an application we obtain that reachability sets of 5-dimensional BVAS are effectively semilinear, as is the case for 5-dimensional VAS.
Comments25 pages, extended version of the paper with same title and same authors presented at FOSSACS'26
