Robustness-by-Construction Synthesis: Adapting to the Environment at Runtime

TL;DR

The paper tackles robustness in reactive synthesis by adopting a robust-LTL ($\mathrm{rLTL}$) framework that assigns a quantitative, many-valued truth to specifications. It introduces two runtime-adaptive strategy concepts—adaptive strategies and strongly adaptive strategies—to exploit non-antagonistic environment moves, achieving better satisfaction levels at runtime via automata-based monitoring and parity-game reductions. Both strategies are shown to be computable in doubly-exponential time, and adaptive strategies exist universally while strongly adaptive strategies may not, with a method to decide and compute them when possible. The work thus shows that robust-by-construction synthesis does not incur worse asymptotic complexity than classical $\mathrm{LTL}$ synthesis and grounds the approach in automata-theoretic and game-theoretic techniques for practical reactive-system design.

Abstract

While most of the current synthesis algorithms only focus on correctness-by-construction, ensuring robustness has remained a challenge. Hence, in this paper, we address the robust-by-construction synthesis problem by considering the specifications to be expressed by a robust version of Linear Temporal Logic (LTL), called robust LTL (rLTL). rLTL has a many-valued semantics to capture different degrees of satisfaction of a specification, i.e., satisfaction is a quantitative notion. We argue that the current algorithms for rLTL synthesis do not compute optimal strategies in a non-antagonistic setting. So, a natural question is whether there is a way of satisfying the specification "better" if the environment is indeed not antagonistic. We address this question by developing two new notions of strategies. The first notion is that of adaptive strategies, which, in response to the opponent's non-antagonistic moves, maximize the degree of satisfaction. The idea is to monitor non-optimal moves of the opponent at runtime using multiple parity automata and adaptively change the system strategy to ensure optimality. The second notion is that of strongly adaptive strategies, which is a further refinement of the first notion. These strategies also maximize the opportunities for the opponent to make non-optimal moves. We show that computing such strategies for rLTL specifications is not harder than the standard synthesis problem, e.g., computing strategies with LTL specifications, and takes doubly-exponential time.