Universality Problem for Unambiguous VASS

Authors Wojciech Czerwiński , Diego Figueira , Piotr Hofman

Thumbnail PDF


  • Filesize: 1.74 MB
  • 15 pages

Document Identifiers

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


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

Cite AsGet 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)


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).

Subject Classification

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


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


  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

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail