Büchi VASS中的可分离性与单非线性不等式系统
Separability in Büchi Vass and Singly Non-Linear Systems of Inequalities
AI总结：
本文证明Büchi VASS覆盖语言的omega-正则可分离性问题是EXPSPACE完全的，并在固定维度下达到PSPACE复杂度，其核心技术是分析单非线性不等式系统并给出其有理数解的指数级大小上界。
摘要：
Büchi VASS覆盖语言的正则可分离性问题最近被证明是可判定的，但其复杂度下界为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判定过程。
英文摘要：
The omega-regular separability problem for Büchi VASS coverability languages has recently been shown to be decidable, but with an EXPSPACE lower and a non-primitive recursive upper bound -- the exact complexity remained open. We close this gap and show that the problem is EXPSPACE-complete. A careful analysis of our complexity bounds additionally yields a PSPACE procedure in the case of fixed dimension >= 1, which matches a pre-established lower bound of PSPACE for one dimensional Büchi VASS. Our algorithm is a non-deterministic search for a witness whose size, as we show, can be suitably bounded. Part of the procedure is to decide the existence of runs in VASS that satisfy certain non-linear properties. Therefore, a key technical ingredient is to analyze a class of systems of inequalities where one variable may occur in non-linear (polynomial) expressions. These so-called singly non-linear systems (SNLS) take the form A(x).y >= b(x), where A(x) and b(x) are a matrix resp. a vector whose entries are polynomials in x, and y ranges over vectors in the rationals. Our main contribution on SNLS is an exponential upper bound on the size of rational solutions to singly non-linear systems. The proof consists of three steps. First, we give a tailor-made quantifier elimination to characterize all real solutions to x. Second, using the root separation theorem about the distance of real roots of polynomials, we show that if a rational solution exists, then there is one with at most polynomially many bits. Third, we insert the solution for x into the SNLS, making it linear and allowing us to invoke standard solution bounds from convex geometry. Finally, we combine the results about SNLS with several techniques from the area of VASS to devise an EXPSPACE decision procedure for omega-regular separability of Büchi VASS.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
