Verification of Autonomous Systems with Optimal Controllers
For developers of autonomous systems, this work provides a method to verify safety even when optimal controllers may not achieve optimality, but the evaluation is limited to two simple examples.
This paper addresses the challenge of verifying safety and correctness of autonomous systems using optimal controllers, particularly when optimal solutions are not always found due to computational constraints. The proposed reachability algorithm, which models gradient descent as a separate dynamical system, is evaluated on a quadrotor and a cartpole, demonstrating feasibility.
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.