Document Open Access Logo

Determinization of One-Counter Nets

Authors Shaull Almagor , Asaf Yeshurun

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2022.18.pdf
  • Filesize: 1 MB
  • 23 pages

Document Identifiers

Author Details

Shaull Almagor
  • Department of Computer Science, Technion - Israel Institute of Technology, Haifa, Israel
Asaf Yeshurun
  • Department of Computer Science, Technion - Israel Institute of Technology, Haifa, Israel

Cite As Get BibTex

Shaull Almagor and Asaf Yeshurun. Determinization of One-Counter Nets. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 18:1-18:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022) https://doi.org/10.4230/LIPIcs.CONCUR.2022.18

Abstract

One-Counter Nets (OCNs) are finite-state automata equipped with a counter that is not allowed to become negative, but does not have zero tests. Their simplicity and close connection to various other models (e.g., VASS, Counter Machines and Pushdown Automata) make them an attractive model for studying the border of decidability for the classical decision problems.
The deterministic fragment of OCNs (DOCNs) typically admits more tractable decision problems, and while these problems and the expressive power of DOCNs have been studied, the determinization problem, namely deciding whether an OCN admits an equivalent DOCN, has not received attention.
We introduce four notions of OCN determinizability, which arise naturally due to intricacies in the model, and specifically, the interpretation of the initial counter value. We show that in general, determinizability is undecidable under most notions, but over a singleton alphabet (i.e., 1 dimensional VASS) one definition becomes decidable, and the rest become trivial, in that there is always an equivalent DOCN.

Subject Classification

ACM Subject Classification
  • Theory of computation → Formal languages and automata theory
Keywords
  • Determinization
  • One-Counter Net
  • Vector Addition System
  • Automata
  • Semilinear

Metrics

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

Related Versions

References

  1. Parosh Aziz Abdulla and Karlis Čerāns. Simulation is decidable for one-counter nets. In International Conference on Concurrency Theory, pages 253-268. Springer, 1998. Google Scholar
  2. Shaull Almagor, Udi Boker, Piotr Hofman, and Patrick Totzke. Parametrized universality problems for one-counter nets. In 31st International Conference on Concurrency Theory (CONCUR 2020). Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 2020. Google Scholar
  3. Leonard Berman. The complexity of logical theories. Theoretical Computer Science, 11(1):71-77, 1980. Google Scholar
  4. Michael Blondin, Matthias Englert, Alain Finkel, Stefan GÖller, Christoph Haase, Ranko Lazić, Pierre Mckenzie, and Patrick Totzke. The reachability problem for two-dimensional vector addition systems with states. Journal of the ACM (JACM), 68(5):1-43, 2021. Google Scholar
  5. Stanislav Böhm, Stefan Göller, and Petr Jančar. Bisimilarity of one-counter processes is pspace-complete. In International Conference on Concurrency Theory, pages 177-191. Springer, 2010. Google Scholar
  6. Stanislav Böhm, Stefan Göller, and Petr Jančar. Bisimulation equivalence and regularity for real-time one-counter automata. Journal of Computer and System Sciences, 80(4):720-743, 2014. Google Scholar
  7. Udi Boker and Thomas A. Henzinger. Exact and approximate determinization of discounted-sum automata. Log. Methods Comput. Sci., 10(1), 2014. URL: https://doi.org/10.2168/LMCS-10(1:10)2014.
  8. Itshak Borosh and Leon Bruce Treybig. Bounds on positive integral solutions of linear diophantine equations. Proceedings of the American Mathematical Society, 55(2):299-304, 1976. Google Scholar
  9. Adam L Buchsbaum, Raffaele Giancarlo, and Jeffery R Westbrook. On the determinization of weighted finite automata. SIAM Journal on Computing, 30(5):1502-1531, 2000. Google Scholar
  10. Wojciech Czerwiński and Slawomir Lasota. Regular separability of one counter automata. In 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1-12. IEEE, 2017. Google Scholar
  11. Alain Finkel, Gilles Geeraerts, J-F Raskin, and Laurent Van Begin. On the ω-language expressive power of extended petri nets. Theoretical computer science, 356(3):374-386, 2006. Google Scholar
  12. Seymour Ginsburg and Edwin H Spanier. Bounded algol-like languages. Transactions of the American Mathematical Society, 113(2):333-368, 1964. Google Scholar
  13. C. Haase. A survival guide to presburger arithmetic. ACM SIGLOG News, 5(3):67-82, 2018. URL: https://dl.acm.org/citation.cfm?id=3242964, URL: https://doi.org/10.1145/3242953.3242964.
  14. Christoph Haase. Subclasses of presburger arithmetic and the weak exp hierarchy. In Proceedings of the 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), pages 1-10, 2014. Google Scholar
  15. Piotr Hofman, Richard Mayr, and Patrick Totzke. Decidability of weak simulation on one-counter nets. In 2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science, pages 203-212. IEEE, 2013. Google Scholar
  16. Piotr Hofman and Patrick Totzke. Trace inclusion for one-counter nets revisited. Theoretical Computer Science, 735:50-63, 2018. Google Scholar
  17. Petr Jančar, Antonín Kučera, and Faron Moller. Simulation and bisimulation over one-counter processes. In Annual Symposium on Theoretical Aspects of Computer Science, pages 334-345. Springer, 2000. Google Scholar
  18. Petr Jancar and Faron Moller. Simulation of one-counter nets via colouring. In Proceedings of Workshop Journées Systemes Infinis, pages 1-6, 1999. Google Scholar
  19. Petr Jančar, Faron Moller, et al. Simulation problems for one-counter machine. In International Conference on Current Trends in Theory and Practice of Computer Science, pages 404-413. Springer, 1999. Google Scholar
  20. Daniel Kirsten and Sylvain Lombardy. Deciding unambiguity and sequentiality of polynomially ambiguous min-plus automata. In 26th International Symposium on Theoretical Aspects of Computer Science. Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 2009. Google Scholar
  21. Ines Klimann, Sylvain Lombardy, Jean Mairesse, and Christophe Prieur. Deciding unambiguity and sequentiality from a finitely ambiguous max-plus automaton. Theoretical Computer Science, 327(3):349-373, 2004. Google Scholar
  22. Jérôme Leroux and Grégoire Sutre. On flatness for 2-dimensional vector addition systems with states. In International Conference on Concurrency Theory, pages 402-416. Springer, 2004. Google Scholar
  23. Richard Mayr. Undecidable problems in unreliable computations. Theoretical Computer Science, 297(1-3):337-354, 2003. Google Scholar
  24. Marvin Lee Minsky. Computation: Finite and Infinite Machines. Prentice-Hall Englewood Cliffs, 1967. Google Scholar
  25. M. Mohri. Finite-state transducers in language and speech processing. Computational Linguistics, 23(2):269-311, 1997. Google Scholar
  26. Mojzesz Presburger. Uber die vollstandigkeiteines gewissen systems der arithmetik ganzer zahlen, in welchen die addition als einzige operation hervortritt. In Comptes-Rendus du ler Congres des Mathematiciens des Pays Slavs, 1929. Google Scholar
  27. Philippe Schnoebelen. Lossy counter machines decidability cheat sheet. In International Workshop on Reachability Problems, pages 51-75. Springer, 2010. Google Scholar
  28. Jiří Srba. Beyond language equivalence on visibly pushdown automata. Logical Methods in Computer Science, 5, 2009. Google Scholar
  29. Larry J Stockmeyer and Albert R Meyer. Word problems requiring exponential time (preliminary report). In Proceedings of the fifth annual ACM symposium on Theory of computing, pages 1-9, 1973. Google Scholar
  30. Patrick Totzke, Richard Mayr, Slawomir Lasota, and Piotr Hofman. Simulation problems over one-counter nets. Logical Methods in Computer Science, 12, 2016. Google Scholar
  31. Leslie Valiant. Decision procedures for families of deterministic pushdown automata. PhD thesis, University of Warwick, 1973. Google Scholar
  32. Rüdiger Valk and Guy Vidal-Naquet. Petri nets and regular languages. Journal of Computer and system Sciences, 23(3):299-325, 1981. 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