Document Open Access Logo

Language Inclusion for Boundedly-Ambiguous Vector Addition Systems Is Decidable

Authors Wojciech Czerwiński , Piotr Hofman

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2022.16.pdf
  • Filesize: 0.77 MB
  • 22 pages

Document Identifiers

Author Details

Wojciech Czerwiński
  • University of Warsaw, Poland
Piotr Hofman
  • University of Warsaw, Poland

Funding

  • Czerwiński, Wojciech: Supported by the ERC grant INFSYS, agreement no. 950398.
  • Hofman, Piotr: Supported by the ERC grant INFSYS, agreement no. 950398.

Acknowledgements

We thank Filip Mazowiecki for asking the question for boundedly-ambiguous VASSes and formulating the conjecture that control automata of boundedly-ambiguous VASSes can be made boundedly-ambiguous. We also thank him and David Purser for inspiring discussions on the problem. We thank Thomas Colcombet for suggesting the way of proving Theorem 25, Mahsa Shirmohammadi for pointing us to the undecidability result [Petr Jancar, 2001] and Lorenzo Clemente for inspiring discussions on weighted models.

Cite As Get BibTex

Wojciech Czerwiński and Piotr Hofman. Language Inclusion for Boundedly-Ambiguous Vector Addition Systems Is Decidable. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 16:1-16:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022) https://doi.org/10.4230/LIPIcs.CONCUR.2022.16

Abstract

We consider the problems of language inclusion and language equivalence for Vector Addition Systems with States (VASSes) with the acceptance condition defined by the set of accepting states (and more generally by some upward-closed conditions). In general the problem of language equivalence is undecidable even for one-dimensional VASSes, thus to get decidability we investigate restricted subclasses. On one hand we show that the problem of language inclusion of a VASS in k-ambiguous VASS (for any natural k) is decidable and even in Ackermann. On the other hand we prove that the language equivalence problem is Ackermann-hard already for deterministic VASSes. These two results imply Ackermann-completeness for language inclusion and equivalence in several possible restrictions. Some of our techniques can be also applied in much broader generality in infinite-state systems, namely for some subclass of well-structured transition systems.

Subject Classification

ACM Subject Classification
  • Theory of computation → Parallel computing models
Keywords
  • vector addition systems
  • language inclusion
  • language equivalence
  • determinism
  • unambiguity
  • bounded ambiguity
  • Petri nets
  • well-structured transition systems

Metrics

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

Related Versions

References

  1. Toshiro Araki and Tadao Kasami. Some decision problems related to the reachability problem for Petri nets. Theor. Comput. Sci., 3(1):85-104, 1976. Google Scholar
  2. Corentin Barloy and Lorenzo Clemente. Bidimensional linear recursive sequences and universality of unambiguous register automata. In Proceedings of STACS 2021), volume 187 of LIPIcs, pages 8:1-8:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. Google Scholar
  3. Mikolaj Bojanczyk, Bartek Klin, and Joshua Moerman. Orbit-finite-dimensional vector spaces and weighted register automata. In Proceedings of LICS 2021, pages 1-13. IEEE, 2021. Google Scholar
  4. Rémi Bonnet. The reachability problem for vector addition system with one zero-test. In Proceedings of MFCS 2011, volume 6907 of Lecture Notes in Computer Science, pages 145-157. Springer, 2011. Google Scholar
  5. 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.
  6. Thomas Colcombet. Unambiguity in automata theory. In Proceedings of DCFS 2015, pages 3-18, 2015. Google Scholar
  7. Wojciech Czerwinski, Diego Figueira, and Piotr Hofman. Universality problem for unambiguous VASS. In Proceedings of CONCUR 2020, pages 36:1-36:15, 2020. Google Scholar
  8. Wojciech Czerwinski and Piotr Hofman. Language inclusion for boundedly-ambiguous vector addition systems is decidable. CoRR, abs/2202.08033, 2022. URL: http://arxiv.org/abs/2202.08033.
  9. Wojciech Czerwinski, Slawomir Lasota, Roland Meyer, Sebastian Muskalla, K. Narayan Kumar, and Prakash Saivasan. Regular separability of well-structured transition systems. In Proceedings of CONCUR 2018, volume 118 of LIPIcs, pages 35:1-35:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. Google Scholar
  10. Wojciech Czerwinski, Antoine Mottet, and Karin Quaas. New techniques for universality in unambiguous register automata. In Proceedings of ICALP 2021, volume 198 of LIPIcs, pages 129:1-129:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. Google Scholar
  11. Wojciech Czerwinski and Lukasz Orlikowski. Reachability in vector addition systems is Ackermann-complete. In Proceedings of FOCS 2021, pages 1229-1240, 2021. Google Scholar
  12. Stéphane Demri and Ranko Lazic. LTL with the freeze quantifier and register automata. ACM Trans. Comput. Log., 10(3):16:1-16:30, 2009. Google Scholar
  13. L.E. Dickson. Finiteness of the odd perfect and primitive abundant numbers with n distinct prime factors. American Journal of Mathematics, 35((4)):413-422, 1913. Google Scholar
  14. Alain Finkel and Philippe Schnoebelen. Well-structured transition systems everywhere! Theor. Comput. Sci., 256(1-2):63-92, 2001. Google Scholar
  15. Jean Goubault-Larrecq, Simon Halfon, Prateek Karandikar, K. Narayan Kumar, and Philippe Schnoebelen. The Ideal Approach to Computing Closed Subsets in Well-Quasi-orderings, pages 55-105. Springer International Publishing, Cham, 2020. Google Scholar
  16. Michel Hack. The equality problem for vector addition systems is undecidable. Theor. Comput. Sci., 2(1):77-95, 1976. Google Scholar
  17. Piotr Hofman, Richard Mayr, and Patrick Totzke. Decidability of weak simulation on one-counter nets. In Proceedings of LICS 2013, pages 203-212. IEEE Computer Society, 2013. Google Scholar
  18. Piotr Hofman and Patrick Totzke. Trace inclusion for one-counter nets revisited. In Proceedings of RP 2014, volume 8762 of Lecture Notes in Computer Science, pages 151-162. Springer, 2014. Google Scholar
  19. Petr Jancar. Undecidability of bisimilarity for Petri nets and some related problems. Theor. Comput. Sci., 148(2):281-301, 1995. Google Scholar
  20. Petr Jancar. Nonprimitive recursive complexity and undecidability for petri net equivalences. Theor. Comput. Sci., 256(1-2):23-30, 2001. Google Scholar
  21. M. Kabil and M. Pouzet. Une extension d'un théorème de P. Jullien sur les âges de mots. RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, 26(5):449-482, 1992. Google Scholar
  22. Ranko Lazic and Sylvain Schmitz. The ideal view on Rackoff’s coverability technique. Inf. Comput., 277:104582, 2021. URL: https://doi.org/10.1016/j.ic.2020.104582.
  23. Jérôme Leroux. The reachability problem for petri nets is not primitive recursive. In Proceedings of FOCS 2021, pages 1241-1252, 2021. Google Scholar
  24. Jérôme Leroux and Sylvain Schmitz. Reachability in vector addition systems is primitive-recursive in fixed dimension. In Proceedings of LICS 2019, pages 1-13. IEEE, 2019. Google Scholar
  25. Ernst W. Mayr. An algorithm for the general Petri net reachability problem. In Proceedings of STOC 1981, pages 238-246, 1981. Google Scholar
  26. Antoine Mottet and Karin Quaas. The containment problem for unambiguous register automata. In Proceedings of STACS 2019, pages 53:1-53:15, 2019. Google Scholar
  27. Frank Neven, Thomas Schwentick, and Victor Vianu. Finite state machines for strings over infinite alphabets. ACM Trans. Comput. Log., 5(3):403-435, 2004. Google Scholar
  28. Jean-Eric Pin. Syntactic semigroups. In Grzegorz Rozenberg and Arto Salomaa, editors, Handbook of Formal Languages, Volume 1: Word, Language, Grammar, pages 679-746. Springer, 1997. Google Scholar
  29. Charles Rackoff. The covering and boundedness problems for vector addition systems. Theor. Comput. Sci., 6:223-231, 1978. Google Scholar
  30. Klaus Reinhardt. Reachability in Petri nets with inhibitor arcs. Electron. Notes Theor. Comput. Sci., 223:239-264, 2008. Google Scholar
  31. Marcel Paul Schützenberger. On the definition of a family of automata. Inf. Control., 4(2-3):245-270, 1961. Google Scholar
  32. Wen-Guey Tzeng. On path equivalence of nondeterministic finite automata. Inf. Process. Lett., 58(1):43-46, 1996. Google Scholar
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 About DROPS Imprint Privacy Contact