# Verified Compositional Neuro-Symbolic Control for Stochastic Systems with Temporal Logic Tasks

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 26 of its 47 references that are in the map.
- First posted on arXiv 17 Nov 2023.

## Builds on (most cited first, 26 of 26)

- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical Systems](https://mlsanity.com/paper/2004.05519/) (2020)
- [Safety Verification and Robustness Analysis of Neural Networks via Quadratic Constraints and Semidefinite Programming](https://mlsanity.com/paper/1903.01287/) (2019)
- [Reachability Analysis of Deep Neural Networks with Provable Guarantees](https://mlsanity.com/paper/1805.02242/) (2018)
- [Reinforcement Learning for Temporal Logic Control Synthesis with Probabilistic Satisfaction Guarantees](https://mlsanity.com/paper/1909.05304/) (2019)
- [Omega-Regular Objectives in Model-Free Reinforcement Learning](https://mlsanity.com/paper/1810.00950/) (2018)
- [Control Synthesis from Linear Temporal Logic Specifications using Model-Free Reinforcement Learning](https://mlsanity.com/paper/1909.07299/) (2019)
- [Compositional Reinforcement Learning from Logical Specifications](https://mlsanity.com/paper/2106.13906/) (2021)
- [Formal Verification of Neural Network Controlled Autonomous Systems](https://mlsanity.com/paper/1810.13072/) (2018)
- [Enforcing robust control guarantees within neural network policies](https://mlsanity.com/paper/2011.08105/) (2020)
- [Scalable Quantitative Verification For Deep Neural Networks](https://mlsanity.com/paper/2002.06864/) (2020)
- [Reinforcement Learning with Probabilistic Guarantees for Autonomous Driving](https://mlsanity.com/paper/1904.07189/) (2019)
- [STyLuS*: A Temporal Logic Optimal Control Synthesis Algorithm for Large-Scale Multi-Robot Systems](https://mlsanity.com/paper/1809.08345/) (2018)
- [Reinforcement Learning Based Temporal Logic Control with Maximum Probabilistic Satisfaction](https://mlsanity.com/paper/2010.06797/) (2020)
- [Formal Controller Synthesis for Continuous-Space MDPs via Model-Free Reinforcement Learning](https://mlsanity.com/paper/2003.00712/) (2020)
- [Verifiable and Compositional Reinforcement Learning Systems](https://mlsanity.com/paper/2106.05864/) (2021)
- [A Simple and Efficient Sampling-based Algorithm for General Reachability Analysis](https://mlsanity.com/paper/2112.05745/) (2021)
- [LCRL: Certified Policy Synthesis via Logically-Constrained Reinforcement Learning](https://mlsanity.com/paper/2209.10341/) (2022)
- [A Classification-based Approach for Approximate Reachability](https://mlsanity.com/paper/1803.03237/) (2018)
- [Accelerated Reinforcement Learning for Temporal Logic Control Objectives](https://mlsanity.com/paper/2205.04424/) (2022)
- [DeepSplit: Scalable Verification of Deep Neural Networks via Operator Splitting](https://mlsanity.com/paper/2106.09117/) (2021)
- [Fast Decomposition of Temporal Logic Specifications for Heterogeneous Teams](https://mlsanity.com/paper/2010.00030/) (2020)
- [Robustness to Adversarial Attacks in Learning-Enabled Controllers](https://mlsanity.com/paper/2006.06861/) (2020)
- [Verified Compositions of Neural Network Controllers for Temporal Logic Control Objectives](https://mlsanity.com/paper/2209.06130/) (2022)
- [Technical Report: Reactive Planning for Mobile Manipulation Tasks in Unexplored Semantic Environments](https://mlsanity.com/paper/2011.00642/) (2020)
- [A hybrid barrier certificate approach to satisfy linear temporal logic specifications](https://mlsanity.com/paper/2011.11464/) (2020)

## Abstract (arXiv)

Several methods have been proposed recently to learn neural network (NN) controllers for autonomous agents, with unknown and stochastic dynamics, tasked with complex missions captured by Linear Temporal Logic (LTL). Due to the sample-inefficiency of the majority of these works, compositional learning methods have been proposed decomposing the LTL specification into smaller sub-tasks. Then, separate controllers are learned and composed to satisfy the original task. A key challenge within these approaches is that they often lack safety guarantees or the provided guarantees are impractical. This paper aims to address this challenge. Particularly, we consider autonomous systems with unknown and stochastic dynamics and LTL-encoded tasks. We assume that the system is equipped with a finite set of base skills modeled by trained NN feedback controllers. 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 a composite system behavior that satisfies the assigned LTL task with probability one. We propose a new approach that relies on a novel integration of automata theory and data-driven reachability analysis tools for NN-controlled stochastic systems. The resulting neuro-symbolic controller allows the agent to generate safe behaviors for unseen complex temporal logic tasks in a zero-shot fashion by leveraging its base skills. We show correctness of the proposed method and we provide conditions under which it is complete. To the best of our knowledge, this is the first work that designs verified temporal compositions of NN controllers for unknown and stochastic systems. Finally, we provide extensive numerical simulations and hardware experiments on robot navigation tasks to demonstrate the proposed method.