Complementation of Emerson-Lei Automata (Technical Report)
Fuente:
arXiv
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866917803923079168 |
|---|---|
| author | Havlena, Vojtěch Lengál, Ondřej Šmahlíková, Barbora |
| author_facet | Havlena, Vojtěch Lengál, Ondřej Šmahlíková, Barbora |
| contents | We give new constructions for complementing subclasses of Emerson-Lei automata using modifications of rank-based Büchi automata complementation. In particular, we propose a specialized rank-based construction for a Boolean combination of Inf acceptance conditions, which heavily relies on a novel way of a run DAG labelling enhancing the ranking functions with models of the acceptance condition. Moreover, we propose a technique for complementing generalized Rabin automata, which are structurally as concise as general Emerson-Lei automata (but can have a larger acceptance condition). The construction is modular in the sense that it combines a given complementation algorithm for a condition $φ$ in a way that the resulting procedure handles conditions of the form Fin ${} \land φ$. The proposed constructions give upper bounds that are exponentially better than the state of the art for some of the classes. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2410_11644 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Complementation of Emerson-Lei Automata (Technical Report) Havlena, Vojtěch Lengál, Ondřej Šmahlíková, Barbora Logic in Computer Science Formal Languages and Automata Theory We give new constructions for complementing subclasses of Emerson-Lei automata using modifications of rank-based Büchi automata complementation. In particular, we propose a specialized rank-based construction for a Boolean combination of Inf acceptance conditions, which heavily relies on a novel way of a run DAG labelling enhancing the ranking functions with models of the acceptance condition. Moreover, we propose a technique for complementing generalized Rabin automata, which are structurally as concise as general Emerson-Lei automata (but can have a larger acceptance condition). The construction is modular in the sense that it combines a given complementation algorithm for a condition $φ$ in a way that the resulting procedure handles conditions of the form Fin ${} \land φ$. The proposed constructions give upper bounds that are exponentially better than the state of the art for some of the classes. |
| title | Complementation of Emerson-Lei Automata (Technical Report) |
| topic | Logic in Computer Science Formal Languages and Automata Theory |
| url | https://arxiv.org/abs/2410.11644 |