一句话：证明 VASS 可达语言的正则可分离性可判定且为 Fω-完全，并引入双标记图转移序列分解算法。
本文研究向量加法系统（VASS）可达语言的正则可分离性问题：给定两个 VASS 可达语言，是否存在正则语言包含其中一个且与另一个不相交。作者证明该问题是可判定的，且其复杂度为 Fω-完全。核心工具是双标记图转移序列（DMGTS），一种跟踪待分离 VASS 的适当乘积的新证明对象。作者为 DMGTS 设计了分解算法，不仅达到已知 MGTS 的完美性，还满足新提出的忠实性。忠实性使得可以从 VASS 的 Z-版本正则分离器构造出 N-版本的正则分离器，其关键在于：为判定可分离性，只需跟踪一个 VASS 的计数器模一个由分解确定的大数。
We show that the regular separability problem of VASS reachability languages is decidable and Fω-complete. At the heart of our decision procedure are doubly-marked graph transition sequences, a new proof object that tracks a suitable product of the VASS we wish to separate. We give a decomposition algorithm for DMGTS that not only achieves perfectness as known from MGTS, but also a new property called faithfulness. Faithfulness allows us to construct, from a regular separator for the Z-versions of the VASS, a regular separator for the N-versions. Behind faithfulness is the insight that, for separability, it is sufficient to track the counters of one VASS modulo a large number that is determined by the decomposition.