Near-Optimal Reactive Synthesis Incorporating Runtime Information

TL;DR

This paper presents a method for optimal reactive strategy synthesis that incorporates runtime information by pre-synthesizing strategies for different scenarios and switching between them dynamically, ensuring safety and performance.

Contribution

It introduces a novel approach to incorporate real-time information into reactive synthesis without online re-synthesis, using precomputed strategies and a switching mechanism.

Findings

Effective in robotic motion planning with real-time goal likelihood updates

Applicable to urban air mobility air traffic management

Guarantees safety and bounds on performance loss

Abstract

We consider the problem of optimal reactive synthesis - compute a strategy that satisfies a mission specification in a dynamic environment, and optimizes a performance metric. We incorporate task-critical information, that is only available at runtime, into the strategy synthesis in order to improve performance. Existing approaches to utilising such time-varying information require online re-synthesis, which is not computationally feasible in real-time applications. In this paper, we pre-synthesize a set of strategies corresponding to candidate instantiations (pre-specified representative information scenarios). We then propose a novel switching mechanism to dynamically switch between the strategies at runtime while guaranteeing all safety and liveness goals are met. We also characterize bounds on the performance suboptimality. We demonstrate our approach on two examples - robotic motion planning where the likelihood of the position of the robot's goal is updated in real-time, and an air traffic management problem for urban air mobility.