abstraction-mpc-integration

The deployment of autonomous systems in safety-critical environments requires control policies that guarantee satisfaction of complex objectives. These systems are commonly modeled as nonlinear discrete-time stochastic systems. A popular approach to computing provably-correct policies is to construct a finite-state abstraction, often represented as a Markov decision process (MDP) with intervals of transition probabilities (IMDP). However, existing abstraction techniques compute a single policy, thus leaving no room for online cost/performance optimization, e.g., of energy consumption. To overcome this limitation, we propose a novel IMDP abstraction technique in which every abstract action corresponds to a set of inputs for the original system. Hence, an abstract policy leads to a set of provably-correct policies for the concrete system, each of which satisfies the control objective with at least the same probability as the abstract policy. We can thus search through this set of verified policies with an online control algorithm, namely model predictive control (MPC), to minimize a desired cost function online, while retaining the guaranteed satisfaction probability of the entire policy set. Our experiments demonstrate that our approach yields better control performance than state-of-the-art single-policy abstraction techniques, with a small degradation of the guarantees.