hybrid:混合系统的近似概率验证

混合系统的近似概率验证 介绍 这是非线性混合系统的近似概率验证方法的 MATLAB 实现。 系统动力学由离散模式和连续常微分方程的组合描述，这些方程控制每个模式中状态变量的时间演变。 模式之间的转换受保护措施限制，保护措施以状态变量的当前值为条件。 为了验证模型是否满足有界线性时间时序逻辑 (BLTL) 属性，我们使用概率近似技术，并根据 [1] 的算法 1 构建依赖于重复轨迹模拟的统计模式检查 (SMC) 方案。 系统是否满足该性质作为假设检验并根据 [1] 的算法 2 确定。 模型构建 模型表示为具有以下字段的结构。 nstates：模型的状态变量数 nmodes：模型的模式数 mode0：初始模式的索引（介于 1 和 nmodes 之间） x0：一个大小为 (nstates,2) 的矩阵，每行包含一个状态变量的初始条件的下限和上限 模式：具有 nmodes 元素的模式结构向量