Result Details
Complementation of Emerson-Lei Automata
Lengál Ondřej, doc. Ing., Ph.D., DITS (FIT)
Šmahlíková Barbora, Ing.
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
extends a given complementation algorithm for a condition in a way that the
resulting procedure handles conditions of the form Fin & phi. The
proposed constructions give upper bounds that are exponentially better than the
state of the art for some of the classes.
Emerson-Lei automata, TELA, complementation, Büchi automata, rank-based
complementation, Rabin automata, parity automata
@inproceedings{BUT196842,
author="Vojtěch {Havlena} and Ondřej {Lengál} and Barbora {Šmahlíková}",
title="Complementation of Emerson-Lei Automata",
booktitle="Proceedings of FoSSaCS'25",
year="2025",
journal="Lecture Notes in Computer Science",
volume="15691",
number="1",
pages="88--110",
publisher="Springer Verlag",
address="Heidelberg",
doi="10.1007/978-3-031-90897-2\{_}5",
issn="0302-9743",
url="https://link.springer.com/chapter/10.1007/978-3-031-90897-2_5"
}QUAK: Quantum Program Analysis using Automata Toolkit, GACR, Standardní projekty, 25-18318S, start: 2025-01-01, end: 2027-12-31, running
Reliable, Secure, and Intelligent Computer Systems, BUT, Vnitřní projekty VUT, FIT-S-23-8151, start: 2023-03-01, end: 2026-02-28, running