Document Open Access Logo

History-Deterministic Vector Addition Systems

Authors Sougata Bose , David Purser , Patrick Totzke

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2023.18.pdf
  • Filesize: 0.94 MB
  • 17 pages

Document Identifiers

Author Details

Sougata Bose
  • University of Liverpool, UK
David Purser
  • University of Liverpool, UK
Patrick Totzke
  • University of Liverpool, UK

Funding

We gratefully acknowledge support from the EPSRC, project number EP/V025848/1 and the Royal Society, IES\R3\203109.

Acknowledgements

The authors thank Ismaël Jecker, Piotr Hofman and Filip Mazowiecki for fruitful discussions.

Cite AsGet BibTex

Sougata Bose, David Purser, and Patrick Totzke. History-Deterministic Vector Addition Systems. In 34th International Conference on Concurrency Theory (CONCUR 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 279, pp. 18:1-18:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.CONCUR.2023.18

Abstract

We consider history-determinism, a restricted form of non-determinism, for Vector Addition Systems with States (VASS) when used as acceptors to recognise languages of finite words. History-determinism requires that the non-deterministic choices can be resolved on-the-fly; based on the past and without jeopardising acceptance of any possible continuation of the input word. Our results show that the history-deterministic (HD) VASS sit strictly between deterministic and non-deterministic VASS regardless of the number of counters. We compare the relative expressiveness of HD systems, and closure-properties of the induced language classes, with coverability and reachability semantics, and with and without ε-labelled transitions. Whereas in dimension 1, inclusion and regularity remain decidable, from dimension two onwards, HD-VASS with suitable resolver strategies, are essentially able to simulate 2-counter Minsky machines, leading to several undecidability results: It is undecidable whether a VASS is history-deterministic, or if a language equivalent history-deterministic VASS exists. Checking language inclusion between history-deterministic 2-VASS is also undecidable.

Subject Classification

ACM Subject Classification
  • Theory of computation → Formal languages and automata theory
Keywords
  • Vector Addition Systems
  • History-determinism
  • Good-for Games

Metrics

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

Related Versions

References

  1. Stanislav Böhm, Stefan Göller, Simon Halfon, and Piotr Hofman. On büchi one-counter automata. In International Symposium on Theoretical Aspects of Computer Science, volume 66 of LIPIcs, pages 14:1-14:13. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. URL: https://doi.org/10.4230/LIPIcs.STACS.2017.14.
  2. Stanislav Böhm, Stefan Göller, and Petr Jancar. Bisimulation equivalence and regularity for real-time one-counter automata. Journal of Computer and System Sciences, 80(4):720-743, 2014. URL: https://doi.org/10.1016/j.jcss.2013.11.003.
  3. Udi Boker and Karoliina Lehtinen. Good for games automata: From nondeterminism to alternation. In International Conference on Concurrency Theory, volume 140 of LIPIcs, pages 19:1-19:16, 2019. Google Scholar
  4. Udi Boker and Karoliina Lehtinen. History Determinism vs. Good for Gameness in Quantitative Automata. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, volume 213 of Leibniz International Proceedings in Informatics (LIPIcs), pages 38:1-38:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2021.38.
  5. Udi Boker and Karoliina Lehtinen. Token games and history-deterministic quantitative automata. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, pages 120-139. Springer International Publishing, 2022. Google Scholar
  6. Sougata Bose, Thomas A. Henzinger, Karoliina Lehtinen, Sven Schewe, and Patrick Totzke. History-deterministic timed automata are not determinizable. In International Workshop on Reachability Problems, 2022. Google Scholar
  7. Sougata Bose, David Purser, and Patrick Totzke. History-deterministic vector addition systems. CoRR, abs/2305.01981, 2023. URL: https://doi.org/10.48550/arXiv.2305.01981.
  8. Thomas Colcombet. The theory of stabilisation monoids and regular cost functions. In International Colloquium on Automata, Languages and Programming, pages 139-150, 2009. Google Scholar
  9. Wojciech Czerwinski and Piotr Hofman. Language inclusion for boundedly-ambiguous vector addition systems is decidable. In International Conference on Concurrency Theory, volume 243 of LIPIcs, pages 16:1-16:22. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2022.16.
  10. Wojciech Czerwinski and Lukasz Orlikowski. Reachability in vector addition systems is ackermann-complete. In Annual Symposium on Foundations of Computer Science, pages 1229-1240. IEEE, 2021. URL: https://doi.org/10.1109/FOCS52979.2021.00120.
  11. Enzo Erlich, Shibashis Guha, Ismaël Jecker, Karoliina Lehtinen, and Martin Zimmermann. History-deterministic parikh automata. In International Conference on Concurrency Theory, LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. Google Scholar
  12. Olivier Finkel and Michal Skrzypczak. On the topological complexity of ω-languages of non-deterministic Petri nets. Information Processing Letters, 114(5):229-233, 2014. URL: https://doi.org/10.1016/j.ipl.2013.12.007.
  13. Sheila A. Greibach. Remarks on blind and partially blind one-way multicounter machines. Theoretical Computer Science, 7:311-324, 1978. URL: https://doi.org/10.1016/0304-3975(78)90020-8.
  14. Shibashis Guha, Ismaël Jecker, Karoliina Lehtinen, and Martin Zimmermann. A Bit of Nondeterminism Makes Pushdown Automata Expressive and Succinct. In International Symposium on Mathematical Foundations of Computer Science, volume 202 of Leibniz International Proceedings in Informatics (LIPIcs), pages 53:1-53:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.MFCS.2021.53.
  15. Michel Henri Theódore Hack. Petri net language, 1976. Google Scholar
  16. Thomas A. Henzinger, Karoliina Lehtinen, and Patrick Totzke. History-deterministic timed automata. In International Conference on Concurrency Theory, 2022. Google Scholar
  17. Thomas A. Henzinger and Nir Piterman. Solving games without determinization. In EACSL Annual Conference on Computer Science Logic, pages 395-410. Springer Berlin Heidelberg, 2006. Google Scholar
  18. Piotr Hofman, Slawomir Lasota, Richard Mayr, and Patrick Totzke. Simulation problems over one-counter nets. Logical Methods in Computer Science, 12(1), 2016. URL: https://doi.org/10.2168/LMCS-12(1:6)2016.
  19. Piotr Hofman and Patrick Totzke. Trace inclusion for one-counter nets revisited. Theoretical Computer Science, 11174, 2017. URL: https://doi.org/10.1016/j.tcs.2017.05.009.
  20. Petr Jancar. Nonprimitive recursive complexity and undecidability for Petri net equivalences. Theoretical Computer Science, 256(1-2):23-30, 2001. URL: https://doi.org/10.1016/S0304-3975(00)00100-6.
  21. Petr Jancar, Javier Esparza, and Faron Moller. Petri nets and regular processes. Journal of Computer and System Sciences, 59(3):476-503, 1999. URL: https://doi.org/10.1006/jcss.1999.1643.
  22. Matthias Jantzen. Language theory of Petri nets. In Petri Nets: Central Models and Their Properties, Advances in Petri Nets 1986, Part I, Proceedings of an Advanced Course, Bad Honnef, Germany, 8-19 September 1986, volume 254 of LNCS, pages 397-412. Springer, 1986. URL: https://doi.org/10.1007/BFb0046847.
  23. Petr Jančar and Faron Moller. Checking regular properties of Petri nets. In International Conference on Concurrency Theory, pages 348-362, 1995. Google Scholar
  24. 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.
  25. S. Rao Kosaraju. Decidability of reachability in vector addition systems. In STOC'82, pages 267-281, 1982. URL: https://doi.org/10.1145/800070.802201.
  26. Orna Kupferman, Shmuel Safra, and Moshe Y Vardi. Relating word and tree automata. Annals of Pure and Applied Logic, 138(1-3):126-146, 2006. Google Scholar
  27. Karoliina Lehtinen and Martin Zimmermann. Good-for-games ω-pushdown automata. Logical Methods in Computer Science, 18, 2022. Google Scholar
  28. Jérôme Leroux. The reachability problem for Petri nets is not primitive recursive. In Annual Symposium on Foundations of Computer Science, pages 1241-1252. IEEE, 2021. URL: https://doi.org/10.1109/FOCS52979.2021.00121.
  29. Richard J. Lipton. The reachability problem requires exponential space. Technical Report 62, Yale University, 1976. Google Scholar
  30. Marvin L. Minsky. Computation: finite and infinite machines. Prentice-Hall, Inc., 1967. Google Scholar
  31. Reino Niskanen, Igor Potapov, and Julien Reichert. Undecidability of two-dimensional robot games. In International Symposium on Mathematical Foundations of Computer Science, volume 58 of LIPIcs, pages 73:1-73:13. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. URL: https://doi.org/10.4230/LIPIcs.MFCS.2016.73.
  32. Aditya Prakash and K. S. Thejaswini. On history-deterministic one-counter nets. In International Conference on Foundations of Software Science and Computational Structures. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-30829-1_11.
  33. Charles Rackoff. The covering and boundedness problems for vector addition systems. Theoretical Computer Science, pages 223-231, 1978. URL: https://doi.org/10.1016/0304-3975(78)90036-1.
  34. Klaus Reinhardt. Reachability in Petri nets with inhibitor arcs. Electronic Notes in Theoretical Computer Science, 223:239-264, 2008. URL: https://doi.org/10.1016/j.entcs.2008.12.042.
  35. Michal Skrzypczak. Büchi VASS recognise w-languages that are Sigma^1_1 - complete. CoRR, abs/1708.09658, 2017. URL: https://arxiv.org/abs/1708.09658.
  36. Leslie G. Valiant and Mike Paterson. Deterministic one-counter automata. Journal of Computer and System Sciences, 10(3):340-350, 1975. URL: https://doi.org/10.1016/S0022-0000(75)80005-5.
  37. Rüdiger Valk and Guy Vidal-Naquet. Petri nets and regular languages. Journal of Computer and System Sciences, 23(3):299-325, 1981. URL: https://doi.org/10.1016/0022-0000(81)90067-2.
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