Document Open Access Logo

Parametrized Universality Problems for One-Counter Nets

Authors Shaull Almagor , Udi Boker, Piotr Hofman , Patrick Totzke

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2020.47.pdf
  • Filesize: 0.63 MB
  • 16 pages

Document Identifiers

Author Details

Shaull Almagor
  • Technion - Israel Institute of Technology, Haifa, Israel
Udi Boker
  • Interdisciplinary Center (IDC) Herzliya, Israel
Piotr Hofman
  • University of Warsaw, Poland
Patrick Totzke
  • University of Liverpool, UK

Funding

  • Almagor, Shaull: European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie grant agreement No 837327.
  • Boker, Udi: Israel Science Foundation grant 1373/16.
  • Hofman, Piotr: Supported by the NCN grant 2017 B/ST6/02093.

Acknowledgements

We are grateful for fruitful discussions during the Autoboz'2019 workshop.

Cite As Get BibTex

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). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 47:1-47:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020) https://doi.org/10.4230/LIPIcs.CONCUR.2020.47

Abstract

We study the language universality problem for One-Counter Nets, also known as 1-dimensional Vector Addition Systems with States (1-VASS), parameterized either with an initial counter value, or with an upper bound on the allowed counter value during runs. The language accepted by an OCN (defined by reaching a final control state) is monotone in both parameters. This yields two natural questions: 1) does there exist an initial counter value that makes the language universal? 2) does there exist a sufficiently high ceiling so that the bounded language is universal?
Although the ordinary universality problem is decidable (and Ackermann-complete) and these parameterized variants seem to reduce to checking basic structural properties of the underlying automaton, we show that in fact both problems are undecidable. We also look into the complexities of the problems for several decidable subclasses, namely for unambiguous, and deterministic systems, and for those over a single-letter alphabet.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
Keywords
  • Counter net
  • VASS
  • Unambiguous Automata
  • Universality

Metrics

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

Related Versions

References

  1. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Piotr Hofman, Richard Mayr, K. Narayan Kumar, and Patrick Totzke. Infinite-state energy games. In ACM/IEEE Symposium on Logic in Computer Science (LICS). ACM, 2014. URL: https://doi.org/10.1145/2603088.2603100.
  2. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Richard Mayr Radu Ciobanu, and Patrick Totzke. Universal safety for timed Petri nets is PSPACE-complete. In International Conference on Concurrency Theory (CONCUR), 2018. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2018.6.
  3. Parosh Aziz Abdulla, Pavel Krcal, and Wang Yi. R-automata. In International Conference on Concurrency Theory (CONCUR), 2008. Google Scholar
  4. S. Almagor, U. Boker, and O. Kupferman. What’s decidable about weighted automata? In International Symposium on Automated Technology for Verification and Analysis (ATVA), 2011. Google Scholar
  5. Shaull Almagor, Udi Boker, Piotr Hofman, and Patrick Totzke. Parametrized universality problems for one-counter nets. CoRR, 2020. URL: http://arxiv.org/abs/2005.03435.
  6. Shaull Almagor, Nathann Cohen, Guillermo A. Pérez, Mahsa Shirmohammadi, and James Worrell. Coverability in 1-vass with disequality tests. In International Conference on Concurrency Theory (CONCUR), 2020. Google Scholar
  7. Michael Blondin, Alain Finkel, Stefan Göller, Christoph Haase, and Pierre McKenzie. Reachability in two-dimensional vector addition systems with states is PSPACE-complete. In ACM/IEEE Symposium on Logic in Computer Science (LICS). IEEE Computer Society, 2015. URL: https://doi.org/10.1109/LICS.2015.14.
  8. 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 (STACS). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2017. URL: https://doi.org/10.4230/LIPIcs.STACS.2017.14.
  9. Stanislav Böhm, Stefan Göller, and Petr Jančar. Bisimilarity of one-counter processes is pspace-complete. In International Conference on Concurrency Theory (CONCUR), 2010. Google Scholar
  10. Patricia Bouyer, Uli Fahrenberg, Kim G. Larsen, Nicolas Markey, and Jiří Srba. Infinite runs in weighted timed automata with energy constraints. In International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS), 2008. URL: https://doi.org/10.1007/978-3-540-85778-5_4.
  11. Wojciech Czerwiński, Diego Figueira, and Piotr Hofman. Universality Problem for Unambiguous VASS. In International Conference on Concurrency Theory (CONCUR), 2020. Google Scholar
  12. A. Degorre, L. Doyen, R. Gentilini, J.F. Raskin, and S. Torunczyk. Energy and mean-payoff games with imperfect information. In Computer Science Logic (CSL), 2010. Google Scholar
  13. Stéphane Demri. On selective unboundedness of VASS. Journal of Computer and System Sciences, 2013. Google Scholar
  14. Piotr Hofman, Slawomir Lasota, Richard Mayr, and Patrick Totzke. Simulation problems over one-counter nets. Logical Methods in Computer Science, 2016. URL: https://doi.org/10.2168/LMCS-12(1:6)2016.
  15. Piotr Hofman and Patrick Totzke. Trace inclusion for one-counter nets revisited. Theoretical Computer Science, 2017. URL: https://doi.org/10.1016/j.tcs.2017.05.009.
  16. Petr Jancar, Javier Esparza, and Faron Moller. Petri Nets and Regular Processes. Journal of Computer and System Sciences, 1999. Google Scholar
  17. S. Rao Kosaraju and Gregory F. Sullivan. Detecting cycles in dynamic graphs in polynomial time (preliminary version). In Symposium on Theory of Computing (STOC). ACM, 1988. Google Scholar
  18. Jérôme Leroux and Grégoire Sutre. On flatness for 2-dimensional vector addition systems with states. In International Conference on Concurrency Theory (CONCUR). Springer Berlin Heidelberg, 2004. Google Scholar
  19. Richard Mayr. Undecidability of weak bisimulation equivalence for 1-counter processes. In International Colloquium on Automata, Languages and Programming (ICALP). Springer, 2003. Google Scholar
  20. M.L. Minsky. Computation: Finite and Infinite Machines. Prentice Hall, 1 edition, 1967. Google Scholar
  21. Charles Rackoff. The covering and boundedness problems for vector addition systems. Theoretical Computer Science, 1978. URL: https://doi.org/10.1016/0304-3975(78)90036-1.
  22. Louis E. Rosier and Hsu-Chun Yen. A multiparameter analysis of the boundedness problem for vector addition systems. In International Symposium on Fundamentals of Computation Theory (FCT). Springer Berlin Heidelberg, 1985. Google Scholar
  23. L. J. Stockmeyer and A. R. Meyer. Word problems requiring exponential time(preliminary report). In Proceedings of the Fifth Annual ACM Symposium on Theory of Computing. ACM, 1973. URL: https://doi.org/10.1145/800125.804029.
  24. Leslie G. Valiant. Decision Procedures for Families of Deterministic Pushdown Automata. PhD thesis, University of Warwick, 1973. URL: http://wrap.warwick.ac.uk/34701/.
  25. Heribert Vollmer. Introduction to Circuit Complexity: A Uniform Approach. Springer-Verlag, 1999. Google Scholar
  26. Tzeng Wen-Guey. On path equivalence of nondeterministic finite automata. Information Processing Letters, 1996. URL: https://doi.org/10.1016/0020-0190(96)00039-7.
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