Document Open Access Logo

Coverability in 1-VASS with Disequality Tests

Authors Shaull Almagor , Nathann Cohen, Guillermo A. Pérez , Mahsa Shirmohammadi, James Worrell

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2020.38.pdf
  • Filesize: 0.57 MB
  • 20 pages

Document Identifiers

Author Details

Shaull Almagor
  • Technion - Israel Institute of Technology, Haifa, Israel
Nathann Cohen
  • CNRS & LRI, Gif-sur-Yvette, France
Guillermo A. Pérez
  • University of Antwerp, Belgium
Mahsa Shirmohammadi
  • CNRS & IRIF, Université de Paris, France
James Worrell
  • University of Oxford, UK

Funding

  • Almagor, Shaull: has received funding from the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie grant agreement No 837327.
  • Worrell, James: Supported by EPSRC Fellowship EP/N008197/1.

Acknowledgements

We thank P. Offtermatt for pointing us to literature on NC-algorithms.

Cite AsGet BibTex

Shaull Almagor, Nathann Cohen, Guillermo A. Pérez, Mahsa Shirmohammadi, and James Worrell. Coverability in 1-VASS with Disequality Tests. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 38:1-38:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/LIPIcs.CONCUR.2020.38

Abstract

We study a class of reachability problems in weighted graphs with constraints on the accumulated weight of paths. The problems we study can equivalently be formulated in the model of vector addition systems with states (VASS). We consider a version of the vertex-to-vertex reachability problem in which the accumulated weight of a path is required always to be non-negative. This is equivalent to the so-called control-state reachability problem (also called the coverability problem) for 1-dimensional VASS. We show that this problem lies in NC: the class of problems solvable in polylogarithmic parallel time. In our main result we generalise the problem to allow disequality constraints on edges (i.e., we allow edges to be disabled if the accumulated weight is equal to a specific value). We show that in this case the vertex-to-vertex reachability problem is solvable in polynomial time even though a shortest path may have exponential length. In the language of VASS this means that control-state reachability is in polynomial time for 1-dimensional VASS with disequality tests.

Subject Classification

ACM Subject Classification
  • Theory of computation → Models of computation
Keywords
  • Reachability
  • Vector addition systems with states
  • Weighted graphs

Metrics

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

References

  1. Sanjeev Arora and Boaz Barak. Computational Complexity - A Modern Approach. Cambridge University Press, 2009. URL: http://www.cambridge.org/catalogue/catalogue.asp?isbn=9780521424264.
  2. Benedikt Bollig, Karin Quaas, and Arnaud Sangnier. The complexity of flat freeze LTL. In 28th International Conference on Concurrency Theory, CONCUR, volume 85 of LIPIcs, pages 33:1-33:16, 2017. Google Scholar
  3. Daniel P. Bovet and Pierluigi Crescenzi. Introduction to the theory of complexity. Prentice Hall international series in computer science. Prentice Hall, 1994. Google Scholar
  4. Daniel Bundala and Joël Ouaknine. On parametric timed automata and one-counter machines. Inf. Comput., 253:272-303, 2017. Google Scholar
  5. Wojciech Czerwinski, Slawomir Lasota, Ranko Lazic, Jérôme Leroux, and Filip Mazowiecki. The reachability problem for petri nets is not elementary. In Proceedings of the 51st Annual ACM SIGACT Symposium on Theory of Computing, STOC 2019, pages 24-33. ACM, 2019. Google Scholar
  6. S. Demri, R. Lazic, and A. Sangnier. Model checking memoryful linear-time logics over one-counter automata. Theor. Comput. Sci., 411(22-24):2298-2316, 2010. Google Scholar
  7. John Fearnley and Marcin Jurdzinski. Reachability in two-clock timed automata is pspace-complete. In Automata, Languages, and Programming - 40th International Colloquium, ICALP 2013, Riga, Latvia, July 8-12, 2013, Proceedings, volume 7966 of Lecture Notes in Computer Science, pages 212-223. Springer, 2013. Google Scholar
  8. Alain Finkel, Stefan Göller, and Christoph Haase. Reachability in register machines with polynomial updates. In Mathematical Foundations of Computer Science 2013 - 38th International Symposium, MFCS, volume 8087 of Lecture Notes in Computer Science, pages 409-420. Springer, 2013. Google Scholar
  9. Stefan Göller, Christoph Haase, Joël Ouaknine, and James Worrell. Model checking succinct and parametric one-counter automata. In Automata, Languages and Programming, 37th International Colloquium, ICALP, volume 6199 of Lecture Notes in Computer Science, pages 575-586. Springer, 2010. Google Scholar
  10. C. Haase, S. Kreutzer, J. Ouaknine, and J. Worrell. Reachability in succinct and parametric one-counter automata. In Proceedings of CONCUR, volume 5710 of LNCS, pages 369-383. Springer, 2009. Google Scholar
  11. P. Lafourcade, D. Lugiez, and R. Treinen. Intruder deduction for AC-like equational theories with homomorphisms. In Research Report LSV-04-16, LSV, ENS de Cachan, 2004. Google Scholar
  12. Matti Nykänen and Esko Ukkonen. The exact path length problem. J. Algorithms, 42(1):41-53, 2002. Google Scholar
  13. Christos H. Papadimitriou. Computational complexity. Addison-Wesley, 1994. Google Scholar
  14. Franco P. Preparata. New parallel-sorting schemes. IEEE Trans. Computers, 27(7):669-673, 1978. URL: https://doi.org/10.1109/TC.1978.1675167.
  15. Charles Rackoff. The covering and boundedness problems for vector addition systems. Theor. Comput. Sci., 6:223-231, 1978. Google Scholar
  16. Louis E. Rosier and Hsu-Chun Yen. A multiparameter analysis of the boundedness problem for vector addition systems. J. Comput. Syst. Sci., 32(1):105-135, 1986. Google Scholar
  17. Heribert Vollmer. Introduction to Circuit Complexity - A Uniform Approach. Texts in Theoretical Computer Science. An EATCS Series. Springer, 1999. URL: https://doi.org/10.1007/978-3-662-03927-4.
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