05930523

a

05930523 Ehlers, R\"udiger Generalized Rabin(1) synthesis with applications to robust system synthesis. Bobaru, Mihaela (ed.) et al., NASA formal methods. Third international symposium, NFM 2011, Pasadena, CA, USA, April 18--20, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-20397-8/pbk). Lecture Notes in Computer Science 6617, 101-115 (2011). 2011 Berlin: Springer EN

doi:10.1007/978-3-642-20398-5_9

Summary: 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 it usable for the synthesis of robust systems.