Document Open Access Logo

Using Automata and a Decision Procedure to Prove Results in Pattern Matching (Invited Talk)

Author Jeffrey Shallit

PDF
Thumbnail PDF

File

LIPIcs.CPM.2022.2.pdf
  • Filesize: 0.52 MB
  • 3 pages

Document Identifiers

Author Details

Jeffrey Shallit
  • School of Computer Science, University of Waterloo, Canada

Funding

Research supported by NSERC 2018-04118.

Cite AsGet BibTex

Jeffrey Shallit. Using Automata and a Decision Procedure to Prove Results in Pattern Matching (Invited Talk). In 33rd Annual Symposium on Combinatorial Pattern Matching (CPM 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 223, pp. 2:1-2:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.CPM.2022.2

Abstract

The first-order theory of automatic sequences with addition is decidable, and this means that one can often prove combinatorial properties of these sequences "automatically", using the free software Walnut written by Hamoon Mousavi. In this talk I will explain how this is done, using as an example the measure of minimize size string attractor, introduced by Kempa and Prezza in 2018. Using the logic-based approach, we can also prove more general properties of string attractors for automatic sequences. This is joint work with Luke Schaeffer.

Subject Classification

ACM Subject Classification
  • Mathematics of computing → Combinatorics on words
  • Theory of computation → Regular languages
  • Theory of computation → Logic and verification
Keywords
  • finite automata
  • decision procedure
  • automatic sequence
  • Thue-Morse sequence
  • Fibonacci word
  • string attractor

Metrics

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

Related Versions

References

  1. A. Amir, Y. Aumann, A. Levy, and Y. Roshko. Quasi-distinct parsing and optimal compression methods. In G. Kucherov and E. Ukkonen, editors, CPM 2009, volume 5577 of Lecture Notes in Computer Science, pages 12-25. Springer-Verlag, 2009. Google Scholar
  2. H. Bannai, M. Funakoshi, T. I, D. Köppl, T. Mieno, and T. Nishimoto. A separation of γ and b via Thue–Morse words. In T. Lecroq and H. Touzet, editors, SPIRE 2021, volume 12944 of Lecture Notes in Computer Science, pages 168-178. Springer-Verlag, 2021. Google Scholar
  3. V. Bruyère, G. Hansel, C. Michaux, and R. Villemaire. Logic and p-recognizable sets of integers. Bull. Belgian Math. Soc., 1:191-238, 1994. Corrigendum, Bull. Belg. Math. Soc. 1:577, 1994. Google Scholar
  4. J. R. Büchi. Weak secord-order arithmetic and finite automata. Z. Math. Logik Grundlagen Math., 6:66-92, 1960. Reprinted in S. Mac Lane and D. Siefkes, eds., The Collected Works of J. Richard Büchi, Springer-Verlag, 1990, pp. 398-424. Google Scholar
  5. M. Karpinski, W. Rytter, and A. Shinohara. An efficient pattern-matching algorithm for strings with short descriptions. Nordic J. Computing, 4:172-186, 1997. Google Scholar
  6. D. Kempa and N. Prezza. At the roots of dictionary compression: string attractors. In STOC'18 Proceedings, pages 827-840. ACM Press, 2018. Google Scholar
  7. T. Kociumaka, G. Navarro, and N. Prezza. Towards a definitive measure of repetitiveness. In Y. Kohayakawa and F. K. Miyazawa, editors, LATIN 2020, volume 12118 of Lecture Notes in Computer Science, pages 207-219. Springer-Verlag, 2020. Google Scholar
  8. K. Kutsukake, T. Matsumoto, Y. Nakashima, S. Inenaga, H. Bannai, and M. Takeda. On repetitiveness measures of Thue-Morse words. In C. Boucher and S. V. Thankachan, editors, SPIRE 2020, volume 12303 of Lecture Notes in Computer Science, pages 213-220. Springer-Verlag, 2020. Google Scholar
  9. S. Mantaci, A. Restivo, G. Romana, G. Rosone, and M. Sciortino. String attractors and combinatorics on words. In ICTCS 2019, volume 2504 of CEUR Workshop Proceedings, pages 57-71, 2019. Available at URL: http://ceur-ws.org/Vol-2504/paper8.pdf.
  10. S. Mantaci, A. Restivo, G. Romana, G. Rosone, and M. Sciortino. A combinatorial view on string attractors. Theoret. Comput. Sci., 850:236-248, 2021. Google Scholar
  11. H. Mousavi. Automatic theorem proving in Walnut. Arxiv preprint arXiv:1603.06017 [cs.FL], 2016. URL: http://arxiv.org/abs/1603.06017.
  12. J. Radoszewski and W. Rytter. On the structure of compacted subword graphs of Thue-Morse words and their applications. J. Discrete Algorithms, 11:15-24, 2012. Google Scholar
  13. W. Rytter. The structure of subword graphs and suffix trees of Fibonacci words. Theoret. Comput. Sci., 363:211-223, 2006. Google Scholar
  14. L. Schaeffer and J. Shallit. String attractors for automatic sequences. Arxiv preprint arXiv:2012.06840 [cs.FL], 2021. URL: http://arxiv.org/abs/2012.06840.
  15. J. Shallit. The Logical Approach To Automatic Sequences: Exploring Combinatorics on Words with Walnut. Cambridge University Press, 2022. In press. 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