Abstract
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.
Cite
CITATION STYLE
Křetínský, J., Meggendorfer, T., Waldmann, C., & Weininger, M. (2017). Index appearance record for transforming rabin automata into parity automata. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 10205 LNCS, pp. 443–460). Springer Verlag. https://doi.org/10.1007/978-3-662-54577-5_26
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
