Cyclic system for an algebraic theory of alternating parity automata
Fuente:
arXiv
Salvato in:
| Autori principali: | , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2025
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866916735970443264 |
|---|---|
| author | Das, Anupam De, Abhishek |
| author_facet | Das, Anupam De, Abhishek |
| contents | $ω$-regular languages are a natural extension of the regular languages to the setting of infinite words. Likewise, they are recognised by a host of automata models, one of the most important being Alternating Parity Automata (APAs), a generalisation of Büchi automata that symmetrises both the transitions (with universal as well as existential branching) and the acceptance condition (by a parity condition).
In this work we develop a cyclic proof system manipulating APAs, represented by an algebraic notation of Right Linear Lattice expressions. This syntax dualises that of previously introduced Right Linear Algebras, which comprised a notation for non-deterministic finite automata (NFAs). This dualisation induces a symmetry in the proof systems we design, with lattice operations behaving dually on each side of the sequent. Our main result is the soundness and completeness of our system for $ω$-language inclusion, heavily exploiting game theoretic techniques from the theory of $ω$-regular languages. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2505_09000 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Cyclic system for an algebraic theory of alternating parity automata Das, Anupam De, Abhishek Logic in Computer Science Formal Languages and Automata Theory Logic $ω$-regular languages are a natural extension of the regular languages to the setting of infinite words. Likewise, they are recognised by a host of automata models, one of the most important being Alternating Parity Automata (APAs), a generalisation of Büchi automata that symmetrises both the transitions (with universal as well as existential branching) and the acceptance condition (by a parity condition). In this work we develop a cyclic proof system manipulating APAs, represented by an algebraic notation of Right Linear Lattice expressions. This syntax dualises that of previously introduced Right Linear Algebras, which comprised a notation for non-deterministic finite automata (NFAs). This dualisation induces a symmetry in the proof systems we design, with lattice operations behaving dually on each side of the sequent. Our main result is the soundness and completeness of our system for $ω$-language inclusion, heavily exploiting game theoretic techniques from the theory of $ω$-regular languages. |
| title | Cyclic system for an algebraic theory of alternating parity automata |
| topic | Logic in Computer Science Formal Languages and Automata Theory Logic |
| url | https://arxiv.org/abs/2505.09000 |