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 speciﬁcation debugging technique for reactive systems and can quickly generate prototype implementations for realizable speciﬁcations. 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 speciﬁcation 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.
Copyright by Springer Verlag. The original publication is available at www.springerlink.com.