On Flatness for 2-Dimensional Vector Addition Systems with States
On Flatness for 2-Dimensional Vector Addition Systems with States
复制标题
关于二维矢量加法系统的平坦度
DOI：
--
复制
发表时间：
2004
期刊：
影响因子：
--
通讯作者：
G. Sutre
中科院分区：
文献类型：
--
作者：
Jérôme Leroux;G. Sutre
带状态的向量加法系统（VASS）是计数器自动机，其中（1）计数器保持非负整数值，（2）计数器上允许的操作是递增和递减。加速符号模型检查器，如FAST、LASH或TReX，提供通用的半算法来计算VASS（和其他模型）的可达性集，但没有任何终止保证。Hopcroft和Pansiot证明了对于2-dimVASS（即具有两个计数器的VASS），可达集是有效半线性的。然而，他们使用专门设计用于分析2-dim VASS的ad-hoc算法。在本文中，我们表明，2-dimVASS是平坦的（即他们“本质上”不包含嵌套循环）。我们得到的-向前，向后和二进制可达集是有效的半线性类2维VASS，这些集可以使用通用的加速技术计算。
Vector addition systems with states (VASS) are counter automata where (1) counters hold nonnegative integer values, and (2) the allowed operations on counters are increment and decrement. Accelerated symbolic model checkers, like FAST, LASH or TReX, provide generic semi-algorithms to compute reachability sets for VASS (and for other models), but without any termination guarantee. Hopcroft and Pansiot proved that for 2-dim VASS (i.e. VASS with two counters), the reachability set is effectively semilinear. However, they use an ad-hoc algorithm that is specifically designed to analyze 2-dim VASS. In this paper, we show that 2-dim VASS are flat (i.e. they “intrinsically” contain no nested loops). We obtain that – forward, backward and binary – reachability sets are effectively semilinear for the class of 2-dim VASS, and that these sets can be computed using generic acceleration techniques.