一类非线性混合自动机的离散化验证

施枫

摘要：混合系统是同时包含有相互作用的连续性子系统和离散性子系统的一类动态系统。混合自动机是目前混合系统验证研究中最常用的一种形式化模型。由于混合自动机连续变量的复杂性以及连续变量和离散变量的相互作用性，对混合自动机的可达集的计算一直是一个复杂而难以解决的问题。该文提出了在连续时间下针对一类非线性混合自动机的离散化验证算法，通过求出混合自动机每次发生离散迁移之后，在新的控制模式下的可達集的区域近似极值来解决该文所研究的问题。实验结果表明，该文提出的算法可以有效地对连续时间下的一类非线性混合自动机所代表的混合系统的部分性质进行验证。

关键词：混合自动机；离散化验证；计算树逻辑；连续变量；形式化验证