Document Open Access Logo

Separability in Büchi VASS and Singly Non-Linear Systems of Inequalities

Authors Pascal Baumann , Eren Keskin , Roland Meyer , Georg Zetzsche

PDF
Thumbnail PDF

File

LIPIcs.ICALP.2024.126.pdf
  • Filesize: 0.84 MB
  • 19 pages

Document Identifiers

Author Details

Pascal Baumann
  • Max Planck Institute for Software Systems (MPI-SWS), Kaiserslautern, Germany
Eren Keskin
  • TU Braunschweig, Germany
Roland Meyer
  • TU Braunschweig, Germany
Georg Zetzsche
  • Max Planck Institute for Software Systems (MPI-SWS), Kaiserslautern, Germany

Funding

Funded by the European Union (ERC, FINABIS, 101077902). Views and opinions expressed are however those of the author(s) only and do not necessarily reflect those of the European Union or the European Research Council Executive Agency. Neither the European Union nor the granting authority can be held responsible for them.

Cite AsGet BibTex

Pascal Baumann, Eren Keskin, Roland Meyer, and Georg Zetzsche. Separability in Büchi VASS and Singly Non-Linear Systems of Inequalities. In 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 297, pp. 126:1-126:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.ICALP.2024.126

Abstract

The ω-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 ω-regular separability of Büchi VASS.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic
  • Theory of computation → Formal languages and automata theory
Keywords
  • Vector addition systems
  • infinite words
  • separability
  • inequalities
  • quantifier elimination
  • rational
  • polynomials

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

References

  1. M. F. Atig and P. Habermehl. On Yen’s path logic for Petri nets. Int. J. Found. Comput. Sci., 22(4):783-799, 2011. URL: https://doi.org/10.1142/S0129054111008428.
  2. P. Baumann, R. Meyer, and G. Zetzsche. Regular separability in Büchi VASS. In Proc. STACS, volume 254 of LIPIcs, pages 9:1-9:19. Schloss Dagstuhl, 2023. URL: https://doi.org/10.4230/LIPICS.STACS.2023.9.
  3. Pascal Baumann, Roland Meyer, and Georg Zetzsche. Regular separability in Büchi VASS. CoRR, abs/2301.11242, 2023. URL: https://doi.org/10.48550/arXiv.2301.11242.
  4. M. Blockelet and S. Schmitz. Model checking coverability graphs of vector addition systems. In Proc. MFCS, volume 6907 of LNCS, pages 108-119. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-22993-0_13.
  5. L. Clemente, W. Czerwiński, S. Lasota, and C. Paperman. Regular separability of parikh automata. In Proc. ICALP, volume 80 of LIPIcs, pages 117:1-117:13. Schloss Dagstuhl, 2017. URL: https://doi.org/10.4230/LIPICS.ICALP.2017.117.
  6. L. Clemente, W. Czerwiński, S. Lasota, and C. Paperman. Separability of reachability sets of vector addition systems. In H. Vollmer and B. Vallée, editors, Proc. STACS, volume 66 of LIPIcs, pages 24:1-24:14. Schloss Dagstuhl, 2017. URL: https://doi.org/10.4230/LIPICS.STACS.2017.24.
  7. W. Czerwiński and P. Hofman. Language inclusion for boundedly-ambiguous vector addition systems is decidable. In Proc. CONCUR, volume 243 of LIPIcs, pages 16:1-16:22. Schloss Dagstuhl, 2022. URL: https://doi.org/10.4230/LIPICS.CONCUR.2022.16.
  8. W. Czerwiński, P. Hofman, and G. Zetzsche. Unboundedness problems for languages of vector addition systems. In Proc. ICALP, volume 107 of LIPIcs, pages 119:1-119:15. Schloss Dagstuhl, 2018. URL: https://doi.org/10.4230/LIPICS.ICALP.2018.119.
  9. W. Czerwiński and S. Lasota. Regular separability of one counter automata. Log. Methods Comput. Sci., 15(2), 2019. URL: https://doi.org/10.23638/LMCS-15(2:20)2019.
  10. W. Czerwiński, S. Lasota, R. Meyer, S. Muskalla, K. N. Kumar, and P. Saivasan. Regular separability of well-structured transition systems. In Proc. CONCUR, volume 118 of LIPIcs, pages 35:1-35:18. Schloss Dagstuhl, 2018. URL: https://doi.org/10.4230/LIPICS.CONCUR.2018.35.
  11. W. Czerwiński and G. Zetzsche. An approach to regular separability in vector addition systems. In Proc. LICS, pages 341-354. ACM, 2020. URL: https://doi.org/10.1145/3373718.3394776.
  12. S. Demri. On selective unboundedness of VASS. JCSS, 79(5):689-713, 2013. URL: https://doi.org/10.1016/J.JCSS.2013.01.014.
  13. E. M. Gurari and O. H. Ibarra. An NP-complete number-theoretic problem. J. ACM, 26(3):567-581, 1979. URL: https://doi.org/10.1145/322139.322152.
  14. P. Habermehl. On the complexity of the linear-time μ-calculus for Petri Nets. In Proc. ICATPN, volume 1248 of LNCS, pages 102-116. Springer, 1997. URL: https://doi.org/10.1007/3-540-63139-9_32.
  15. E. Keskin and R. Meyer. Separability and non-determinizability of WSTS. In Proc. CONCUR, volume 279 of LIPIcs, pages 8:1-8:17. Schloss Dagstuhl, 2023. URL: https://doi.org/10.4230/LIPICS.CONCUR.2023.8.
  16. E. Keskin and R. Meyer. On the separability problem of VASS reachability languages. In To appear in Proc. of LICS, 2024. Google Scholar
  17. C. Köcher and G. Zetzsche. Regular separators for VASS coverability languages. In Proc. FSTTCS, volume 284 of LIPIcs, pages 15:1-15:19. Schloss Dagstuhl, 2023. URL: https://doi.org/10.4230/LIPICS.FSTTCS.2023.15.
  18. S. R. Kosaraju. Decidability of reachability in vector addition systems (preliminary version). In Proc. STOC, pages 267-281. ACM, 1982. URL: https://doi.org/10.1145/800070.802201.
  19. J.-L. Lambert. A structure to decide reachability in Petri nets. Theor. Comput. Sci., 99(1):79-104, 1992. URL: https://doi.org/10.1016/0304-3975(92)90173-D.
  20. S. Lang. Algebra, Rev. 3rd Ed. Springer, New York, 2002. Google Scholar
  21. J. Leroux. Vector addition system reachability problem: a short self-contained proof. In Proc. POPL, pages 307-316. ACM, 2011. URL: https://doi.org/10.1145/1926385.1926421.
  22. J. Leroux and S. Schmitz. Demystifying reachability in vector addition systems. In Proc. LICS, pages 56-67. IEEE Computer Society, 2015. URL: https://doi.org/10.1109/LICS.2015.16.
  23. R. J. Lipton. The reachability problem requires exponential space. Technical Report 63, Yale University, 1976. Google Scholar
  24. Angus Macintyre, Kenneth McKenna, and Lou van den Dries. Elimination of quantifiers in algebraic structures. Advances in Mathematics, 47(1):74-87, 1983. URL: https://doi.org/10.1016/0001-8708(83)90055-5.
  25. D. Marker. Model Theory: An Introduction. Springer, New York, 2002. Google Scholar
  26. E. W. Mayr. An algorithm for the general Petri net reachability problem. SIAM J. Comput., 13(3):441-460, 1984. URL: https://doi.org/10.1137/0213029.
  27. B. Mishra. Algorithmic Algebra. Texts and Monographs in Computer Science. Springer, 1993. URL: https://doi.org/10.1007/978-1-4612-4344-1.
  28. C. Rackoff. The covering and boundedness problems for vector addition systems. Theor. Comput. Sci., 6:223-231, 1978. URL: https://doi.org/10.1016/0304-3975(78)90036-1.
  29. W. J. Savitch. Relationships between nondeterministic and deterministic tape complexities. JCSS, 4(2):177-192, 1970. URL: https://doi.org/10.1016/S0022-0000(70)80006-X.
  30. A. Schrijver. Theory of linear and integer programming. John Wiley & Sons, 1986. Google Scholar
  31. R. S. Thinniyam and G. Zetzsche. Regular separability and intersection emptiness are independent problems. In Proc. FSTTCS, volume 150 of LIPIcs, pages 51:1-51:15. Schloss Dagstuhl, 2019. URL: https://doi.org/10.4230/LIPICS.FSTTCS.2019.51.
  32. V. Weispfenning. The complexity of almost linear diophantine problems. J. Symb. Comput., 10(5):395-404, 1990. URL: https://doi.org/10.1016/S0747-7171(08)80051-X.
  33. H.-C. Yen. A unified approach for deciding the existence of certain Petri net paths. Information and Computation, 96(1):119-137, 1992. URL: https://doi.org/10.1016/0890-5401(92)90059-O.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact