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 $\ell$-step trajectories of an unknown system, we build an abstraction based on the notion of $\ell$-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.

翻译：对动态系统验证复杂逻辑规范的常用技术是构建符号抽象：即行为模拟目标系统的简化有限状态模型。通常，抽象建模需要依赖对底层模型的精确知识——这在现实应用中可能代价高昂。通过采样未知系统的随机$\ell$步轨迹，我们基于$\ell$完备性概念构建抽象模型。新定义了概率行为包含关系，并借助非凸问题的场景理论，为有限和无限时间范围内抽象模型包含具体系统所有行为提供了可能近似正确（PAC）保证。该方法已在多个数值基准测试中得到验证。