conference paper published yes Jan Kretinsky author 44CEF464-F248-11E8-B48F-1D18A9856A870000-0002-8122-2881 Tobias Meggendorfer author b21b0c15-30a2-11eb-80dc-f13ca25802e10000-0002-1712-2165 Clara Waldmann author Maximilian Weininger author KrCh department TACAS: Tools and Algorithms for the Construction and Analysis of Systems 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. Springer2017Uppsala, Sweden eng 0302-9743 1611-3349 9783662545768 1701.05738 00044073490002610.1007/978-3-662-54577-5_26 10205443-460 Kretinsky, Jan, et al. “Index Appearance Record for Transforming Rabin Automata into Parity Automata.” <i>Tools and Algorithms for the Construction and Analysis of Systems</i>, vol. 10205, Springer, 2017, pp. 443–60, doi:<a href="https://doi.org/10.1007/978-3-662-54577-5_26">10.1007/978-3-662-54577-5_26</a>. J. Kretinsky, T. Meggendorfer, C. Waldmann, M. Weininger, in:, Tools and Algorithms for the Construction and Analysis of Systems, Springer, 2017, pp. 443–460. Kretinsky, Jan, Tobias Meggendorfer, Clara Waldmann, and Maximilian Weininger. “Index Appearance Record for Transforming Rabin Automata into Parity Automata.” In <i>Tools and Algorithms for the Construction and Analysis of Systems</i>, 10205:443–60. Springer, 2017. <a href="https://doi.org/10.1007/978-3-662-54577-5_26">https://doi.org/10.1007/978-3-662-54577-5_26</a>. Kretinsky, J., Meggendorfer, T., Waldmann, C., &#38; Weininger, M. (2017). Index appearance record for transforming Rabin automata into parity automata. In <i>Tools and Algorithms for the Construction and Analysis of Systems</i> (Vol. 10205, pp. 443–460). Uppsala, Sweden: Springer. <a href="https://doi.org/10.1007/978-3-662-54577-5_26">https://doi.org/10.1007/978-3-662-54577-5_26</a> Kretinsky J, Meggendorfer T, Waldmann C, Weininger M. 2017. Index appearance record for transforming Rabin automata into parity automata. Tools and Algorithms for the Construction and Analysis of Systems. TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 10205, 443–460. J. Kretinsky, T. Meggendorfer, C. Waldmann, and M. Weininger, “Index appearance record for transforming Rabin automata into parity automata,” in <i>Tools and Algorithms for the Construction and Analysis of Systems</i>, Uppsala, Sweden, 2017, vol. 10205, pp. 443–460. Kretinsky J, Meggendorfer T, Waldmann C, Weininger M. Index appearance record for transforming Rabin automata into parity automata. In: <i>Tools and Algorithms for the Construction and Analysis of Systems</i>. Vol 10205. Springer; 2017:443-460. doi:<a href="https://doi.org/10.1007/978-3-662-54577-5_26">10.1007/978-3-662-54577-5_26</a> 131602023-06-21T13:21:14Z2025-09-18T10:42:48Z