Optimal Assumptions for Synthesis

TL;DR

This paper presents a method to automatically identify the weakest environmental assumptions needed for controller synthesis, improving the robustness and generality of the resulting controllers by leveraging game-theoretic strategies.

Contribution

It introduces an algorithm to compute optimal assumptions ensuring controller existence, based on the correspondence with strongly winning, admissible, and remorsefree strategies.

Findings

Optimal assumptions correspond to strongly winning, admissible, and remorsefree strategies.

The proposed algorithm effectively computes environment-assurable assumptions.

Results improve controller robustness and reduce overly strong assumptions.

Abstract

Controller synthesis is the process of constructing a correct system automatically 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 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 remorsefree strategies respectively. Based on this correspondence, we propose an algorithm for computing optimal assumptions that can be ensured by the environment.