# Data-Driven Abstraction-Based Control Synthesis

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

## Key facts

- Cited by 8 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 16 Jun 2022.

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

- [Data-Driven Distributionally Robust Safety Verification Using Barrier Certificates and Conditional Mean Embeddings](https://mlsanity.com/paper/2403.10497/) (2024)
- [Data-Driven Abstractions via Binary-Tree Gaussian Processes for Formal Verification](https://mlsanity.com/paper/2407.21029/) (2024)
- [Neural Abstraction-Based Controller Synthesis and Deployment](https://mlsanity.com/paper/2307.03783/) (2023)
- [Average Reward Reinforcement Learning for Omega-Regular and Mean-Payoff Objectives](https://mlsanity.com/paper/2505.15693/) (2025)
- [Data-Driven Probabilistic Evaluation of Logic Properties with PAC-Confidence on Mealy Machines](https://mlsanity.com/paper/2508.14710/) (2025)
- [Kernel-Based Learning of Safety Barriers](https://mlsanity.com/paper/2601.12002/) (2026)
- [k-Inductive Neural Barrier Certificates for Unknown Nonlinear Dynamics](https://mlsanity.com/paper/2605.20108/) (2026)
- [Safe Deep Reinforcement Learning for Energy-Efficient HVAC Control in Multi-Zone Residential Buildings](https://mlsanity.com/paper/2608.17235/) (2026)

## Abstract (arXiv)

This paper studies formal synthesis of controllers for continuous-space systems with unknown dynamics to satisfy requirements expressed as linear temporal logic formulas. Formal abstraction-based synthesis schemes rely on a precise mathematical model of the system to build a finite abstract model, which is then used to design a controller. The abstraction-based schemes are not applicable when the dynamics of the system are unknown. We propose a data-driven approach that computes the growth bound of the system using a finite number of trajectories. The growth bound together with the sampled trajectories are then used to construct the abstraction and synthesise a controller. Our approach casts the computation of the growth bound as a robust convex optimisation program (RCP). Since the unknown dynamics appear in the optimisation, we formulate a scenario convex program (SCP) corresponding to the RCP using a finite number of sampled trajectories. We establish a sample complexity result that gives a lower bound for the number of sampled trajectories to guarantee the correctness of the growth bound computed from the SCP with a given confidence. We also provide a sample complexity result for the satisfaction of the specification on the system in closed loop with the designed controller for a given confidence. Our results are founded on estimating a bound on the Lipschitz constant of the system and provide guarantees on satisfaction of both finite and infinite-horizon specifications. We show that our data-driven approach can be readily used as a model-free abstraction refinement scheme by modifying the formulation of the growth bound and providing similar sample complexity results. The performance of our approach is shown on three case studies.