AI 中文总结
本综述针对复杂动态系统，梳理了三类数据驱动形式化方法及其保障类型，重点关注确定性与随机系统的差异，填补了现有研究零散的空白。
AI 中文摘要
近期，具备形式化保障的数据驱动方法已成为对复杂动态系统进行验证与控制器综合的有力手段。这类方法的关注度正迅速提升，因为在实际场景中往往无法获取系统模型，且非线性行为、不确定性以及维度灾难等挑战通常会导致精确建模难以实现。这些困难促使人们利用从系统收集的有限数据，同时仍能对其整体行为提供形式化保障。因此，该领域已提出数百篇文章，用于开发无需显式模型即可对动态系统进行形式化验证与综合的数据驱动框架，以处理超越稳定性的复杂规范。尽管发展迅速，现有成果仍较为零散，缺乏连贯的组织，这限制了人们对其原理、区别和实际潜力的清晰理解。本综述通过对确定性和随机动态系统的数据驱动方法进行全面概述，填补了这一空白。我们围绕形式化方法的三个主要方法论支柱组织文献：基于（有限/无限）抽象的技术、诸如控制障碍证书之类的函数证书方法，以及组合方法。对于每种方法，我们将所得的数据驱动保障分为三类：（i）基于可能近似正确（PAC）和场景框架的统计保障；（ii）源自利普希茨连续性的保障；（iii）利用结构特性的保障。尽管关于确定性系统的文献丰富得多，但我们也特别关注随机对应情况，强调其与确定性情况相比所固有的差异和挑战。
英文摘要
Data-driven approaches with formal guarantees have recently emerged as a powerful means for the verification and controller synthesis of complex dynamical systems. Interest in these methods is rapidly growing, as system models are often unavailable in practice, and challenges such as nonlinear behavior, uncertainty, and the curse of dimensionality typically render accurate modeling infeasible. These difficulties motivate leveraging limited data collected from the system while still providing formal guarantees on its overall behavior. The community has therefore proposed a few hundred articles on the development of data-driven frameworks that enable the formal verification and synthesis of dynamical systems without explicit models, addressing complex specifications beyond stability. Despite this rapid growth, existing results remain scattered and lack a coherent organization, limiting a clear understanding of their principles, distinctions, and practical potential. This survey fills this gap by providing a comprehensive overview of these data-driven methods for both deterministic and stochastic dynamical systems. We structure the literature around three main methodological pillars in formal methods: (in)finite-abstraction-based techniques, functional certificate approaches, such as control barrier certificates, and compositional methods. For each of these approaches, we classify the resulting data-driven guarantees into three main categories: (i) statistical guarantees grounded in probably approximately correct and scenario-based frameworks, (ii) guarantees derived from Lipschitz continuity, and (iii) guarantees exploiting structural properties. While the literature on deterministic systems is considerably richer, we also devote particular attention to the stochastic counterpart, highlighting the inherent differences and challenges that arise compared to the deterministic case.
CommentsThe proposal for this survey paper has been accepted at Automatica
