Optimal Assumptions for Synthesis

Synthesis is the process of constructing a correct system automatically from its specification. For reactive systems, 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 sub-optimal in terms of generality and robustness. In this work, given a specification, we identify the weakest assumptions that ensures 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 speaks only about inputs of the systems. We show that optimal assumptions correspond to strongly winning strategies, admissible strategies and remorse-free strategies respectively. Based on this correspondence, we propose an algorithm for computing optimal assumptions that can be ensured by the environment.

Authors

• Romain Brenguier

Keywords

No keywords are indexed for this paper.