Document Open Access Logo

New Techniques for Universality in Unambiguous Register Automata

Authors Wojciech Czerwiński , Antoine Mottet , Karin Quaas

PDF
Thumbnail PDF

File

LIPIcs.ICALP.2021.129.pdf
  • Filesize: 0.79 MB
  • 16 pages

Document Identifiers

Author Details

Wojciech Czerwiński
  • University of Warsaw, Poland
Antoine Mottet
  • Department of Algebra, Faculty of Mathematics and Physics, Charles University, Prague, Czech Republic
Karin Quaas
  • University of Leipzig, Germany

Funding

  • Czerwiński, Wojciech: Supported by the European Research Council (ERC) grant LIPA, grant agreement No 683080.
  • Mottet, Antoine: This author has received funding from the ERC under the European Union’s Horizon 2020 research and innovation programme (grant agreement No 771005).
  • Quaas, Karin: Funded by the Deutsche Forschungsgemeinschaft (DFG), project 406907430.

Acknowledgements

We thank Lorenzo Clemente, Sławomir Lasota, and Radosław Piórkowski for inspiring discussions on URA.

Cite AsGet BibTex

Wojciech Czerwiński, Antoine Mottet, and Karin Quaas. New Techniques for Universality in Unambiguous Register Automata. In 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 198, pp. 129:1-129:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.ICALP.2021.129

Abstract

Register automata are finite automata equipped with a finite set of registers ranging over the domain of some relational structure like (ℕ; =) or (ℚ; <). Register automata process words over the domain, and along a run of the automaton, the registers can store data from the input word for later comparisons. It is long known that the universality problem, i.e., the problem to decide whether a given register automaton accepts all words over the domain, is undecidable. Recently, we proved the problem to be decidable in 2-ExpSpace if the register automaton under study is over (ℕ; =) and unambiguous, i.e., every input word has at most one accepting run; this result was shortly after improved to 2-ExpTime by Barloy and Clemente. In this paper, we go one step further and prove that the problem is in ExpSpace, and in PSpace if the number of registers is fixed. Our proof is based on new techniques that additionally allow us to show that the problem is in PSpace for single-register automata over (ℚ; <). As a third technical contribution we prove that the problem is decidable (in ExpSpace) for a more expressive model of unambiguous register automata, where the registers can take values nondeterministically, if defined over (ℕ; =) and only one register is used.

Subject Classification

ACM Subject Classification
  • Theory of computation → Automata over infinite objects
Keywords
  • Register Automata
  • Data Languages
  • Unambiguity
  • Unambiguous
  • Universality
  • Containment
  • Language Inclusion
  • Equivalence

Metrics

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

References

  1. Corentin Barloy and Lorenzo Clemente. Bidimensional linear recursive sequences and universality of unambiguous register automata. In Proceedings of STACS'21, 2021. To appear. Google Scholar
  2. Mikolaj Bojanczyk, Bartek Klin, and Joshua Moerman. Orbit-finite-dimensional vector spaces and weighted register automata. In Proceedings of LICS'21, 2021. To appear. URL: http://arxiv.org/abs/2104.02438.
  3. Alin Bostan, Arnaud Carayol, Florent Koechlin, and Cyril Nicaud. Weakly-Unambiguous Parikh Automata and Their Link to Holonomic Series. In Artur Czumaj, Anuj Dawar, and Emanuela Merelli, editors, 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020), volume 168 of Leibniz International Proceedings in Informatics (LIPIcs), pages 114:1-114:16, Dagstuhl, Germany, 2020. Schloss Dagstuhl-Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.ICALP.2020.114.
  4. Nicolas Bousquet and Christof Löding. Equivalence and inclusion problem for strongly unambiguous Büchi automata. In Language and Automata Theory and Applications, 4th International Conference, LATA 2010, Trier, Germany, May 24-28, 2010. Proceedings, pages 118-129, 2010. URL: https://doi.org/10.1007/978-3-642-13089-2_10.
  5. Thomas Colcombet. Unambiguity in automata theory. In Proceedings of DCFS 2015, pages 3-18, 2015. Google Scholar
  6. Wojciech Czerwinski, Diego Figueira, and Piotr Hofman. Universality problem for unambiguous VASS. In Proceedings of CONCUR 2020, pages 36:1-36:15, 2020. Google Scholar
  7. Laure Daviaud, Marcin Jurdzinski, Ranko Lazic, Filip Mazowiecki, Guillermo A. Pérez, and James Worrell. When is containment decidable for probabilistic automata? In 45th International Colloquium on Automata, Languages, and Programming, ICALP 2018, July 9-13, 2018, Prague, Czech Republic, pages 121:1-121:14, 2018. URL: https://doi.org/10.4230/LIPIcs.ICALP.2018.121.
  8. 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.
  9. Stéphane Demri, Ranko Lazic, and Arnaud Sangnier. Model checking freeze LTL over one-counter automata. In Proceedings of FOSSACS 2008, pages 490-504, 2008. Google Scholar
  10. Diego Figueira, Santiago Figueira, Sylvain Schmitz, and Philippe Schnoebelen. Ackermannian and primitive-recursive bounds with dickson’s lemma. In Proceedings of LICS 2011, pages 269-278, 2011. Google Scholar
  11. Dimitri Isaak and Christof Löding. Efficient inclusion testing for simple classes of unambiguous ω-automata. Inf. Process. Lett., 112(14-15):578-582, 2012. URL: https://doi.org/10.1016/j.ipl.2012.04.010.
  12. Michael Kaminski and Nissim Francez. Finite-memory automata. Theor. Comput. Sci., 134(2):329-363, 1994. Google Scholar
  13. Michael Kaminski and Daniel Zeitlin. Finite-memory automata with non-deterministic reassignment. International Journal of Foundations of Computer Science, Volume 21, Issue 05, 2010. Google Scholar
  14. 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
  15. 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
  16. Erik Paul. Finite Sequentiality of Finitely Ambiguous Max-Plus Tree Automata. In Artur Czumaj, Anuj Dawar, and Emanuela Merelli, editors, 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020), volume 168 of Leibniz International Proceedings in Informatics (LIPIcs), pages 137:1-137:15, Dagstuhl, Germany, 2020. Schloss Dagstuhl-Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.ICALP.2020.137.
  17. 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
  18. 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
  19. 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-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact