Detail výsledku

Complementation of Emerson-Lei Automata

HAVLENA, V.; LENGÁL, O.; ŠMAHLÍKOVÁ, B. Complementation of Emerson-Lei Automata. Proceedings of FoSSaCS'25. Lecture Notes in Computer Science. Heidelberg: Springer Verlag, 2025. no. 1, p. 88-110. ISSN: 0302-9743.
Typ
článek ve sborníku konference
Jazyk
anglicky
Autoři
Havlena Vojtěch, Ing., Ph.D., UITS (FIT)
Lengál Ondřej, doc. Ing., Ph.D., UITS (FIT)
Šmahlíková Barbora, Ing.
Abstrakt

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.

Klíčová slova

Emerson-Lei automata, TELA, complementation, Büchi automata, rank-based
complementation, Rabin automata, parity automata

URL
Rok
2025
Strany
88–110
Časopis
Lecture Notes in Computer Science, roč. 15691, č. 1, ISSN 0302-9743
Sborník
Proceedings of FoSSaCS'25
Konference
28th International Conference on Foundations of Software Science and Computation Structures --- FoSSaCS'25
Vydavatel
Springer Verlag
Místo
Heidelberg
DOI
10.1007/978-3-031-90897-2_5
BibTeX 
@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"
}
Soubory
Projekty
Efektivní konečné automaty pro automatické usuzování, MŠMT, ERC CZ, LL1908, zahájení: 2020-01-01, ukončení: 2024-12-31, ukončen
QUAK: Analýza kvantových programů pomocí automatů, GAČR, Standardní projekty, 25-18318S, zahájení: 2025-01-01, ukončení: 2027-12-31, řešení
Reliable, Secure, and Intelligent Computer Systems, VUT, Vnitřní projekty VUT, FIT-S-23-8151, zahájení: 2023-03-01, ukončení: 2026-02-28, řešení
Výzkumné skupiny
Automata@FIT (VZ Automata@FIT)
Výzkumná skupina automatizované analýzy a verifikace - VeriFIT (VZ VERIFIT)
Pracoviště
Ústav inteligentních systémů (UITS)
Nahoru