Abstraction refinement for attractivity controllers using quantitative synthesis

International audienceAttractivity specifications consist in driving the state of a system to a target region and to keep it in that region afterwards. In this paper, we develop an approach to controller synthesis for attractivity specifications based on iterative refinements of symbolic abstractions. We compute iteratively sequences of least-violating attractivity controllers and of associated attractors. The current controller is used to restrict possible control actions at the next iteration where a new abstraction is used following a local refinement applied inside the current attractor. The approach results in a nested sequence of attractors which are closer to the target region at each iteration. To illustrate the effectiveness of our approach, we show an application to a marine vessel system