Index Appearance Record for Transforming Rabin Automata into Parity Automata

KŘETÍNSKÝ, Jan; Tobias MEGGENDORFER; Clara WALDMANN a Maximilian WEININGER. Index Appearance Record for Transforming Rabin Automata into Parity Automata. In Tools and Algorithms for the Construction and Analysis of Systems - 23rd International Conference, TACAS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, Part I. Springer, 2017, s. 443-460. ISBN 9783662545768. Dostupné z: https://doi.org/10.1007/978-3-662-54577-5_26.

Základní údaje

Originální název

Index Appearance Record for Transforming Rabin Automata into Parity Automata

Autoři

KŘETÍNSKÝ, Jan; Tobias MEGGENDORFER; Clara WALDMANN a Maximilian WEININGER

Vydání

Tools and Algorithms for the Construction and Analysis of Systems - 23rd International Conference, TACAS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, Part I, od s. 443-460, 18 s. 2017

Nakladatel

Springer

---

Další údaje

Typ výsledku

Stať ve sborníku

Označené pro přenos do RIV

Ne

Organizační jednotka

Fakulta informatiky

ISBN

9783662545768

ISSN

DOI

https://doi.org/10.1007/978-3-662-54577-5_26

---

Anotace

V originále

Transforming deterministic ω-automata into deterministic parity automata is traditionally done using variants of appearance records. We present a more efficient variant of this approach, tailored to Rabin automata, and several optimizations applicable to all appearance records. We compare the methods experimentally and find out that our method produces smaller automata than previous approaches. Moreover, the experiments demonstrate the potential of our method for LTL synthesis, using LTL-to-Rabin translators. It leads to significantly smaller parity automata when compared to state-of-the-art approaches on complex formulae.