具有周期循环的扁平计数器机器可达性问题的复杂性

本文证明了具有差值约束以及更一般的八边形关系（标记循环上的转换）的扁平计数器机器类其可达性问题的 NP 完全性。证明基于这样一个事实：此类关系的幂序列 $\{R^i\}_{i=1}^\infty$ 可以编码为周期性的矩阵序列，且该序列的前缀和周期在关系 $R$ 的二进制编码 $\bin{R}$ 的大小上均为 $2^{\mathcal{O}(\bin{R})}$。这一结果有助于刻画最受研究的计数器机器类之一的可达性问题复杂性 \cite{cav10,comon-jurski98}，并对程序验证中的其他问题具有潜在影响。