Separability in Büchi Vass and Singly Non-Linear Systems of Inequalities
International Colloquium on Automata, Languages and Programming(2024)
Abstract
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.
MoreTranslated text
AI Read Science
Must-Reading Tree
Example
![](https://originalfileserver.aminer.cn/sys/aminer/pubs/mrt_preview.jpeg)
Generate MRT to find the research sequence of this paper
Chat Paper
Summary is being generated by the instructions you defined