一类非线性混成系统的建模与面向路径的可达性分析方法

摘要

本发明提出一类非线性混成系统的建模与面向路径的可达性分析方法，步骤1：对非线性混成系统进行建模，得到非线性混成自动机；步骤2：判断非线性混成自动机的凸性混成；当混成自动机每一个节点上的状态空间都为凸集时，称该混成自动机为凸性混成自动机；步骤3：若为凸性混成自动机，则根据规则将待验证可达性问题编码为凸规划问题进行求解；对于编码后的凸规划问题，若该问题有解，则对应的路径满足可达性规约；最后针对其面向路径的可达性问题，给出将其可达性问题编码为凸规划可满足性问题的方法，并通过求解凸规划问题，给出半判定过程；本发明给出了凸性混成自动机的可达性分析，相对于基于近似和抽象的分析方法，有更好的效果。

主权项

一类非线性混成系统的建模与面向路径的可达性分析方法，其特征在于，步骤1：对非线性混成系统进行建模，得到非线性混成自动机；对于混成系统的连续状态变化，用混成自动机的节点描述；对于混成系统的离散状态变化，用混成自动机节点之间的状态迁移来描述；其中，初始节点描述混成自动机的初始状态；步骤2：判断非线性混成自动机的凸性混成；当混成自动机每一个节点上的状态空间都为凸集时，称该混成自动机为凸性混成自动机；步骤3：若为凸性混成自动机，则根据规则将待验证可达性问题编码为凸规划问题进行求解；对于编码后的凸规划问题，若该问题有解，则对应的路径满足可达性规约；若该问题无解，则对应的路径不满足可达性规约、即无法得到路径是否满足可达性规约；否则问题不可判定，放弃求解；步骤4：求解编码后的凸规划问题；步骤5：若问题可解，则说明当前求解路径满足可达性规约；否则，分别判断凸性混成自动机是否属于以下子类：线性流凸性混成自动机，要求凸性混成自动机所有节点上的流条件（Flow Condition）都是线性的，也即是自动机中所有连续状态变化的变化率都是线性的；单调不变式凸性混成自动机，要求凸性混成自动机上的不变式f(x)对于时间变量t都是单调的；步骤6：若凸性混成自动机属于上述子类中的任何一个，则说明当前求解路径不满足可达性规约；否则问题不可判定，放弃求解。