Document Open Access Logo

Bidimensional Linear Recursive Sequences and Universality of Unambiguous Register Automata

Authors Corentin Barloy, Lorenzo Clemente

PDF
Thumbnail PDF

File

LIPIcs.STACS.2021.8.pdf
  • Filesize: 0.98 MB
  • 15 pages

Document Identifiers

Author Details

Corentin Barloy
  • École Normale Supérieure de Paris, PSL, France
Lorenzo Clemente
  • University of Warsaw, Poland

Funding

  • Barloy, Corentin: Partially supported by the Polish NCN grant 2017/26/D/ST6/00201.
  • Clemente, Lorenzo: Partially supported by the Polish NCN grant 2017/26/D/ST6/00201.

Acknowledgements

We would like to thank Daniel Robertz for kindly providing us with the LDA package for Maple 16.

Cite AsGet BibTex

Corentin Barloy and Lorenzo Clemente. Bidimensional Linear Recursive Sequences and Universality of Unambiguous Register Automata. In 38th International Symposium on Theoretical Aspects of Computer Science (STACS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 187, pp. 8:1-8:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.STACS.2021.8

Abstract

We study the universality and inclusion problems for register automata over equality data (A, =). We show that the universality L(B) = (Σ × A)^* and inclusion problems L(A) ⊆ L(B) B can be solved with 2-EXPTIME complexity when both automata are without guessing and B is unambiguous, improving on the currently best-known 2-EXPSPACE upper bound by Mottet and Quaas. When the number of registers of both automata is fixed, we obtain a lower EXPTIME complexity, also improving the EXPSPACE upper bound from Mottet and Quaas for fixed number of registers. We reduce inclusion to universality, and then we reduce universality to the problem of counting the number of orbits of runs of the automaton. We show that the orbit-counting function satisfies a system of bidimensional linear recursive equations with polynomial coefficients (linrec), which generalises analogous recurrences for the Stirling numbers of the second kind, and then we show that universality reduces to the zeroness problem for linrec sequences. While such a counting approach is classical and has successfully been applied to unambiguous finite automata and grammars over finite alphabets, its application to register automata over infinite alphabets is novel. We provide two algorithms to decide the zeroness problem for bidimensional linear recursive sequences arising from orbit-counting functions. Both algorithms rely on techniques from linear non-commutative algebra. The first algorithm performs variable elimination and has elementary complexity. The second algorithm is a refined version of the first one and it relies on the computation of the Hermite normal form of matrices over a skew polynomial field. The second algorithm yields an EXPTIME decision procedure for the zeroness problem of linrec sequences, which in turn yields the claimed bounds for the universality and inclusion problems of register automata.

Subject Classification

ACM Subject Classification
  • Theory of computation → Automata over infinite objects
Keywords
  • unambiguous register automata
  • universality and inclusion problems
  • multi-dimensional linear recurrence sequences

Metrics

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

Related Versions

References

  1. Christel Baier, Stefan Kiefer, Joachim Klein, Sascha Klüppelholz, David Müller, and James Worrell. Markov Chains and Unambiguous Büchi Automata. In Swarat Chaudhuri and Azadeh Farzan, editors, Proc. of CAV'16, pages 23-42, Cham, 2016. Springer International Publishing. Google Scholar
  2. Corentin Barloy and Lorenzo Clemente. Bidimensional linear recursive sequences and universality of unambiguous register automata. arXiv e-prints, January 2021. URL: http://arxiv.org/abs/2101.01033.
  3. Mikołaj Bojańczyk. Slightly infinite sets, 2019. URL: https://www.mimuw.edu.pl/~bojan/paper/atom-book.
  4. 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, Proc. of ICALP'20, volume 168 of LIPIcs, pages 114:1-114:16, Dagstuhl, Germany, 2020. Schloss Dagstuhl-Leibniz-Zentrum für Informatik. Google Scholar
  5. Nicolas Bousquet and Christof Löding. Equivalence and inclusion problem for strongly unambiguous büchi automata. In Adrian-Horia Dediu, Henning Fernau, and Carlos Martín-Vide, editors, Proc. of LATA'10, pages 118-129, Berlin, Heidelberg, 2010. Springer Berlin Heidelberg. Google Scholar
  6. Mireille Bousquet-Mélou. Algebraic generating functions in enumerative combinatorics and context-free languages. In Volker Diekert and Bruno Durand, editors, Proc. of STACS'05, pages 18-35, Berlin, Heidelberg, 2005. Springer Berlin Heidelberg. Google Scholar
  7. Michaël Cadilhac, Alain Finkel, and Pierre McKenzie. Unambiguous constrained automata. In Hsu-Chun Yen and Oscar H. Ibarra, editors, Proc. of DLT'12, volume 7410 of LNCS, pages 239-250. Springer Berlin Heidelberg, 2012. Google Scholar
  8. Michaël Cadilhac, Filip Mazowiecki, Charles Paperman, Michał Pilipczuk, and Géraud Sénizergues. On Polynomial Recursive Sequences. In Artur Czumaj, Anuj Dawar, and Emanuela Merelli, editors, Proc. of ICALP'20, volume 168 of LIPIcs, pages 117:1-117:17, Dagstuhl, Germany, 2020. Schloss Dagstuhl-Leibniz-Zentrum für Informatik. Google Scholar
  9. Peter J. Cameron. Notes on Counting: An Introduction to Enumerative Combinatorics. Australian Mathematical Society Lecture Series. Cambridge University Press, 1 edition, 2017. Google Scholar
  10. Edward Y. C. Cheng and Michael Kaminski. Context-free languages over infinite alphabets. Acta Inf., 35(3):245-267, 1998. Google Scholar
  11. N. Chomsky and M. P. Schützenberger. The algebraic theory of context-free languages. In P. Braffort and D. Hirschberg, editors, Computer Programming and Formal Systems, volume 35 of Studies in Logic and the Foundations of Mathematics, pages 118-161. Elsevier, 1963. Google Scholar
  12. Lorenzo Clemente. On the complexity of the universality and inclusion problems for unambiguous context-free grammars. In Laurent Fribourg and Matthias Heizmann, editors, Proceedings 8th International Workshop on Verification and Program Transformation and 7th Workshop on Horn Clauses for Verification and Synthesis, Dublin, Ireland, 25-26th April 2020, volume 320 of EPTCS, pages 29-43. Open Publishing Association, 2020. URL: https://doi.org/10.4204/EPTCS.320.2.
  13. Lorenzo Clemente and Slawomir Lasota. Reachability analysis of first-order definable pushdown systems. In Stephan Kreutzer, editor, Proc. of CSL'15, volume 41 of LIPIcs, pages 244-259, Dagstuhl, 2015. Google Scholar
  14. Thomas Colcombet. Forms of Determinism for Automata (Invited Talk). In Christoph Dürr and Thomas Wilke, editors, Proc. of STACS'12, volume 14 of LIPIcs, pages 1-23, Dagstuhl, Germany, 2012. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. Google Scholar
  15. Thomas Colcombet. Unambiguity in automata theory. In Jeffrey Shallit and Alexander Okhotin, editors, Descriptional Complexity of Formal Systems, pages 3-18, Cham, 2015. Springer International Publishing. Google Scholar
  16. Wojciech Czerwiński, Diego Figueira, and Piotr Hofman. Universality Problem for Unambiguous VASS. In Igor Konnov and Laura Kovács, editors, Proc. of CONCUR'20, volume 171 of LIPIcs, pages 36:1-36:15, Dagstuhl, Germany, 2020. Schloss Dagstuhl-Leibniz-Zentrum für Informatik. Google Scholar
  17. Laure Daviaud, Marcin Jurdzinski, Ranko Lazic, Filip Mazowiecki, Guillermo A. Pérez, and James Worrell. When is Containment Decidable for Probabilistic Automatal. In Ioannis Chatzigiannakis, Christos Kaklamanis, Dániel Marx, and Donald Sannella, editors, Proc. of ICALP'18, volume 107 of LIPIcs, pages 121:1-121:14, Dagstuhl, Germany, 2018. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. Google Scholar
  18. Stéphane Demri and Ranko Lazić. LTL with the freeze quantifier and register automata. ACM Trans. Comput. Logic, 10(3):16:1-16:30, April 2009. Google Scholar
  19. Mark Giesbrecht and Myung Sub Kim. Computing the Hermite form of a matrix of Ore polynomials. Journal of Algebra, 376:341-362, 2013. Google Scholar
  20. John Hopcroft, Rajeev Motwani, and Jeffrey Ullman. Introduction to Automata Theory, Languages, and Computation. Addison-Wesley, 2000. Google Scholar
  21. Michael Kaminski and Nissim Francez. Finite-memory automata. Theoretical Computer Science, 134(2):329-363, 1994. Google Scholar
  22. Michael Kaminski and Daniel Zeitlin. Finite-memory automata with non-deterministic reassignment. International Journal of Foundations of Computer Science, 21(05):741-760, 2010. Google Scholar
  23. Werner Kuich. On the multiplicity equivalence problem for context-free grammars. In Proceedings of the Colloquium in Honor of Arto Salomaa on Results and Trends in Theoretical Computer Science, pages 232 - -250, Berlin, Heidelberg, 1994. Springer-Verlag. Google Scholar
  24. Dugald Macpherson. A survey of homogeneous structures. Discrete Math., 311(15):1599-1634, August 2011. Google Scholar
  25. Antoine Mottet and Karin Quaas. The containment problem for unambiguous register automata and unambiguous timed automata. Theory of Computing Systems, 2020. URL: https://doi.org/10.1007/s00224-020-09997-2.
  26. A.S. Murawski, S.J. Ramsay, and N. Tzevelekos. Reachability in pushdown register automata. Journal of Computer and System Sciences, 87:58-83, 2017. Google Scholar
  27. Frank Neven, Thomas Schwentick, and Victor Vianu. Finite state machines for strings over infinite alphabets. ACM Trans. Comput. Logic, 5(3):403 - -435, July 2004. Google Scholar
  28. Oystein Ore. Linear equations in non-commutative fields. Annals of Mathematics, 32(3):463-477, 1931. URL: http://www.jstor.org/stable/1968245.
  29. Oystein Ore. Theory of non-commutative polynomials. Annals of Mathematics, 34(3):480-508, 1933. URL: http://www.jstor.org/stable/1968173.
  30. Mikhail Raskin. A Superpolynomial Lower Bound for the Size of Non-Deterministic Complement of an Unambiguous Automaton. In Ioannis Chatzigiannakis, Christos Kaklamanis, Dániel Marx, and Donald Sannella, editors, Proc. of ICALP'18, volume 107 of LIPIcs, pages 138:1-138:11, Dagstuhl, Germany, 2018. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. Google Scholar
  31. Arto Salomaa and Marti Soittola. Automata-theoretic aspects of formal power series. Texts and Monographs in Computer Science. Springer, 1978. Google Scholar
  32. James Schmerl. A decidable ℵ₀-categorical theory with a non-recursive Ryll-Nardzewski function. Fundamenta Mathematicae, 98(2):121-125, 1978. Google Scholar
  33. Luc Segoufin. Automata and logics for words and trees over an infinite alphabet. In Zoltán Ésik, editor, Computer Science Logic, volume 4207 of LNCS, pages 41-57. Springer Berlin Heidelberg, 2006. Google Scholar
  34. Géraud Sénizergues. The equivalence problem for deterministic pushdown automata is decidable. In Pierpaolo Degano, Roberto Gorrieri, and Alberto Marchetti-Spaccamela, editors, Proc. of ICALP'97, pages 671-681, Berlin, Heidelberg, 1997. Springer Berlin Heidelberg. Google Scholar
  35. Richard P. Stanley. Differentiably finite power series. European Journal of Combinatorics, 1(2):175-188, 1980. Google Scholar
  36. Richard P. Stanley. Enumerative Combinatorics. The Wadsworth & Brooks/Cole Mathematics Series 1. Springer, 1 edition, 1986. Google Scholar
  37. R. Stearns and H. Hunt. On the equivalence and containment problems for unambiguous regular expressions, grammars, and automata. In Proc. of SFCS'81, pages 74-81, Washington, DC, USA, 1981. IEEE Computer Society. URL: https://doi.org/10.1109/SFCS.1981.29.
  38. L. J. Stockmeyer and A. R. Meyer. Word problems requiring exponential time (preliminary report). In Proc. of STOC'73, pages 1-9, New York, NY, USA, 1973. ACM. Google Scholar
  39. Tzeng Wen-Guey. On path equivalence of nondeterministic finite automata. Information Processing Letters, 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