Detail publikačního výsledku

Reducing (to) the Ranks: Efficient Rank-based Büchi Automata Complementation

HAVLENA, V.; LENGÁL, O.

Original Title

Reducing (to) the Ranks: Efficient Rank-based Büchi Automata Complementation

English Title

Reducing (to) the Ranks: Efficient Rank-based Büchi Automata Complementation

Type

Paper in proceedings (conference paper)

Original Abstract

This paper provides several optimizations of the rank-based approach for complementing Büchi automata. We start with Schewe's theoretically optimal construction and develop a set of techniques for pruning its state space that are key to obtaining small complement automata in practice. In particular, the reductions (except one) have the property that they preserve (at least some) so-called super-tight runs, which are runs whose ranking is as tight as possible. Our evaluation on a large benchmark shows that the optimizations indeed significantly help the rank-based approach and that, in a large number of cases, the obtained complement is the smallest from those produced by state-of-the-art tools for Büchi complementation.

English abstract

This paper provides several optimizations of the rank-based approach for complementing Büchi automata. We start with Schewe's theoretically optimal construction and develop a set of techniques for pruning its state space that are key to obtaining small complement automata in practice. In particular, the reductions (except one) have the property that they preserve (at least some) so-called super-tight runs, which are runs whose ranking is as tight as possible. Our evaluation on a large benchmark shows that the optimizations indeed significantly help the rank-based approach and that, in a large number of cases, the obtained complement is the smallest from those produced by state-of-the-art tools for Büchi complementation.

Keywords

Büchi automata,rank-based complementation,super-tight runs

Key words in English

Büchi automata,rank-based complementation,super-tight runs

Authors

HAVLENA, V.; LENGÁL, O.

RIV year

2022

Released

23.08.2021

Publisher

Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik

Location

Paris

Book

32nd International Conference on Concurrency Theory (CONCUR 2021)

ISBN

1868-8969

Periodical

Leibniz International Proceedings in Informatics, LIPIcs

Volume

203

Number

8

State

unknown

Pages from

1

Pages to

19

Pages count

19

URL

https://doi.org/10.4230/LIPIcs.CONCUR.2021.2

Full text in the Digital Library

http://hdl.handle.net/

BibTex

@inproceedings{BUT175801,
  author="Vojtěch {Havlena} and Ondřej {Lengál}",
  title="Reducing (to) the Ranks: Efficient Rank-based Büchi Automata Complementation",
  booktitle="32nd International Conference on Concurrency Theory (CONCUR 2021)",
  year="2021",
  journal="Leibniz International Proceedings in Informatics, LIPIcs",
  volume="203",
  number="8",
  pages="1--19",
  publisher="Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik",
  address="Paris",
  doi="10.4230/LIPIcs.CONCUR.2021.2",
  issn="1868-8969",
  url="https://doi.org/10.4230/LIPIcs.CONCUR.2021.2"
}