mlsanityData to 14 Oct 2026

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

arXiv 2311.10863 ↗First posted 17 Nov 2023cs.RO cs.AI cs.LGcited by 0

Not on the map. Why?

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.

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

26 of 47 references.

References · 26

  1. 2017Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networkscited by 744
  2. 2020NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical Systemscited by 128
  3. 2019Safety Verification and Robustness Analysis of Neural Networks via Quadratic Constraints and Semidefinite Programmingcited by 101
  4. 2018Reachability Analysis of Deep Neural Networks with Provable Guaranteescited by 93
  5. 2019Reinforcement Learning for Temporal Logic Control Synthesis with Probabilistic Satisfaction Guaranteescited by 77
  6. 2018Omega-Regular Objectives in Model-Free Reinforcement Learningcited by 75
  7. 2019Control Synthesis from Linear Temporal Logic Specifications using Model-Free Reinforcement Learningcited by 75
  8. 2021Compositional Reinforcement Learning from Logical Specificationscited by 67
  9. 2018Formal Verification of Neural Network Controlled Autonomous Systemscited by 41
  10. 2020Enforcing robust control guarantees within neural network policiescited by 40
  11. 2020Scalable Quantitative Verification For Deep Neural Networkscited by 31
  12. 2019Reinforcement Learning with Probabilistic Guarantees for Autonomous Drivingcited by 28
14 more
  1. 2018STyLuS*: A Temporal Logic Optimal Control Synthesis Algorithm for Large-Scale Multi-Robot Systemscited by 24
  2. 2020Reinforcement Learning Based Temporal Logic Control with Maximum Probabilistic Satisfactioncited by 22
  3. 2020Formal Controller Synthesis for Continuous-Space MDPs via Model-Free Reinforcement Learningcited by 15
  4. 2021Verifiable and Compositional Reinforcement Learning Systemscited by 13
  5. 2021A Simple and Efficient Sampling-based Algorithm for General Reachability Analysiscited by 12
  6. 2022LCRL: Certified Policy Synthesis via Logically-Constrained Reinforcement Learningcited by 11
  7. 2018A Classification-based Approach for Approximate Reachabilitycited by 10
  8. 2022Accelerated Reinforcement Learning for Temporal Logic Control Objectivescited by 9
  9. 2021DeepSplit: Scalable Verification of Deep Neural Networks via Operator Splittingcited by 8
  10. 2020Fast Decomposition of Temporal Logic Specifications for Heterogeneous Teamscited by 5
  11. 2020Robustness to Adversarial Attacks in Learning-Enabled Controllerscited by 4
  12. 2022Verified Compositions of Neural Network Controllers for Temporal Logic Control Objectivescited by 4
  13. 2020Technical Report: Reactive Planning for Mobile Manipulation Tasks in Unexplored Semantic Environmentscited by 3
  14. 2020A hybrid barrier certificate approach to satisfy linear temporal logic specificationscited by 2

Built on by

Not cited yet.