Index appearance record for transforming Rabin automata into parity automata

TL;DR

This paper introduces an optimized appearance record method for transforming Rabin automata into parity automata, resulting in smaller automata and improved performance in LTL synthesis compared to existing approaches.

Contribution

A novel, more efficient appearance record variant tailored for Rabin automata, with optimizations and experimental validation showing improved automata size reduction.

Findings

Smaller automata produced than previous methods

Enhanced efficiency demonstrated in LTL synthesis

Potential for significant improvements on complex formulas

Abstract

Transforming deterministic $\omega$-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.