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

Anupam Das; Abhishek De

doi:10.4230/LIPIcs.MFCS.2025.39

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

Anupam Das^*
, Abhishek De^*

^*Corresponding author for this work

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

12 Downloads (Pure)

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 [10], 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.

Original language	English
Title of host publication	50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)
Editors	Pawel Gawrychowski, Filip Mazowiecki, Michal Skrzypczak
Publisher	Schloss Dagstuhl - Leibniz-Zentrum für Informatik
Number of pages	17
ISBN (Electronic)	9783959773881
DOIs	https://doi.org/10.4230/LIPIcs.MFCS.2025.39
Publication status	Published - 20 Aug 2025
Event	50th International Symposium on Mathematical Foundations of Computer Science, MFCS 2025 - Warsaw, Poland Duration: 25 Aug 2025 → 29 Aug 2025

Publication series

Name	Leibniz International Proceedings in Informatics (LIPIcs)
Volume	345
ISSN (Print)	1868-8969

Conference

Conference	50th International Symposium on Mathematical Foundations of Computer Science, MFCS 2025
Country/Territory	Poland
City	Warsaw
Period	25/08/25 → 29/08/25

Bibliographical note

Publisher Copyright:
© Anupam Das and Abhishek De.

Keywords

fixed points
Kleene algebras
omega-languages
regular languages
right-linear grammars

ASJC Scopus subject areas

Software

Access to Document

10.4230/LIPIcs.MFCS.2025.39Licence: Creative Commons: Attribution (CC BY)

DasA2025RightFinal published version, 859 KBLicence: Creative Commons: Attribution (CC BY)

Structure vs. Invariants in Proofs (StrIP)
Das, A. (Principal Investigator)
Medical Research Council
1/05/20 → 31/07/24
Project: Research Councils

Cite this

Das, A., & De, A. (2025). Right-Linear Lattices: An Algebraic Theory of ω-Regular Languages, with Fixed Points. In P. Gawrychowski, F. Mazowiecki, & M. Skrzypczak (Eds.), 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025) Article 39 (Leibniz International Proceedings in Informatics (LIPIcs); Vol. 345). Schloss Dagstuhl - Leibniz-Zentrum für Informatik . https://doi.org/10.4230/LIPIcs.MFCS.2025.39

Das, Anupam ; De, Abhishek. / Right-Linear Lattices : An Algebraic Theory of ω-Regular Languages, with Fixed Points. 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025). editor / Pawel Gawrychowski ; Filip Mazowiecki ; Michal Skrzypczak. Schloss Dagstuhl - Leibniz-Zentrum für Informatik , 2025. (Leibniz International Proceedings in Informatics (LIPIcs)).

@inproceedings{b478d5d0241f48d79e7ba0fc8100d53c,

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

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 [10], 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.",

keywords = "fixed points, Kleene algebras, omega-languages, regular languages, right-linear grammars",

author = "Anupam Das and Abhishek De",

note = "Publisher Copyright: {\textcopyright} Anupam Das and Abhishek De.; 50th International Symposium on Mathematical Foundations of Computer Science, MFCS 2025 ; Conference date: 25-08-2025 Through 29-08-2025",

year = "2025",

month = aug,

day = "20",

doi = "10.4230/LIPIcs.MFCS.2025.39",

language = "English",

series = "Leibniz International Proceedings in Informatics (LIPIcs)",

publisher = "Schloss Dagstuhl - Leibniz-Zentrum f{\"u}r Informatik ",

editor = "Pawel Gawrychowski and Filip Mazowiecki and Michal Skrzypczak",

booktitle = "50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)",

}

Das, A & De, A 2025, Right-Linear Lattices: An Algebraic Theory of ω-Regular Languages, with Fixed Points. in P Gawrychowski, F Mazowiecki & M Skrzypczak (eds), 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)., 39, Leibniz International Proceedings in Informatics (LIPIcs), vol. 345, Schloss Dagstuhl - Leibniz-Zentrum für Informatik , 50th International Symposium on Mathematical Foundations of Computer Science, MFCS 2025, Warsaw, Poland, 25/08/25. https://doi.org/10.4230/LIPIcs.MFCS.2025.39

Right-Linear Lattices: An Algebraic Theory of ω-Regular Languages, with Fixed Points. / Das, Anupam; De, Abhishek.
50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025). ed. / Pawel Gawrychowski; Filip Mazowiecki; Michal Skrzypczak. Schloss Dagstuhl - Leibniz-Zentrum für Informatik , 2025. 39 (Leibniz International Proceedings in Informatics (LIPIcs); Vol. 345).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Right-Linear Lattices

T2 - 50th International Symposium on Mathematical Foundations of Computer Science, MFCS 2025

AU - Das, Anupam

AU - De, Abhishek

PY - 2025/8/20

Y1 - 2025/8/20

N2 - 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 [10], 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.

AB - 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 [10], 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.

KW - fixed points

KW - Kleene algebras

KW - omega-languages

KW - regular languages

KW - right-linear grammars

UR - https://www.scopus.com/pages/publications/105014722045

U2 - 10.4230/LIPIcs.MFCS.2025.39

DO - 10.4230/LIPIcs.MFCS.2025.39

M3 - Conference contribution

AN - SCOPUS:105014722045

T3 - Leibniz International Proceedings in Informatics (LIPIcs)

BT - 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)

A2 - Gawrychowski, Pawel

A2 - Mazowiecki, Filip

A2 - Skrzypczak, Michal

PB - Schloss Dagstuhl - Leibniz-Zentrum für Informatik

Y2 - 25 August 2025 through 29 August 2025

ER -

Das A, De A. Right-Linear Lattices: An Algebraic Theory of ω-Regular Languages, with Fixed Points. In Gawrychowski P, Mazowiecki F, Skrzypczak M, editors, 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025). Schloss Dagstuhl - Leibniz-Zentrum für Informatik . 2025. 39. (Leibniz International Proceedings in Informatics (LIPIcs)). doi: 10.4230/LIPIcs.MFCS.2025.39

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

Abstract

Publication series

Conference

Bibliographical note

Keywords

ASJC Scopus subject areas

Access to Document

Fingerprint

Projects

Structure vs. Invariants in Proofs (StrIP)

Cite this