Document Open Access Logo

The Complexity of Separability for Semilinear Sets and Parikh Automata

Authors Elias Rojas Collins , Chris Köcher , Georg Zetzsche

PDF

File

Thumbnail PDF
PDF
LIPIcs.MFCS.2025.38.pdf
  • Filesize: 0.89 MB
  • 21 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Models of computation
  • Theory of computation → Regular languages
Keywords
  • Vector Addition System
  • Separability
  • Regular Language

Metrics

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

Abstract

In a separability problem, we are given two sets K and L from a class 𝒞, and we want to decide whether there exists a set S from a class 𝒮 such that K ⊆ S and S ∩ L = ∅. In this case, we speak of separability of sets in 𝒞 by sets in 𝒮.
We study two types of separability problems. First, we consider separability of semilinear sets (i.e. subsets of ℕ^d for some d) by sets definable by quantifier-free monadic Presburger formulas (or equivalently, the recognizable subsets of ℕ^d). Here, a formula is monadic if each atom uses at most one variable. Second, we consider separability of languages of Parikh automata by regular languages. A Parikh automaton is a machine with access to counters that can only be incremented, and have to meet a semilinear constraint at the end of the run. Both of these separability problems are known to be decidable with elementary complexity.
Our main results are that both problems are coNP-complete. In the case of semilinear sets, coNP-completeness holds regardless of whether the input sets are specified by existential Presburger formulas, quantifier-free formulas, or semilinear representations. Our results imply that recognizable separability of rational subsets of Σ* × ℕ^d (shown decidable by Choffrut and Grigorieff) is coNP-complete as well. Another application is that regularity of deterministic Parikh automata (where the target set is specified using a quantifier-free Presburger formula) is coNP-complete as well.

Cite As Get BibTex

Elias Rojas Collins, Chris Köcher, and Georg Zetzsche. The Complexity of Separability for Semilinear Sets and Parikh Automata. In 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 345, pp. 38:1-38:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.MFCS.2025.38

Author Details

Elias Rojas Collins
  • Massachusetts Institute of Technology, Cambridge, MA, USA
Chris Köcher
  • Max Planck Institute for Software Systems, Kaiserslautern, Germany
Georg Zetzsche
  • Max Planck Institute for Software Systems, 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.

References

  1. Pascal Baumann, Flavio D'Alessandro, Moses Ganardi, Oscar Ibarra, Ian McQuillan, Lia Schütze, and Georg Zetzsche. Unboundedness problems for machines with reversal-bounded counters. In Orna Kupferman and Pawel Sobocinski, editors, Foundations of Software Science and Computation Structures, pages 240-264, Cham, 2023. Springer Nature Switzerland. URL: https://doi.org/10.1007/978-3-031-30829-1_12.
  2. Pascal Baumann, Eren Keskin, Roland Meyer, and Georg Zetzsche. Separability in Büchi VASS and singly non-linear systems of inequalities. In Karl Bringmann, Martin Grohe, Gabriele Puppis, and Ola Svensson, editors, 51st International Colloquium on Automata, Languages, and Programming, ICALP 2024, July 8-12, 2024, Tallinn, Estonia, volume 297 of LIPIcs, pages 126:1-126:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024. URL: https://doi.org/10.4230/LIPICS.ICALP.2024.126.
  3. Pascal Baumann, Roland Meyer, and Georg Zetzsche. Regular separability in Büchi VASS. In Petra Berenbrink, Patricia Bouyer, Anuj Dawar, and Mamadou Moustapha Kanté, editors, 40th International Symposium on Theoretical Aspects of Computer Science, STACS 2023, March 7-9, 2023, Hamburg, Germany, volume 254 of LIPIcs, pages 9:1-9:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPICS.STACS.2023.9.
  4. Pascal Bergsträßer, Moses Ganardi, Anthony W. Lin, and Georg Zetzsche. Ramsey quantifiers in linear arithmetics. Proc. ACM Program. Lang., 8(POPL):1-32, 2024. URL: https://doi.org/10.1145/3632843.
  5. Marcello M. Bersani and Stéphane Demri. The complexity of reversal-bounded model-checking. In Cesare Tinelli and Viorica Sofronie-Stokkermans, editors, Frontiers of Combining Systems, 8th International Symposium, FroCoS 2011, Saarbrücken, Germany, October 5-7, 2011. Proceedings, volume 6989 of Lecture Notes in Computer Science, pages 71-86. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-24364-6_6.
  6. Jean Berstel. Transductions and Context-Free Languages. Teubner, 1979. URL: https://doi.org/10.1007/978-3-663-09367-1.
  7. Alin Bostan, Arnaud Carayol, Florent Koechlin, and Cyril Nicaud. Weakly-unambiguous Parikh automata and their link to holonomic series. 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 114:1-114:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. URL: https://doi.org/10.4230/LIPICS.ICALP.2020.114.
  8. Ahmed Bouajjani and Peter Habermehl. Symbolic reachability analysis of FIFO-channel systems with nonregular sets of configurations. Theor. Comput. Sci., 221(1-2):211-250, 1999. URL: https://doi.org/10.1016/S0304-3975(99)00033-X.
  9. Michaël Cadilhac, Alain Finkel, and Pierre McKenzie. Affine Parikh automata. RAIRO Theor. Informatics Appl., 46(4):511-545, 2012. URL: https://doi.org/10.1051/ITA/2012013.
  10. Michaël Cadilhac, Alain Finkel, and Pierre McKenzie. Unambiguous constrained automata. Int. J. Found. Comput. Sci., 24(7):1099-1116, 2013. URL: https://doi.org/10.1142/S0129054113400339.
  11. Michaël Cadilhac, Arka Ghosh, Guillermo A. Pérez, and Ritam Raha. Parikh one-counter automata. In Jérôme Leroux, Sylvain Lombardy, and David Peleg, editors, 48th International Symposium on Mathematical Foundations of Computer Science, MFCS 2023, August 28 to September 1, 2023, Bordeaux, France, volume 272 of LIPIcs, pages 30:1-30:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPICS.MFCS.2023.30.
  12. Michaël Cadilhac, Andreas Krebs, and Pierre McKenzie. The algebraic theory of Parikh automata. Theory Comput. Syst., 62(5):1241-1268, 2018. URL: https://doi.org/10.1007/S00224-017-9817-2.
  13. Dmitry Chistikov, Christoph Haase, and Alessio Mansutti. Quantifier elimination for counting extensions of presburger arithmetic. In Patricia Bouyer and Lutz Schröder, editors, Foundations of Software Science and Computation Structures - 25th International Conference, FOSSACS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, volume 13242 of Lecture Notes in Computer Science, pages 225-243. Springer, 2022. URL: https://doi.org/10.1007/978-3-030-99253-8_12.
  14. Christian Choffrut and Serge Grigorieff. Separability of rational relations in A^∗ × ℕ^m by recognizable relations is decidable. Information Processing Letters, 99(1):27-32, 2006. URL: https://doi.org/10.1016/j.ipl.2005.09.018.
  15. Lorenzo Clemente, Wojciech Czerwiński, 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), volume 80 of Leibniz International Proceedings in Informatics (LIPIcs), pages 117:1-117:13, Dagstuhl, Germany, 2017. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.ICALP.2017.117.
  16. Lorenzo Clemente, Wojciech Czerwiński, 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.
  17. Wojciech Czerwiński 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.
  18. Wojciech Czerwiński, 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, September 4-7, 2018, Beijing, China, volume 118 of LIPIcs, pages 35:1-35:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. URL: https://doi.org/10.4230/LIPICS.CONCUR.2018.35.
  19. Wojciech Czerwiński and Georg Zetzsche. An approach to regular separability in vector addition systems. In Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '20, pages 341-354, New York, NY, USA, 2020. Association for Computing Machinery. URL: https://doi.org/10.1145/3373718.3394776.
  20. Enzo Erlich, Shibashis Guha, Ismaël Jecker, Karoliina Lehtinen, and Martin Zimmermann. History-deterministic Parikh automata. In Guillermo A. Pérez and Jean-François Raskin, editors, 34th International Conference on Concurrency Theory, CONCUR 2023, September 18-23, 2023, Antwerp, Belgium, volume 279 of LIPIcs, pages 31:1-31:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPICS.CONCUR.2023.31.
  21. Javier Esparza. Petri nets, commutative context-free grammars, and basic parallel processes. Fundam. Informaticae, 31(1):13-25, 1997. URL: https://doi.org/10.3233/FI-1997-3112.
  22. Emmanuel Filiot, Shibashis Guha, and Nicolas Mazzocchi. Two-way Parikh automata. In Arkadev Chattopadhyay and Paul Gastin, editors, 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2019, December 11-13, 2019, Bombay, India, volume 150 of LIPIcs, pages 40:1-40:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. URL: https://doi.org/10.4230/LIPICS.FSTTCS.2019.40.
  23. Alain Finkel and Arnaud Sangnier. Reversal-bounded counter machines revisited. In Edward Ochmanski and Jerzy Tyszkiewicz, editors, Mathematical Foundations of Computer Science 2008, 33rd International Symposium, MFCS 2008, Torun, Poland, August 25-29, 2008, Proceedings, volume 5162 of Lecture Notes in Computer Science, pages 323-334. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-85238-4_26.
  24. Seymour Ginsburg and Edwin H. Spanier. Bounded regular sets. Proceedings of the American Mathematical Society, 17(5):1043-1049, 1966. URL: https://doi.org/10.1090/S0002-9939-1966-0201310-3.
  25. Seymour Ginsburg and Edwin H. Spanier. Semigroups, Presburger formulas, and languages. Pacific Journal of Mathematics, 16(2):285-296, February 1966. Google Scholar
  26. Sheila A. Greibach. Remarks on blind and partially blind one-way multicounter machines. Theoretical Computer Science, 7(3):311-324, 1978. URL: https://doi.org/10.1016/0304-3975(78)90020-8.
  27. Mario Grobler, Leif Sabellek, and Sebastian Siebertz. Remarks on Parikh-recognizable omega-languages. In Aniello Murano and Alexandra Silva, editors, 32nd EACSL Annual Conference on Computer Science Logic, CSL 2024, February 19-23, 2024, Naples, Italy, volume 288 of LIPIcs, pages 31:1-31:21. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024. URL: https://doi.org/10.4230/LIPICS.CSL.2024.31.
  28. Stéphane Grumbach, Philippe Rigaux, and Luc Segoufin. Spatio-temporal data handling with constraints. In Robert Laurini, Kia Makki, and Niki Pissinou, editors, ACM-GIS '98, Proceedings of the 6th international symposium on Advances in Geographic Information Systems, November 6-7, 1998, Washington, DC, USA, pages 106-111. ACM, 1998. URL: https://doi.org/10.1145/288692.288712.
  29. Shibashis Guha, Ismaël Jecker, Karoliina Lehtinen, and Martin Zimmermann. Parikh automata over infinite words. In Anuj Dawar and Venkatesan Guruswami, editors, 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2022, December 18-20, 2022, IIT Madras, Chennai, India, volume 250 of LIPIcs, pages 40:1-40:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPICS.FSTTCS.2022.40.
  30. Christoph Haase and Simon Halfon. Integer vector addition systems with states. In Joël Ouaknine, Igor Potapov, and James Worrell, editors, Reachability Problems - 8th International Workshop, RP 2014, Oxford, UK, September 22-24, 2014. Proceedings, volume 8762 of Lecture Notes in Computer Science, pages 112-124. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-11439-2_9.
  31. Christoph Haase, Shankara Narayanan Krishna, Khushraj Madnani, Om Swostik Mishra, and Georg Zetzsche. An efficient quantifier elimination procedure for Presburger arithmetic. In Karl Bringmann, Martin Grohe, Gabriele Puppis, and Ola Svensson, editors, 51st International Colloquium on Automata, Languages, and Programming, ICALP 2024, July 8-12, 2024, Tallinn, Estonia, volume 297 of LIPIcs, pages 142:1-142:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024. URL: https://doi.org/10.4230/LIPICS.ICALP.2024.142.
  32. Matthew Hague, Anthony W. Lin, Philipp Rümmer, and Zhilin Wu. Monadic decomposition in integer linear arithmetic. In Nicolas Peltier and Viorica Sofronie-Stokkermans, editors, Automated Reasoning - 10th International Joint Conference, IJCAR 2020, Paris, France, July 1-4, 2020, Proceedings, Part I, volume 12166 of Lecture Notes in Computer Science, pages 122-140. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-51074-9_8.
  33. Simon Halfon, Philippe Schnoebelen, and Georg Zetzsche. Decidability, complexity, and expressiveness of first-order logic over the subword ordering. 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.8005141.
  34. 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.
  35. Oscar H Ibarra. Reversal-bounded multicounter machines and their decision problems. Journal of the ACM (JACM), 25(1):116-133, 1978. URL: https://doi.org/10.1145/322047.322058.
  36. Oscar H. Ibarra and Bala Ravikumar. On the Parikh Membership Problem for FAs, PDAs, and CMs. In Adrian-Horia Dediu, Carlos Martín-Vide, José-Luis Sierra-Rodríguez, and Bianca Truthe, editors, Language and Automata Theory and Applications, pages 14-31, Cham, 2014. Springer International Publishing. URL: https://doi.org/10.1007/978-3-319-04921-2_2.
  37. Matthias Jantzen and Alexy Kurganskyy. Refining the hierarchy of blind multicounter languages and twist-closed trios. Inf. Comput., 185(2):159-181, 2003. URL: https://doi.org/10.1016/S0890-5401(03)00087-7.
  38. Eren Keskin and Roland Meyer. Separability and non-determinizability of WSTS. In Guillermo A. Pérez and Jean-François Raskin, editors, 34th International Conference on Concurrency Theory, CONCUR 2023, September 18-23, 2023, Antwerp, Belgium, volume 279 of LIPIcs, pages 8:1-8:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPICS.CONCUR.2023.8.
  39. Eren Keskin and Roland Meyer. On the separability problem of VASS reachability languages. In Pawel Sobocinski, Ugo Dal Lago, and Javier Esparza, editors, Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2024, Tallinn, Estonia, July 8-11, 2024, pages 49:1-49:14. ACM, 2024. URL: https://doi.org/10.1145/3661814.3662116.
  40. Felix Klaedtke and Harald Rueß. Monadic second-order logics with cardinalities. In Jos C. M. Baeten, Jan Karel Lenstra, Joachim Parrow, and Gerhard J. Woeginger, editors, Automata, Languages and Programming, 30th International Colloquium, ICALP 2003, Eindhoven, The Netherlands, June 30 - July 4, 2003. Proceedings, volume 2719 of Lecture Notes in Computer Science, pages 681-696. Springer, 2003. URL: https://doi.org/10.1007/3-540-45061-0_54.
  41. Chris Köcher and Georg Zetzsche. Regular separators for VASS coverability languages. In Patricia Bouyer and Srikanth Srinivasan, editors, 43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2023, December 18-20, 2023, IIIT Hyderabad, Telangana, India, volume 284 of LIPIcs, pages 15:1-15:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPICS.FSTTCS.2023.15.
  42. Gabriel Kuper, Leonid Libkin, and Jan Paredaens. Constraint databases. Springer Science & Business Media, 2013. URL: https://doi.org/10.1007/978-3-662-04031-7.
  43. Kenneth L. McMillan. Interpolation and SAT-based model checking. In Warren A. Hunt Jr. and Fabio Somenzi, editors, Computer Aided Verification, 15th International Conference, CAV 2003, Boulder, CO, USA, July 8-12, 2003, Proceedings, volume 2725 of Lecture Notes in Computer Science, pages 1-13. Springer, 2003. URL: https://doi.org/10.1007/978-3-540-45069-6_1.
  44. Jacques Sakarovitch. Elements of Automata Theory. Cambridge University Press, Cambridge, 2009. URL: https://doi.org/10.1017/CBO9781139195218.
  45. Helmut Seidl, Thomas Schwentick, Anca Muscholl, and Peter Habermehl. Counting in trees for free. In Josep Díaz, Juhani Karhumäki, Arto Lepistö, and Donald Sannella, editors, Automata, Languages and Programming: 31st International Colloquium, ICALP 2004, Turku, Finland, July 12-16, 2004. Proceedings, volume 3142 of Lecture Notes in Computer Science, pages 1136-1149. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-27836-8_94.
  46. Yousef Shakiba, Henry Sinclair-Banks, and Georg Zetzsche. A complexity dichotomy for semilinear target sets in automata with one counter, 2025. To appear in Proc. of LICS 2025. URL: https://doi.org/10.48550/arXiv.2505.13749.
  47. Thomas G. Szymanski and John H. Williams. Noncanonical extensions of bottom-up parsing techniques. SIAM Journal on Computing, 5(2), 1976. URL: https://doi.org/10.1137/0205019.
  48. Ramanathan S. Thinniyam and Georg Zetzsche. Regular separability and intersection emptiness are independent problems. In Arkadev Chattopadhyay and Paul Gastin, editors, 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2019, December 11-13, 2019, Bombay, India, volume 150 of LIPIcs, pages 51:1-51:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. URL: https://doi.org/10.4230/LIPICS.FSTTCS.2019.51.
  49. Margus Veanes, Nikolaj S. Bjørner, Lev Nachmanson, and Sergey Bereg. Monadic decomposition. J. ACM, 64(2):14:1-14:28, 2017. URL: https://doi.org/10.1145/3040488.
  50. Yakir Vizel, Georg Weissenbacher, and Sharad Malik. Boolean satisfiability solvers and their applications in model checking. Proc. IEEE, 103(11):2021-2035, 2015. URL: https://doi.org/10.1109/JPROC.2015.2455034.
  51. Georg Zetzsche. Silent transitions in automata with storage. 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 434-445. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-39212-2_39.
  52. Georg Zetzsche. The complexity of downward closure comparisons. In Ioannis Chatzigiannakis, Michael Mitzenmacher, Yuval Rabani, and Davide Sangiorgi, editors, 43rd International Colloquium on Automata, Languages, and Programming, ICALP 2016, July 11-15, 2016, Rome, Italy, volume 55 of LIPIcs, pages 123:1-123:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. URL: https://doi.org/10.4230/LIPICS.ICALP.2016.123.
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact