# Verified Compositions of Neural Network Controllers for Temporal Logic Control Objectives

arXiv: https://arxiv.org/abs/2209.06130 · HTML: https://mlsanity.com/paper/2209.06130/

## Key facts

- Cited by 4 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 13 Sep 2022.

## Built on by (most cited first, 4 of 4)

- [Conformal Temporal Logic Planning using Large Language Models](https://mlsanity.com/paper/2309.10092/) (2023)
- [Compositional Policy Learning in Stochastic Control Systems with Formal Guarantees](https://mlsanity.com/paper/2312.01456/) (2023)
- [Bridging Deep Reinforcement Learning and Motion Planning for Model-Free Navigation in Cluttered Environments](https://mlsanity.com/paper/2504.07283/) (2025)
- [Verified Compositional Neuro-Symbolic Control for Stochastic Systems with Temporal Logic Tasks](https://mlsanity.com/paper/2311.10863/) (2023)

## Abstract (arXiv)

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.