向量加法系统半线性归纳不变量的仅前向构造

向量加法系统（VAS）的可达性问题是在无限状态系统理论中的一个核心判定问题，由Kosaraju和Mayr在20世纪80年代首次解决。Leroux引入的一种替代性、概念上更简单的方法表明，不可达性总是由半线性归纳不变量所见证，通过结合运行枚举与对此类不变量的搜索产生了一个判定过程。然而，这些不变量的构造依赖于一个前后往返的方案，该方案对称地依赖于源和目标。因此，这些不变量不能保证反映VAS的结构性质，并且该构造难以扩展到诸如分支VAS等非对称模型。我们为VAS引入了一种新的仅前向的半线性归纳不变量构造方法。我们的方法仅从源配置构建不变量，避免了向后推理的需要。这产生了更规范且与系统结构更一致的不变量。特别是，我们的方法为周期VAS生成周期归纳不变量。除了其内在价值外，我们的方法为将基于不变量的技术扩展到分支VAS迈出了一步。