Temporal Logic Control of Nonlinear Stochastic Systems with Online Performance Optimization

TL;DR

This paper introduces a new abstraction method for nonlinear stochastic systems that generates multiple verified policies, enabling online optimization like MPC to improve control performance while maintaining safety guarantees.

Contribution

It proposes a novel interval MDP abstraction technique that produces a set of policies, allowing online performance optimization without sacrificing safety guarantees.

Findings

Better control performance than existing single-policy methods.

Maintains guaranteed satisfaction probability for all policies in the set.

Enables online optimization such as MPC for cost reduction.

Abstract

The deployment of autonomous systems in safety-critical environments requires control policies that guarantee satisfaction of complex control specifications. These systems are commonly modeled as nonlinear discrete-time stochastic systems. A~popular approach to computing a policy that provably satisfies a complex control specification is to construct a finite-state abstraction, often represented as a Markov decision process (MDP) with intervals of transition probabilities, i.e., an interval MDP (IMDP). However, existing abstraction techniques compute a \emph{single policy}, thus leaving no room for online cost or performance optimization, e.g., of energy consumption. To overcome this limitation, we propose a novel IMDP abstraction technique that yields a \emph{set of policies}, each of which satisfies the control specification with a certain minimum probability. We can thus use any online control algorithm to search through this set of verified policies while retaining the guaranteed satisfaction probability of the entire policy set. In particular, we employ model predictive control (MPC) to minimize a desired cost function that is independent of the control specification considered in the abstraction. 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.