This work is licensed under the Creative Commons Attribution License. Exploiting the Temporal Logic Hierarchy and the Non-Confluence Property for Efficient LTL Synthesis

The classic approaches to synthesize a reactive system from a linear temporal logic (LTL) specifica-tion first translate the given LTL formula to an equivalent ω-automaton and then compute a winning strategy for the corresponding ω-regular game. To this end, the obtained ω-automata have to be (pseudo)-determinized where typically a variant of Safra’s determinization procedure is used. In this paper, we show that this determinization step can be significantly improved for tool implemen-tations by replacing Safra’s determinization by simpler determinization procedures. In particular, we exploit (1) the temporal logic hierarchy that corresponds to the well-known automata hierar-chy consisting of safety, liveness, Büchi, and co-Büchi automata as well as their boolean closures, (2) the non-confluence property of ω-automata that result from certain translations of LTL formu-las, and (3) symbolic implementations of determinization procedures for the Rabin-Scott and the Miyano-Hayashi breakpoint construction. In particular, we present convincing experimental results that demonstrate the practical applicability of our new synthesis procedure.