A Compositional Framework for Controller Synthesis

The focus of this seminar talk will be a general framework for the compositional synthesis of controllers for partially observable and partially controllable systems. For compositionality it is crucial that the controllers are as permissive as possible, as they have to ensure that legal choices for subsequent controllers are not ruled out prematurely. We present a novel notion of strategies and controllers that allows the compositional synthesis of such most general controllers and provide algorithms for their construction for omega-regular objectives. We furthermore demonstrate our approach in a setting of exogenous coordination based on Reo and constraint automata and present practical results gained by the implementation in our modeling and verification tool Vereofy.