Sciweavers

Share
NFM
2011

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

8 years 1 months ago
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¨uchi-type assumptions and guarantees, which makes i...
Rüdiger Ehlers
Added 14 May 2011
Updated 14 May 2011
Type Journal
Year 2011
Where NFM
Authors Rüdiger Ehlers
Comments (0)
books