# Data-driven Abstractions for Verification of Deterministic Systems

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

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 3 Nov 2022.

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

- [Reinforcement Learning for Robust Ageing-Aware Control of Li-ion Battery Systems with Data-Driven Formal Verification](https://mlsanity.com/paper/2509.04288/) (2025)
- [S3: A Smooth Simulation Surrogate for Optimizing Discrete Abstractions of Dynamical Systems](https://mlsanity.com/paper/2608.15920/) (2026)

## Abstract (arXiv)

A common technique to verify complex logic specifications for dynamical systems is the construction of symbolic abstractions: simpler, finite-state models whose behaviour mimics the one of the systems of interest. Typically, abstractions are constructed exploiting an accurate knowledge of the underlying model: in real-life applications, this may be a costly assumption. By sampling random ℓ-step trajectories of an unknown system, we build an abstraction based on the notion of ℓ-completeness. We newly define the notion of probabilistic behavioural inclusion, and provide probably approximately correct (PAC) guarantees that this abstraction includes all behaviours of the concrete system, for finite and infinite time horizon, leveraging the scenario theory for non convex problems. Our method is then tested on several numerical benchmarks.