Publication result detail

Complementation of Emerson-Lei Automata

HAVLENA, V.; LENGÁL, O.; ŠMAHLÍKOVÁ, B.

Original Title

Complementation of Emerson-Lei Automata

English Title

Complementation of Emerson-Lei Automata

Type

Paper in proceedings outside WoS and Scopus

Original Abstract

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.

English abstract

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.

Keywords

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

Key words in English

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

Authors

HAVLENA, V.; LENGÁL, O.; ŠMAHLÍKOVÁ, B.

Released

03.05.2025

Publisher

Springer Verlag

Location

Heidelberg

Book

Proceedings of FoSSaCS'25

ISBN

0302-9743

Periodical

Lecture Notes in Computer Science

Volume

15691

Number

1

State

Federal Republic of Germany

Pages from

88

Pages to

110

Pages count

19

URL

Full text in the Digital Library

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"
}

Documents