Exploiting the Temporal Logic Hierarchy and the Non-Confluence Property for Efficient LTL Synthesis

TL;DR

This paper introduces an improved LTL synthesis method that leverages the temporal logic hierarchy and non-confluence property to simplify automaton determinization, resulting in more efficient reactive system synthesis.

Contribution

It replaces Safra's determinization with simpler procedures by exploiting automata properties and hierarchy, enhancing practical LTL synthesis efficiency.

Findings

Significant reduction in automaton determinization complexity

Improved synthesis performance demonstrated through experiments

Practical applicability of the new approach confirmed

Abstract

The classic approaches to synthesize a reactive system from a linear temporal logic (LTL) specification first translate the given LTL formula to an equivalent omega-automaton and then compute a winning strategy for the corresponding omega-regular game. To this end, the obtained omega-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 implementations 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 hierarchy consisting of safety, liveness, Buechi, and co-Buechi automata as well as their boolean closures, (2) the non-confluence property of omega-automata that result from certain translations of LTL formulas, 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.