In this work, we propose a data-driven approach for the stability analysis of discrete-time homogeneous nonlinear systems with unknown models. The proposed framework is based on constructing Lyapunov functions via a set of data, collected from trajectories of unknown systems, while providing an a-priori guaranteed confidence on the stability of the system. In our data-driven setting, we first cast the original stability problem as a robust optimization program (ROP). Since unknown models appear in the constraint of the proposed ROP, we collect a finite number of data from trajectories of unknown systems and provide two variants of scenario optimization program (SOP) associated to the original ROP. We discuss that the proposed ROP, and its corresponding SOPs, are not convex due to having a bilinearity between decision variables. We also show that while one of the proposed SOPs is more efficient in terms of computational complexity, the other one provides Lyapunov functions with a much better performance for the original ROP. We then establish a probabilistic closeness between the optimal value of (non-convex) SOP and that of ROP, and subsequently, formally provide the stability guarantee for unknown systems with a guaranteed confidence level. We illustrate the efficacy of our proposed results by applying them to two physical case studies with unknown dynamics including (i) a DC motor and (ii) a (homogeneous) nonlinear jet engine compressor. We collect data from trajectories of unknown systems and verify their global asymptotic stability (GAS) with desirable confidence levels.@en

This report presents the results of a friendly competition for formal verification and policy synthesis of stochastic models. It also introduces new benchmarks and their properties within this category and recommends next steps for this category towards next year’s edition of the competition. In comparison with tools on non-probabilistic models, the tools for stochastic models are at the early stages of development that do not allow full competition on a standard set of benchmarks. We report on an initiative to collect a set of minimal benchmarks that all such tools can run, thus facilitating the comparison between efficiency of the implemented techniques. The friendly competition took place as part of the workshop Applied Verification for Continuous and Hybrid Systems (ARCH) in Summer 2022.@en

This report presents the results of a friendly competition for formal verification and policy synthesis of stochastic models. It also introduces new benchmarks within this category, and recommends next steps for this category towards next year's edition of the competition. The friendly competition took place as part of the workshop Applied Verification for Continuous and Hybrid Systems (ARCH) in Spring/Summer 2020.@en

Abstract This report is concerned with a friendly competition for formal verification and policy synthesis of stochastic models. The main goal of the report is to introduce new benchmarks and their properties within this category and recommend next steps toward next year’s edition of the competition. Given that the tools for stochastic models are at their early stages of development compared to those of non-probabilistic models, the main focus is to report on an initiative to collect a set of minimal benchmarks that all such tools can run, thus facilitating the comparison between the efficiency of the implemented techniques. This friendly competition took place as part of the workshop Applied Verification for Continuous and Hybrid Systems (ARCH) in Summer 2023.@en