摘要：Controller synthesis is the automatic construction a correct system from its specification. This often requires assumptions about the behaviour of the environment. It is difficult for the designer to identify the assumptions that ensures the existence of a correct controller, and doing so manually can lead to assumptions that are stronger than necessary. As a consequence the generated controllers are suboptimal in terms of robustness. In this work, given a specification, we identify the weakest assumptions that ensure the existence of a controller. We also consider two important classes of assumptions: the ones that can be ensured by the environment and assumptions that restricts only inputs of the systems. We show that optimal assumptions correspond to strongly winning strategies, admissible strategies and remorse-free strategies depending on the classes. Using these correspondences, we then propose an algorithm for computing optimal assumptions that can be ensured by the environment.
