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

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216305%3A26230%2F21%3APU142924" target="_blank" >RIV/00216305:26230/21:PU142924 - isvavai.cz</a>

Výsledek na webu

<a href="https://doi.org/10.4230/LIPIcs.CONCUR.2021.2" target="_blank" >https://doi.org/10.4230/LIPIcs.CONCUR.2021.2</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.4230/LIPIcs.CONCUR.2021.2" target="_blank" >10.4230/LIPIcs.CONCUR.2021.2</a>

Jazyk výsledku

angličtina

Název v původním jazyce

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

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

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

Popis výsledku anglicky

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.

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Projekt

<a href="/cs/project/GA20-07487S" target="_blank" >GA20-07487S: Škálovatelné techniky pro analýzu komplexních vlastností počítačových systémů</a><br>

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Rok uplatnění

2021

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název statě ve sborníku

32nd International Conference on Concurrency Theory (CONCUR 2021)

ISBN

—

ISSN

1868-8969

e-ISSN

—

Počet stran výsledku

19

Strana od-do

1-19

Název nakladatele

Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik

Místo vydání

Paris

Místo konání akce

Paris

Datum konání akce

23. 8. 2021

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

—