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.
翻译:用于核实动态系统复杂逻辑规格的一个常见技术是构建象征性的抽象概念:简单、有限状态模型,其行为模仿了感兴趣的系统之一。通常,抽象模型的构建利用了对基本模型的准确知识:在实际应用中,这可能是一个代价高昂的假设。通过抽查未知系统的随机美元/美元-分步轨道,我们根据美元-美元-完整的概念构建了一个抽象概念。我们新定义了概率行为包容的概念,并提供了大致正确的(PAC)保证,即这一抽象概念包括了混凝土系统的所有行为,从有限和无限的时间角度来看,利用假设理论解决非混凝土问题。然后,我们的方法根据数基准进行了测试。