AI 中文总结
研究分支向量加法系统的可达性问题，核心方法是基于半线性归纳不变量，证明不可达配置存在不包含它的半线性归纳不变量，并据此推导出简单枚举算法解决该可达性问题。
AI 中文摘要
本文解决了分支向量加法系统（BVAS）的可达性问题，这是一个长期存在的开放问题。我们的方法基于半线性归纳不变量。具体而言，我们证明如果BVAS的一个配置不可达，那么存在一个作为半线性集给出的归纳不变量不包含此配置。基于此性质，我们推导出一个非常简单的（枚举）算法来解决BVAS的可达性问题。
英文摘要
In this paper, we solve the reachability problem for branching vector addition systems (BVAS), a long standing open problem. Our approach is based on semilinear inductive invariants. More precisely, we prove that if a configuration of a BVAS is not reachable, then there exists an inductive invariant, given as a semilinear set, that does not contain this configuration. Based on this property, we deduce a very simple (enumerative) algorithm solving the reachability problem for BVAS.
