Document Open Access Logo

A Polynomial-Time Algorithm for Reachability in Branching VASS in Dimension One

Authors Stefan Göller, Christoph Haase, Ranko Lazic, Patrick Totzke

PDF
Thumbnail PDF

File

LIPIcs.ICALP.2016.105.pdf
  • Filesize: 0.6 MB
  • 13 pages

Document Identifiers

Author Details

Stefan Göller
Christoph Haase
Ranko Lazic
Patrick Totzke

Cite As Get BibTex

Stefan Göller, Christoph Haase, Ranko Lazic, and Patrick Totzke. A Polynomial-Time Algorithm for Reachability in Branching VASS in Dimension One. In 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 55, pp. 105:1-105:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016) https://doi.org/10.4230/LIPIcs.ICALP.2016.105

Abstract

Branching VASS (BVASS) generalise vector addition systems with states by allowing for special branching transitions that can non-deterministically distribute a counter value between two control states. A run of a BVASS consequently becomes a tree, and reachability is to decide whether a given configuration is the root of a reachability tree. This paper shows P-completeness of reachability in BVASS in dimension one, the first decidability result for reachability in a subclass of BVASS known so far. Moreover, we show that coverability and boundedness in BVASS in dimension one are P-complete as well.

Subject Classification

Keywords
  • branching vector addition systems
  • reachability
  • coverability
  • boundedness

Metrics

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

References

  1. A.K. Chandra, D. Kozen, and L.J. Stockmeyer. Alternation. J. ACM, 28(1):114-133, 1981. URL: http://dx.doi.org/10.1145/322234.322243.
  2. Ph. de Groote, B. Guillaume, and S. Salvati. Vector addition tree automata. In Logic in Computer Science, LICS, pages 64-73. IEEE Computer Society, 2004. URL: http://dx.doi.org/10.1109/LICS.2004.1319601.
  3. S. Demri, M. Jurdziński, O. Lachish, and R. Lazić. The covering and boundedness problems for branching vector addition systems. J. Comput. Syst. Sci., 79(1):23-38, 2013. URL: http://dx.doi.org/10.1016/j.jcss.2012.04.002.
  4. M. Englert, R. Lazić, and P. Totzke. Reachability in two-dimensional unary vector addition systems with states is NL-complete. In Logic in Computer Science, LICS, 2016. To appear. Google Scholar
  5. P. Ganty and R. Majumdar. Algorithmic verification of asynchronous programs. ACM Trans. Program. Lang. Syst., 34(1):6, 2012. URL: http://dx.doi.org/10.1145/2160910.2160915.
  6. S.M. German and A.P. Sistla. Reasoning about systems with many processes. J. ACM, 39(3):675-735, 1992. URL: http://dx.doi.org/10.1145/146637.146681.
  7. S. Göller, C. Haase, R. Lazić, and P. Totzke. A polynomial-time algorithm for reachability in branching VASS in dimension one. CoRR, abs/1602.05547, 2016. URL: http://arxiv.org/abs/1602.05547.
  8. P. Jančar and Z. Sawa. A note on emptiness for alternating finite automata with a one-letter alphabet. Inf. Process. Lett., 104(5):164-167, 2007. URL: http://dx.doi.org/10.1016/j.ipl.2007.06.006.
  9. A. Jez and A. Okhotin. Conjunctive grammars over a unary alphabet: Undecidability and unbounded growth. Theory Comput. Syst., 46(1):27-58, 2010. URL: http://dx.doi.org/10.1007/s00224-008-9139-5.
  10. R. Lazić and S. Schmitz. Nonelementary complexities for branching VASS, MELL, and Extensions. ACM Trans. Comput. Log., 16(3):20, 2015. URL: http://dx.doi.org/10.1145/2733375.
  11. J. Leroux and S. Schmitz. Demystifying reachability in vector addition systems. In Logic in Computer Science, LICS, pages 56-67. IEEE, 2015. URL: http://dx.doi.org/10.1109/LICS.2015.16.
  12. R.J. Lipton. The reachability problem requires exponential space. Yale University, Technical Report 62, 1976. Google Scholar
  13. C.H. Papadimitriou. Computational Complexity. Addison-Wesley, 1994. Google Scholar
  14. C. Rackoff. The covering and boundedness problems for vector addition systems. Theor. Comput. Sci., 6:223-231, 1978. URL: http://dx.doi.org/10.1016/0304-3975(78)90036-1.
  15. O. Serre. Parity games played on transition graphs of one-counter processes. In Foundations of Software Science and Computation Structures, FoSSaCS, pages 337-351, 2006. URL: http://dx.doi.org/10.1007/11690634_23.
  16. L.G. Valiant and M. Paterson. Deterministic one-counter automata. J. Comput. Syst. Sci., 10(3):340-350, 1975. URL: http://dx.doi.org/10.1016/S0022-0000(75)80005-5.
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