Document Open Access Logo

Right-Linear Lattices: An Algebraic Theory of ω-Regular Languages, with Fixed Points

Authors Anupam Das , Abhishek De

PDF

File

Thumbnail PDF
PDF
LIPIcs.MFCS.2025.39.pdf
  • Filesize: 0.83 MB
  • 17 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Grammars and context-free languages
  • Theory of computation → Automata over infinite objects
  • Theory of computation → Logic and verification
  • Theory of computation → Modal and temporal logics
Keywords
  • omega-languages
  • regular languages
  • fixed points
  • Kleene algebras
  • right-linear grammars

Metrics

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

Abstract

Alternating parity automata (APAs) provide a robust formalism for modelling infinite behaviours and play a central role in formal verification. Despite their widespread use, the algebraic theory underlying APAs has remained largely unexplored. In recent work [Anupam Das and Abhishek De, 2024], a notation for non-deterministic finite automata (NFAs) was introduced, along with a sound and complete axiomatisation of their equational theory via right-linear algebras. In this paper, we extend that line of work to the setting of infinite words. In particular, we present a dualised syntax, yielding a notation for APAs based on right-linear lattice expressions, and provide a natural axiomatisation of their equational theory with respect to the standard language model of ω-regular languages. The design of this axiomatisation is guided by the theory of fixed point logics; in fact, the completeness factors cleanly through the completeness of the linear-time μ-calculus.

Cite As Get BibTex

Anupam Das and Abhishek De. Right-Linear Lattices: An Algebraic Theory of ω-Regular Languages, with Fixed Points. In 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 345, pp. 39:1-39:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.MFCS.2025.39

Author Details

Anupam Das
  • School of Computer Science, University of Birmingham, UK
Abhishek De
  • School of Computer Science, University of Birmingham, UK

Funding

This work was supported by a UKRI Future Leaders Fellowship, "Structure vs Invariants in Proofs", project reference MR/S035540/1.

Acknowledgements

The authors thank Georg Struth, Mike Cruchten, Debam Biswas, Denis Kuperberg and Damien Pous for fruitful discussions.

References

  1. Carolyn Jane Anderson, Nate Foster, Arjun Guha, Jean-Baptiste Jeannin, Dexter Kozen, Cole Schlesinger, and David Walker. Netkat: semantic foundations for networks. In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '14, pages 113-126, New York, NY, USA, 2014. Association for Computing Machinery. URL: https://doi.org/10.1145/2535838.2535862.
  2. Hajnal Andréka, Szabolcs Mikulás, and István Németi. The equational theory of kleene lattices. Theoretical Computer Science, 412(52):7099-7108, 2011. URL: https://doi.org/10.1016/j.tcs.2011.09.024.
  3. Maurice Boffa. Une remarque sur les systèmes complets d'identités rationnelles. Theor. Inform. Appl., 24(4):419-423, 1990. URL: https://doi.org/10.1051/ITA/1990240404191.
  4. Maurice Boffa. Une condition impliquant toutes les identités rationnelles. Theor. Inform. Appl., 29(6):515-518, 1995. URL: https://doi.org/10.1051/ITA/1995290605151.
  5. Mikołaj Bojańczyk. Automata, logic and games, 2023. Lecture course at University of Warsaw. URL: https://www.mimuw.edu.pl/~bojan/2022-2023/automata-logic-and-games-2023.
  6. Paul Brunet. Reversible kleene lattices. In Kim G. Larsen, Hans L. Bodlaender, and Jean-Francois Raskin, editors, 42nd International Symposium on Mathematical Foundations of Computer Science, MFCS 2017, August 21-25, 2017 - Aalborg, Denmark, volume 83 of LIPIcs, pages 66:1-66:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. URL: https://doi.org/10.4230/LIPICS.MFCS.2017.66.
  7. J. Richard Büchi. On a Decision Method in Restricted Second Order Arithmetic, pages 425-435. Springer New York, New York, NY, 1990. URL: https://doi.org/10.1007/978-1-4613-8928-6_23.
  8. Ernie Cohen. Separation and reduction. In Roland Backhouse and José Nuno Oliveira, editors, Mathematics of Program Construction, pages 45-59, Berlin, Heidelberg, 2000. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/10722010_4.
  9. James Cranch, Michael R. Laurence, and Georg Struth. Completeness results for omega-regular algebras. J. Log. Algebraic Methods Program., 84(3):402-425, 2015. URL: https://doi.org/10.1016/J.JLAMP.2014.10.002.
  10. 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.
  11. Anupam Das and Abhishek De. An algebraic theory of ω-regular languages, via μν-expressions, 2025. URL: https://arxiv.org/abs/2505.10303.
  12. Anupam Das and Damien Pous. Non-wellfounded proof theory for (kleene+action)(algebras+lattices). In Dan R. Ghica and Achim Jung, editors, 27th EACSL Annual Conference on Computer Science Logic, CSL 2018, September 4-7, 2018, Birmingham, UK, volume 119 of LIPIcs, pages 19:1-19:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. URL: https://doi.org/10.4230/LIPICS.CSL.2018.19.
  13. Amina Doumane. Constructive completeness for the linear-time μ-calculus. In 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017, pages 1-12. IEEE Computer Society, 2017. URL: https://doi.org/10.1109/LICS.2017.8005075.
  14. Paul Gastin and Denis Oddoux. Fast ltl to büchi automata translation. In Gérard Berry, Hubert Comon, and Alain Finkel, editors, Computer Aided Verification, pages 53-65, Berlin, Heidelberg, 2001. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/3-540-44585-4_6.
  15. R. Gerth, D. Peled, M. Y. Vardi, and P. Wolper. Simple On-the-fly Automatic Verification of Linear Temporal Logic, pages 3-18. Springer US, Boston, MA, 1996. URL: https://doi.org/10.1007/978-0-387-34892-6_1.
  16. Erich Grädel, Wolfgang Thomas, and Thomas Wilke, editors. Automata, Logics, and Infinite Games. Lecture notes in computer science. Springer, New York, NY, 2002 edition, February 2003. Google Scholar
  17. Gerard Holzmann. The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley Professional, 1st edition, 2011. Google Scholar
  18. Roope Kaivola. Axiomatising linear time mu-calculus. In Insup Lee and Scott A. Smolka, editors, CONCUR '95: Concurrency Theory, 6th International Conference, Philadelphia, PA, USA, August 21-24, 1995, Proceedings, volume 962 of Lecture Notes in Computer Science, pages 423-437. Springer, 1995. URL: https://doi.org/10.1007/3-540-60218-6_32.
  19. Bronisław Knaster and Alfred Tarski. Un théorème sur les fonctions d'ensembles. Annales de la Société Polonaise de Mathématique, 6:133-134, 1927. Google Scholar
  20. D. Kozen. A completeness theorem for kleene algebras and the algebra of regular events. Information and Computation, 110(2):366-390, 1994. URL: https://doi.org/10.1006/inco.1994.1037.
  21. Daniel Krob. Complete systems of b-rational identities. Theoretical Computer Science, 89(2):207-343, 1991. URL: https://doi.org/10.1016/0304-3975(91)90395-I.
  22. Michael R. Laurence and Georg Struth. On completeness of omega-regular algebras. In Wolfram Kahl and Timothy G. Griffin, editors, Relational and Algebraic Methods in Computer Science - 13th International Conference, RAMiCS 2012, Cambridge, UK, September 17-20, 2012. Proceedings, volume 7560 of Lecture Notes in Computer Science, pages 179-194. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-33314-9_12.
  23. Robert McNaughton. Testing and generating infinite sequences by a finite automaton. Information and Control, 9(5):521-530, 1966. URL: https://doi.org/10.1016/S0019-9958(66)80013-X.
  24. Michael O. Rabin. Decidability of second-order theories and automata on infinite trees. Bulletin of the American Mathematical Society, 74(5):1025-1029, 1968. Google Scholar
  25. V.N. Redko. On defining relations for the algebra of regular events. Ukrainskii Matematicheskii Zhurnal, 16(1):120-126, 1964. Google Scholar
  26. S. Safra. On the complexity of omega -automata. In [Proceedings 1988] 29th Annual Symposium on Foundations of Computer Science, pages 319-327, 1988. URL: https://doi.org/10.1109/SFCS.1988.21948.
  27. Arto Salomaa. Two complete axiom systems for the algebra of regular events. Journal of the ACM (JACM), 13(1):158-169, 1966. URL: https://doi.org/10.1145/321312.321326.
  28. Alfred Tarski. A lattice-theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics, 5:285-309, 1955. Google Scholar
  29. Moshe Y. Vardi. An automata-theoretic approach to linear temporal logic, pages 238-266. Springer Berlin Heidelberg, Berlin, Heidelberg, 1996. URL: https://doi.org/10.1007/3-540-60915-6_6.
  30. M.Y. Vardi and P. Wolper. Reasoning about infinite computations. Information and Computation, 115(1):1-37, 1994. URL: https://doi.org/10.1006/inco.1994.1092.
  31. K. W. Wagner. Eine axiomatisierung der theorie der regulären folgenmengen. J. Inf. Process. Cybern., 12:337-354, 1976. URL: https://api.semanticscholar.org/CorpusID:27249080.
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact