Sandboxing (AI-based) Unverified Controllers in Stochastic Games: An Abstraction-based Approach with Safe-visor Architecture

TL;DR

This paper introduces a formal framework for sandboxing unverified AI controllers in stochastic games using an abstraction-based Safe-visor architecture that guarantees safety while utilizing the controller's functionality.

Contribution

It proposes a novel abstraction-based Safe-visor architecture with formal safety guarantees for unverified controllers in stochastic games.

Findings

Successfully applied to quadrotor control with AI-based unverified controllers.

Provides formal safety guarantees via probabilistic relations.

Demonstrates effectiveness in a real-world control scenario.

Abstract

In this paper, we propose a construction scheme for a Safe-visor architecture for sandboxing unverified controllers, e.g., artificial intelligence-based (a.k.a. AI-based) controllers, in two-players non-cooperative stochastic games. Concretely, we leverage abstraction-based approaches to construct a supervisor that checks and decides whether or not to accept the inputs provided by the unverified controller, and a safety advisor that provides fallback control inputs to ensure safety whenever the unverified controller is rejected. Moreover, by leveraging an ($\epsilon,\delta$)-approximate probabilistic relation between the original game and its finite abstraction, we provide a formal safety guarantee with respect to safety specifications modeled by deterministic finite automata (DFA), while the functionality of the unverified controllers is still exploited. To show the effectiveness of the proposed results, we apply them to a control problem of a quadrotor tracking a moving ground vehicle, in which an AI-based unverified controller is employed to control the quadrotor.