Document Open Access Logo

Regular Separability in Büchi VASS

Authors Pascal Baumann , Roland Meyer , Georg Zetzsche

PDF

File

Thumbnail PDF
PDF
LIPIcs.STACS.2023.9.pdf
  • Filesize: 0.91 MB
  • 19 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Models of computation
Keywords
  • Separability problem
  • Vector addition systems
  • Infinite words
  • Decidability

Metrics

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

Abstract

We study the (ω-)regular separability problem for Büchi VASS languages: Given two Büchi VASS with languages L₁ and L₂, check whether there is a regular language that fully contains L₁ while remaining disjoint from L₂. We show that the problem is decidable in general and PSPACE-complete in the 1-dimensional case, assuming succinct counter updates. The results rely on several arguments. We characterize the set of all regular languages disjoint from L₂. Based on this, we derive a (sound and complete) notion of inseparability witnesses, non-regular subsets of L₁. Finally, we show how to symbolically represent inseparability witnesses and how to check their existence.

Cite As Get BibTex

Pascal Baumann, Roland Meyer, and Georg Zetzsche. Regular Separability in Büchi VASS. In 40th International Symposium on Theoretical Aspects of Computer Science (STACS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 254, pp. 9:1-9:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023) https://doi.org/10.4230/LIPIcs.STACS.2023.9

Author Details

Pascal Baumann
  • Max Planck Institute for Software Systems (MPI-SWS), Kaiserslautern, 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. The second author was supported by the DFG project EDS@SYN: Effective Denotational Semantics for Synthesis.

References

  1. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Vrunda Dave, and Shankara Narayanan Krishna. On the Separability Problem of String Constraints. In Igor Konnov and Laura Kovács, editors, 31st International Conference on Concurrency Theory, CONCUR 2020, September 1-4, 2020, Vienna, Austria (Virtual Conference), volume 171 of LIPIcs, pages 16:1-16:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2020.16.
  2. Mohamed Faouzi Atig and Peter 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.
  3. Michel Blockelet and Sylvain Schmitz. Model checking coverability graphs of vector addition systems. In Filip Murlak and Piotr Sankowski, editors, Mathematical Foundations of Computer Science 2011 - 36th International Symposium, MFCS 2011, Warsaw, Poland, August 22-26, 2011. Proceedings, volume 6907 of Lecture Notes in Computer Science, pages 108-119. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-22993-0_13.
  4. Michael Blondin, Matthias Englert, Alain Finkel, Stefan Göller, Christoph Haase, Ranko Lazic, Pierre McKenzie, and Patrick Totzke. The Reachability Problem for Two-Dimensional Vector Addition Systems with States. J. ACM, 68(5):34:1-34:43, 2021. URL: https://doi.org/10.1145/3464794.
  5. Heino Carstensen. Infinite behaviour if deterministic petri nets. In Michal Chytil, Ladislav Janiga, and Václav Koubek, editors, Mathematical Foundations of Computer Science 1988, MFCS'88, Carlsbad, Czechoslovakia, August 29 - September 2, 1988, Proceedings, volume 324 of Lecture Notes in Computer Science, pages 210-219. Springer, 1988. URL: https://doi.org/10.1007/BFb0017144.
  6. Pierre Chambart, Alain Finkel, and Sylvain Schmitz. Forward analysis and model checking for trace bounded WSTS. Theor. Comput. Sci., 637:1-29, 2016. URL: https://doi.org/10.1016/j.tcs.2016.04.020.
  7. Christian Choffrut, Flavio D'Alessandro, and Stefano Varricchio. On the separability of sparse context-free languages and of bounded rational relations. Theor. Comput. Sci., 381(1-3):274-279, 2007. URL: https://doi.org/10.1016/j.tcs.2007.04.003.
  8. Lorenzo Clemente, Wojciech Czerwinski, Slawomir Lasota, and Charles Paperman. Regular Separability of Parikh Automata. In Ioannis Chatzigiannakis, Piotr Indyk, Fabian Kuhn, and Anca Muscholl, editors, 44th International Colloquium on Automata, Languages, and Programming, ICALP 2017, July 10-14, 2017, Warsaw, Poland, volume 80 of LIPIcs, pages 117:1-117:13. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. URL: https://doi.org/10.4230/LIPIcs.ICALP.2017.117.
  9. Lorenzo Clemente, Wojciech Czerwinski, Slawomir Lasota, and Charles Paperman. Separability of Reachability Sets of Vector Addition Systems. In Heribert Vollmer and Brigitte Vallée, editors, 34th Symposium on Theoretical Aspects of Computer Science, STACS 2017, March 8-11, 2017, Hannover, Germany, volume 66 of LIPIcs, pages 24:1-24:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. URL: https://doi.org/10.4230/LIPIcs.STACS.2017.24.
  10. Lorenzo Clemente, Slawomir Lasota, and Radoslaw Piórkowski. Timed Games and Deterministic Separability. In Artur Czumaj, Anuj Dawar, and Emanuela Merelli, editors, 47th International Colloquium on Automata, Languages, and Programming, ICALP 2020, July 8-11, 2020, Saarbrücken, Germany (Virtual Conference), volume 168 of LIPIcs, pages 121:1-121:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. URL: https://doi.org/10.4230/LIPIcs.ICALP.2020.121.
  11. Wojciech Czerwiński, Piotr Hofman, and Georg Zetzsche. Unboundedness problems for languages of vector addition systems. In Ioannis Chatzigiannakis, Christos Kaklamanis, Dániel Marx, and Donald Sannella, editors, Proc. of the 45th International Colloquium on Automata, Languages, and Programming (ICALP 2018), volume 107 of Leibniz International Proceedings in Informatics (LIPIcs), pages 119:1-119:15, Dagstuhl, Germany, 2018. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. URL: https://doi.org/10.4230/LIPIcs.ICALP.2018.119.
  12. Wojciech Czerwinski and Slawomir Lasota. Regular separability of one counter automata. In 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017, pages 1-12. IEEE Computer Society, 2017. URL: https://doi.org/10.1109/LICS.2017.8005079.
  13. Wojciech Czerwinski, Slawomir Lasota, Roland Meyer, Sebastian Muskalla, K. Narayan Kumar, and Prakash Saivasan. Regular Separability of Well-Structured Transition Systems. In Sven Schewe and Lijun Zhang, editors, 29th International Conference on Concurrency Theory (CONCUR 2018), volume 118 of Leibniz International Proceedings in Informatics (LIPIcs), pages 35:1-35:18, Dagstuhl, Germany, 2018. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2018.35.
  14. Wojciech Czerwinski, Wim Martens, and Tomás Masopust. Efficient Separability of Regular Languages by Subsequences and Suffixes. In Fedor V. Fomin, Rusins Freivalds, Marta Z. Kwiatkowska, and David Peleg, editors, Automata, Languages, and Programming - 40th International Colloquium, ICALP 2013, Riga, Latvia, July 8-12, 2013, Proceedings, Part II, volume 7966 of Lecture Notes in Computer Science, pages 150-161. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-39212-2_16.
  15. Wojciech Czerwiński, Wim Martens, Lorijn van Rooijen, Marc Zeitoun, and Georg Zetzsche. A Characterization for Decidable Separability by Piecewise Testable Languages. Discrete Mathematics and Theoretical Computer Science, 19(4), 2017. URL: https://doi.org/10.23638/DMTCS-19-4-1.
  16. Wojciech Czerwiński and Georg Zetzsche. An Approach to Regular Separability in Vector Addition Systems. In Holger Hermanns, Lijun Zhang, Naoki Kobayashi, and Dale Miller, editors, Proc. of the Thirty-Fifth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2020), pages 341-354. ACM, 2020. URL: https://doi.org/10.1145/3373718.3394776.
  17. Stéphane Demri. On selective unboundedness of VASS. J. Comput. Syst. Sci., 79(5):689-713, 2013. URL: https://doi.org/10.1016/j.jcss.2013.01.014.
  18. Jacques Duparc, Olivier Finkel, and Jean-Pierre Ressayre. The wadge hierarchy of petri nets ω-languages. In Vasco Brattka, Hannes Diener, and Dieter Spreen, editors, Logic, Computation, Hierarchies, volume 4 of Ontos Mathematical Logic, pages 109-138. De Gruyter, 2014. URL: https://doi.org/10.1515/9781614518044.109.
  19. Javier Esparza. Decidability and complexity of Petri net problems - an introduction. In G. Rozenberg and W. Reisig, editors, Lectures on Petri Nets I: Basic Models. Advances in Petri Nets, number 1491 in Lecture Notes in Computer Science, pages 374-428, 1998. Google Scholar
  20. John Fearnley and Marcin Jurdzinski. Reachability in two-clock timed automata is PSPACE-complete. Inf. Comput., 243:26-36, 2015. URL: https://doi.org/10.1016/j.ic.2014.12.004.
  21. Olivier Finkel. Borel ranks and wadge degrees of context free omega-languages. Math. Struct. Comput. Sci., 16(5):813-840, 2006. URL: https://doi.org/10.1017/S0960129506005597.
  22. Olivier Finkel and Michal Skrzypczak. On the expressive power of non-deterministic and unambiguous petri nets over infinite words. Fundam. Informaticae, 183(3-4):243-291, 2021. URL: https://doi.org/10.3233/FI-2021-2088.
  23. Peter Habermehl. On the Complexity of the Linear-Time μ-calculus for Petri-Nets. In ICATPN, volume 1248 of LNCS, pages 102-116. Springer, 1997. Google Scholar
  24. Christopher Hugenroth. Separating Regular Languages over Infinite Words with Respect to the Wagner Hierarchy. In Mikolaj Bojanczyk and Chandra Chekuri, editors, 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2021, December 15-17, 2021, Virtual Conference, volume 213 of LIPIcs, pages 46:1-46:13. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2021.46.
  25. Harry B. Hunt III. On the Decidability of Grammar Problems. Journal of the ACM, 29(2):429-447, 1982. URL: https://doi.org/10.1145/322307.322317.
  26. Richard M. Karp and Raymond E. Miller. Parallel program schemata. Journal of Computer and System Sciences, 3(2):147-195, 1969. URL: https://doi.org/10.1016/S0022-0000(69)80011-5.
  27. Eryk Kopczynski. Invisible Pushdown Languages. In Martin Grohe, Eric Koskinen, and Natarajan Shankar, editors, Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16, New York, NY, USA, July 5-8, 2016, pages 867-872. ACM, 2016. URL: https://doi.org/10.1145/2933575.2933579.
  28. Jérôme Leroux and Sylvain Schmitz. Demystifying Reachability in Vector Addition Systems. In 30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2015, Kyoto, Japan, July 6-10, 2015, pages 56-67. IEEE Computer Society, 2015. URL: https://doi.org/10.1109/LICS.2015.16.
  29. Richard Lipton. The reachability problem is exponential-space hard. Yale University, Department of Computer Science, Report, 62, 1976. Google Scholar
  30. Tomás Masopust. Separability by piecewise testable languages is PTime-complete. Theor. Comput. Sci., 711:109-114, 2018. URL: https://doi.org/10.1016/j.tcs.2017.11.004.
  31. Ernst W Mayr and Albert R Meyer. The complexity of the finite containment problem for Petri nets. Journal of the ACM (JACM), 28(3):561-576, 1981. Google Scholar
  32. Théo Pierron, Thomas Place, and Marc Zeitoun. Quantifier Alternation for Infinite Words. In Bart Jacobs and Christof Löding, editors, Foundations of Software Science and Computation Structures - 19th International Conference, FOSSACS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings, volume 9634 of Lecture Notes in Computer Science, pages 234-251. Springer, 2016. URL: https://doi.org/10.1007/978-3-662-49630-5_14.
  33. Thomas Place, Lorijn van Rooijen, and Marc Zeitoun. Separating Regular Languages by Locally Testable and Locally Threshold Testable Languages. In Anil Seth and Nisheeth K. Vishnoi, editors, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2013, December 12-14, 2013, Guwahati, India, volume 24 of LIPIcs, pages 363-375. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2013. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2013.363.
  34. Thomas Place and Marc Zeitoun. Separating regular languages with first-order logic. In Thomas A. Henzinger and Dale Miller, editors, Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS '14, Vienna, Austria, July 14-18, 2014, pages 75:1-75:10. ACM, 2014. URL: https://doi.org/10.1145/2603088.2603098.
  35. Thomas Place and Marc Zeitoun. Separation and the Successor Relation. In Ernst W. Mayr and Nicolas Ollinger, editors, 32nd International Symposium on Theoretical Aspects of Computer Science, STACS 2015, March 4-7, 2015, Garching, Germany, volume 30 of LIPIcs, pages 662-675. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015. URL: https://doi.org/10.4230/LIPIcs.STACS.2015.662.
  36. Thomas Place and Marc Zeitoun. Separating Regular Languages with First-Order Logic. Log. Methods Comput. Sci., 12(1), 2016. URL: https://doi.org/10.2168/LMCS-12(1:5)2016.
  37. Thomas Place and Marc Zeitoun. Separating Without Any Ambiguity. In Ioannis Chatzigiannakis, Christos Kaklamanis, Dániel Marx, and Donald Sannella, editors, 45th International Colloquium on Automata, Languages, and Programming, ICALP 2018, July 9-13, 2018, Prague, Czech Republic, volume 107 of LIPIcs, pages 137:1-137:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. URL: https://doi.org/10.4230/LIPIcs.ICALP.2018.137.
  38. Thomas Place and Marc Zeitoun. Separation and covering for group based concatenation hierarchies. In 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019, Vancouver, BC, Canada, June 24-27, 2019, pages 1-13. IEEE, 2019. URL: https://doi.org/10.1109/LICS.2019.8785655.
  39. Andreas Podelski and Andrey Rybalchenko. A Complete Method for the Synthesis of Linear Ranking Functions. In VMCAI, volume 2937 of LNCS, pages 239-251. Springer, 2004. Google Scholar
  40. Alexander Schrijver. Theory of Linear and Integer Programming. John Wiley & Sons, Inc., New York, NY, USA, 1986. Google Scholar
  41. Thomas G. Szymanski and John H. Williams. Noncanonical extensions of bottom-up parsing techniques. SIAM Journal on Computing, 5(2), 1976. Google Scholar
  42. Ramanathan S. Thinniyam and Georg Zetzsche. Regular Separability and Intersection Emptiness are Independent Problems. In Proc. of the 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019), volume 150 of LIPIcs, Dagstuhl, Germany, 2019. Schloss Dagstuhl-Leibniz-Zentrum für Informatik. Google Scholar
  43. Rüdiger Valk. Infinite behaviour of petri nets. Theoretical computer science, 25(3):311-341, 1983. Google Scholar
  44. Georg Zetzsche. Separability by piecewise testable languages and downward closures beyond subwords. In Anuj Dawar and Erich Grädel, editors, Proc. of the Thirty-Third Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2018), pages 929-938. ACM, 2018. URL: https://doi.org/10.1145/3209108.3209201.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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