Büchi VASS与单非线性不等式系统的可分离性
形式语言与自动机理论
2024-06-04 v1
摘要
Büchi VASS覆盖语言的omega-正则可分离性问题最近已被证明可判定,但其下界为EXPSPACE、上界为非原始递归——确切复杂度仍未解决。我们填补了这一空白,证明该问题是EXPSPACE完全的。对我们复杂度界限的仔细分析还给出了在固定维度>=1情况下的PSPACE过程,这与一维Büchi VASS已建立的PSPACE下界相匹配。我们的算法是对一个见证者的非确定性搜索,我们证明该见证者的大小可以被适当界定。该过程的一部分是判定VASS中是否存在满足某些非线性性质的运行。因此,一个关键技术要素是分析一类不等式系统,其中某个变量可能出现在非线性(多项式)表达式中。这些所谓的单非线性系统(SNLS)形式为A(x).y >= b(x),其中A(x)和b(x)分别是矩阵和向量,其条目是x的多项式,而y的取值范围是有理向量。我们在SNLS上的主要贡献是关于单非线性系统有理解大小的指数上界。证明包含三个步骤。首先,我们给出一个定制的量词消去来刻画x的所有实数解。其次,利用关于多项式实根距离的根分离定理,我们证明如果存在有理数解,则存在一个最多具有多项式比特数的解。第三,我们将x的解代入SNLS,使其线性化,从而允许我们调用凸几何中的标准解界限。最后,我们将关于SNLS的结果与VASS领域的多种技术相结合,为Büchi VASS的omega-正则可分离性设计了一个EXPSPACE判定过程。
引用
@article{arxiv.2406.01008,
title = {Separability in B\"uchi Vass and Singly Non-Linear Systems of Inequalities},
author = {Pascal Baumann and Eren Keskin and Roland Meyer and Georg Zetzsche},
journal= {arXiv preprint arXiv:2406.01008},
year = {2024}
}