Algebras for Automata: Reasoning with Regularity (Invited Talk)

Author Anupam Das



PDF
Thumbnail PDF

File

LIPIcs.STACS.2025.3.pdf
  • Filesize: 424 kB
  • 1 pages

Document Identifiers

Author Details

Anupam Das
  • University of Birmingham, UK

Cite As Get BibTex

Anupam Das. Algebras for Automata: Reasoning with Regularity (Invited Talk). In 42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 327, p. 3:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.STACS.2025.3

Abstract

In the second half of the 20th century various theories of regular expressions were proposed, eventually leading to the notion of a Kleene Algebra (KA). Kozen and Krob independently proved the completeness of KA for the model of regular languages, a now celebrated result that has been refined and generalised over the years. In recent years proof theoretic approaches to regular languages have been studied, providing alternative routes to metalogical results like completeness and decidability. 
In this talk I will present a new approach from a different starting point: finite state automata. A notation for non-deterministic finite automata is readily obtained via expressions with least fixed points, leading to a theory of right-linear algebras (RLA). RLA is strictly more general than KA, e.g. admitting ω-regular languages as a model too, and enjoys a simpler proof theory than KA. This allows us to recover (more general) metalogical results in a robust way, combining techniques from automata, games, and cyclic proofs. Finally I will discuss extensions of RLA by greatest fixed points, comprising a notation for parity automata, to reason about ω-regular languages too.
This talk is based on joint works with Abhishek De [Anupam Das and Abhishek De, 2024a and 2024b].

Subject Classification

ACM Subject Classification
  • Theory of computation → Regular languages
  • Theory of computation → Proof theory
Keywords
  • Regular languages
  • Linear grammars
  • Proof theory
  • Cyclic proofs
  • Automata theory
  • Fixed points
  • Games

Metrics

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

References

  1. Anupam Das and Abhishek De. A proof theory of (ω-)context-free languages, via non-wellfounded proofs. In Christoph Benzmüller, Marijn J. H. Heule, and Renate A. Schmidt, editors, Automated Reasoning - 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3-6, 2024, Proceedings, Part II, volume 14740 of Lecture Notes in Computer Science, pages 237-256. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-63501-4_13.
  2. Anupam Das and Abhishek De. A proof theory of right-linear (ω-)grammars via cyclic proofs. In Pawel Sobocinski, Ugo Dal Lago, and Javier Esparza, editors, Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2024, Tallinn, Estonia, July 8-11, 2024, pages 30:1-30:14. ACM, 2024. URL: https://doi.org/10.1145/3661814.3662138.
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