Synthesizing Optimally Resilient Controllers

TL;DR

This paper extends the computation of optimally resilient strategies from safety to a broader class of winning conditions, maintaining efficiency and memory bounds, with implications for robust controller synthesis.

Contribution

It introduces algorithms for computing optimally resilient strategies for various winning conditions, including parity, with polynomial overhead and no additional memory requirements.

Findings

Strategies for parity conditions are positional.

Algorithms operate in quasipolynomial time.

Resilient strategies do not require more memory than classical strategies.

Abstract

Recently, Dallal, Neider, and Tabuada studied a generalization of the classical game-theoretic model used in program synthesis, which additionally accounts for unmodeled intermittent disturbances. In this extended framework, one is interested in computing optimally resilient strategies, i.e., strategies that are resilient against as many disturbances as possible. Dallal, Neider, and Tabuada showed how to compute such strategies for safety specifications. In this work, we compute optimally resilient strategies for a much wider range of winning conditions and show that they do not require more memory than winning strategies in the classical model. Our algorithms only have a polynomial overhead in comparison to the ones computing winning strategies. In particular, for parity conditions, optimally resilient strategies are positional and can be computed in quasipolynomial time.