Generalized Rabin(1) Synthesis with Applications to Robust System Synthesis

Synthesis of finite-state machines from linear-time temporal logic (LTL) formulas is an important formal specification debugging technique for reactive systems and can quickly generate prototype implementations for realizable specifications.

It has been observed, however, that automatically generated implementations typically do not share the robustness of manually constructed solutions with respect to assumption violations, i.e., they typically do not degenerate nicely when the assumptions in the specification are violated. As a remedy, robust synthesis methods have been proposed. Unfortunately, previous such techniques induced obstacles to their efficient implementation in practice and typically do not scale well.

In this paper, we introduce generalized Rabin(1) synthesis as a solution to this problem. Our approach inherits the good algorithmic properties of generalized reactivity(1) synthesis but extends it to also allow co-Büchi-type assumptions and guarantees, which makes it usable for the synthesis of robust systems.