End-to-End Statistical Model Checking for Parameterization and Stability Analysis of ODE Models
提出一种基于仿真的技术，用于参数化常微分方程并分析其稳定性，通过统计模型检验估计参数或初始条件变化下满足给定属性的概率，并给出统计保证。
We propose a simulation-based technique for the parameterization and the stability analysis of parametric Ordinary Differential Equations. This technique is an adaptation of Statistical Model Checking, often used to verify the validity of biological models, to the setting of Ordinary Differential Equations systems. The aim of our technique is to estimate the probability of satisfying a given property under the variability of the parameter or initial condition of the ODE, with any metrics of choice. To do so, we discretize the values space and use statistical model checking to evaluate each individual value w.r.t. provided data. Contrary to other existing methods, we provide statistical guarantees regarding our results that take into account the unavoidable approximation errors introduced through the numerical integration of the ODE system performed while simulating. In order to show the potential of our technique, we present its application to two case studies taken from the literature, one relative to the growth of a jellyfish population, and the other concerning a well-known oscillator model.