Verified Compositions of Neural Network Controllers for Temporal Logic Control Objectives

TL;DR

This paper introduces a method to verify and synthesize compositions of neural network controllers that ensure autonomous systems satisfy complex temporal logic tasks, using automata theory and reachability analysis.

Contribution

It presents a novel integration of automata theory with reachability analysis to verify and compose neural network controllers for temporal logic objectives.

Findings

Successfully verified controller compositions for aerial navigation tasks.

Demonstrated the method's applicability to systems with neural network controllers.

Showed the approach can be extended to other controller types with suitable reachability tools.

Abstract

This paper presents a new approach to design verified compositions of Neural Network (NN) controllers for autonomous systems with tasks captured by Linear Temporal Logic (LTL) formulas. Particularly, the LTL formula requires the system to reach and avoid certain regions in a temporal/logical order. We assume that the system is equipped with a finite set of trained NN controllers. Each controller has been trained so that it can drive the system towards a specific region of interest while avoiding others. Our goal is to check if there exists a temporal composition of the trained NN controllers - and if so, to compute it - that will yield composite system behaviors that satisfy a user-specified LTL task for any initial system state belonging to a given set. To address this problem, we propose a new approach that relies on a novel integration of automata theory and recently proposed reachability analysis tools for NN-controlled systems. We note that the proposed method can be applied to other controllers, not necessarily modeled by NNs, by appropriate selection of the reachability analysis tool. We focus on NN controllers due to their lack of robustness. The proposed method is demonstrated on navigation tasks for aerial vehicles.