Verification of Autonomous Systems with Optimal Controllers

TL;DR

This paper develops a reachability analysis method for control systems with optimal controllers, using gradient descent as a dynamical system to verify safety and correctness despite optimization challenges.

Contribution

It introduces a novel reachability algorithm that models gradient descent as a dynamical system embedded in the control system for verification purposes.

Findings

Feasibility demonstrated on a 2D quadrotor.

Feasibility demonstrated on a cartpole system.

Method addresses verification under optimization constraints.

Abstract

This paper considers the problem of reachability analysis of control systems with optimal controllers, as a first step towards verifying the safety and correctness of such systems. Despite their appeal in guaranteeing task satisfaction through cost minimization, optimal controllers are often challenging to assure. In particular, as system dynamics grow in complexity, solving the resulting optimization problem may be difficult, especially given time and computation constraints on real platforms. Thus, it is essential to verify that, even if the optimal solution is not always found, such controllers still accomplish the high-level control objective. In this paper, we focus on gradient descent algorithms and design a reachability algorithm by treating gradient descent as a separate (digital) dynamical system, embedded in the original (physical) dynamical system, with controls as part of the state. We evaluate the feasibility of the proposed method on two control systems, a two-dimensional quadrotor and a cartpole.