On the Separability Problem of VASS Reachability Languages
CoRR(2024)
摘要
We show that the regular separability problem of VASS reachability languages
is decidable and 𝐅_ω-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 ℤ-versions of the
VASS, a regular separator for the ℕ-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.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要