Document Open Access Logo

Universality Problem for Unambiguous VASS

Authors Wojciech Czerwiński , Diego Figueira , Piotr Hofman

PDF

File

Thumbnail PDF
PDF
LIPIcs.CONCUR.2020.36.pdf
  • Filesize: 1.74 MB
  • 15 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Formal languages and automata theory
Keywords
  • unambiguity
  • vector addition systems
  • universality problems

Metrics

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

Abstract

We study languages of unambiguous VASS, that is, Vector Addition Systems with States, whose transitions read letters from a finite alphabet, and whose acceptance condition is defined by a set of final states (i.e., the coverability language). We show that the problem of universality for unambiguous VASS is ExpSpace-complete, in sheer contrast to Ackermann-completeness for arbitrary VASS, even in dimension 1. When the dimension d ∈ ℕ is fixed, the universality problem is PSpace-complete if d ≥ 2, and coNP-hard for 1-dimensional VASSes (also known as One Counter Nets).

Cite As Get BibTex

Wojciech Czerwiński, Diego Figueira, and Piotr Hofman. Universality Problem for Unambiguous VASS. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 36:1-36:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020) https://doi.org/10.4230/LIPIcs.CONCUR.2020.36

Author Details

Wojciech Czerwiński
  • University of Warsaw, Poland
Diego Figueira
  • Université Bordeaux, CNRS, Bordeaux INP, LaBRI, UMR 5800, Talence, France
Piotr Hofman
  • University of Warsaw, Poland

Funding

  • Czerwiński, Wojciech: Supported by the ERC grant LIPA, agreement no. 683080.
  • Figueira, Diego: ANR BraVAS (ANR-17-CE40-0028); ANR DéLTA (ANR-16-CE40-0007).

Acknowledgements

We thank Lorenzo Clemente for leading us to the NC² membership for UFA universality problem.

References

  1. Thomas Colcombet. Unambiguity in automata theory. In Proceedings of DCFS 2015, pages 3-18, 2015. Google Scholar
  2. Wojciech Czerwiński, Sławomir Lasota, Roland Meyer, Sebastian Muskalla, K. Narayan Kumar, and Prakash Saivasan. Regular separability of well-structured transition systems. In 29th International Conference on Concurrency Theory, CONCUR 2018, volume 118 of LIPIcs, pages 35:1-35:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2018.35.
  3. Stéphane Demri and Ranko Lazic. LTL with the freeze quantifier and register automata. ACM Trans. Comput. Log., 10(3):16:1-16:30, 2009. URL: https://doi.org/10.1145/1507244.1507246.
  4. John Fearnley and Marcin Jurdziński. Reachability in two-clock timed automata is PSPACE-complete. Inf. Comput., 243:26-36, 2015. Google Scholar
  5. Piotr Hofman and Patrick Totzke. Trace inclusion for one-counter nets revisited. In Joël Ouaknine, Igor Potapov, and James Worrell, editors, Proceedings of RP 2014, volume 8762 of Lecture Notes in Computer Science, pages 151-162. Springer, 2014. Google Scholar
  6. Petr Jančar, Javier Esparza, and Faron Moller. Petri nets and regular processes. J. Comput. Syst. Sci., 59(3):476-503, 1999. Google Scholar
  7. Richard M. Karp. Reducibility among combinatorial problems. In Proceedings of a symposium on the Complexity of Computer Computations 1972, pages 85-103, 1972. Google Scholar
  8. Richard Lipton. The reachability problem requires exponential space. Department of Computer Science. Yale University, 62, 1976. Google Scholar
  9. Antoine Mottet and Karin Quaas. The containment problem for unambiguous register automata. In Proceedings of STACS 2019, pages 53:1-53:15, 2019. Google Scholar
  10. Frank Neven, Thomas Schwentick, and Victor Vianu. Finite state machines for strings over infinite alphabets. ACM Trans. Comput. Log., 5(3):403-435, 2004. Google Scholar
  11. Charles Rackoff. The covering and boundedness problems for vector addition systems. Theor. Comput. Sci., 6:223-231, 1978. Google Scholar
  12. Mikhail Raskin. A superpolynomial lower bound for the size of non-deterministic complement of an unambiguous automaton. In Proceedings of ICALP 2018, pages 138:1-138:11, 2018. Google Scholar
  13. Géraud Sénizergues. L(A)=L(B)? decidability results from complete formal systems. Theor. Comput. Sci., 251(1-2):1-166, 2001. Google Scholar
  14. Richard Edwin Stearns and Harry B. Hunt III. On the equivalence and containment problems for unambiguous regular expressions, regular grammars and finite automata. SIAM J. Comput., 14(3):598-611, 1985. Google Scholar
  15. Wen-Guey Tzeng. On path equivalence of nondeterministic finite automata. Inf. Process. Lett., 58(1):43-46, 1996. 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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact