优先向量加法系统的可平坦性
Flattability of Priority Vector Addition Systems
AI总结：
本文研究了优先向量加法系统（Priority VAS）的可达性问题，证明了 flattening 技术对其所有半线性可达性关系均可终止，且 Priority VAS 允许半线性归纳不变式，核心是通过在运行上定义具有良好泵性质的良拟序获得这些结果。
摘要：
向量加法系统（VAS），也称为 Petri 网，是并发系统的流行模型。许多领域的问题都可归约到 VAS 的可达性问题，即判定 VAS 的目标向量是否可从给定初始配置到达。解决实际实例上该问题的一种方法称为 flattening，直观上是展开嵌套循环。已知该技术对于半线性 VAS 是可终止的。本文中，我们证明对于带有嵌套零测试的 VAS（称为 Priority VAS），flattening 确实对所有半线性可达性关系都可终止。此外，我们证明 Priority VAS 允许半线性归纳不变式。这两个结果都是通过在 Priority VAS 的运行上定义一个具有良好泵性质的良拟序来获得的。
英文摘要：
Vector addition systems (VAS), also known as Petri nets, are a popular model of concurrent systems. Many problems from many areas reduce to the reachability problem for VAS, which consists of deciding whether a target configuration of a VAS is reachable from a given initial configuration. One of the main approaches to solve the problem on practical instances is called flattening, intuitively removing nested loops. This technique is known to terminate for semilinear VAS. In this paper, we prove that also for VAS with nested zero tests, called Priority VAS, flattening does in fact terminate for all semilinear reachability relations. Furthermore, we prove that Priority VAS admit semilinear inductive invariants. Both of these results are obtained by defining a well-quasi-order on runs of Priority VAS which has good pumping properties.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
