基于代数分析与符号计算的混成系统自动验证

混成系统是一种同时包含连续状态和离散事件的动力系统。随着信息科学的发展，混成系统与人们的日常关系日益密切，促使人们更加关注混成系统的研究。特别地，对混成系统自动验证的研究更是目前国际研究的热点之一。相关的大型项目有德国的AVACS、欧盟的HYCON等。我们在该方向的理论和应用研究中业已取得了不少成果。例如，我们曾通过构造约束条件对非线性混成系统的安全性验证问题进行了直接处理，突破了现有理论通常采用线性近似来处理的局限，并开发了验证软件HSolver。. 本课题将在已有成果上深入研究非线性混成系统自动验证理论及其应用。我们希望在抽象精化、模型检查及Lyapunov稳定下，通过采用安全性和稳定性的代数分析理论和方法，并结合符号计算，在程序化验证混成系统安全性和稳定性的理论与方法等方面取得新的进展，并进行实例研究,如分析运行火车间的碰撞问题、空间飞行器的轨道安全问题、生物系统稳定性问题等。

随着信息科学的快速发展，混成系统研究备受关注。在国家自然科学基金项目的资助下，本项目主要围绕混成系统安全性验证、稳定性分析以及两者的关联性展开研究，在Journal of Symbolic Computation、European Journal of Control等国际期刊以及ISSAC、HSCC等国际会议上共发表标注国家自然科学基金项目资助的学术论文14篇，其中SCI收录6篇，ISTP收录3篇，EI收录3篇（不重复计算），完满地完成了申请书里设定的预期目标。特别地，作为第三完成人参与的“复杂信息系统行为与结构的若干科学问题研究”获2013年度高等学校科学研究优秀成果奖（自然科学奖）一等奖（郑志明、许可、佘志坤等）。. 本项目的主要学术成果可归纳如下：.1)基于递归推理与量词消去，对非线性混成系统的安全性验证问题设计了新的算法，该算法消除了区间算法的“滚雪球”效应，并且对于鲁棒式安全系统的验证是可终止的；基于混成自动机与概率自动机，提出了一种保安全属性的有限概率自动机的普适构造方法，该方法进一步发展了验证概率混成系统安全性的抽象精化理论。美国Vanderbilt大学Prof . X. Koutsoukos对该工作专门写了三页的Discussion。.2)基于符号计算中的实根分类，考虑了多项式Lyapunov函数的自动生成；进一步，结合投影算子，考虑了多重Lyapunov函数的自动生成。与国际上现有的稳定性分析方法相比，我们的基于实根分类的代数方法弥补了线性矩阵不等式法只能处理非退化系统的局限性，克服了平方和分解法的数值不可信性，并降低了普适量词消去的计算复杂性。.3)利用类Lyapunov函数，设计了可迭代生成尽可能大的带目标区域的不变内核的理论框架，并基于平方和方法进行了算法实现。该迭代生成的不变内核可以看成是目标区域的一个吸引域估计，也可以看成由目标区域出发的向后可达集的下近似。特别地，当给定的目标区域为吸引域的一初估计时，与国际上最新方法的比较，我们的数值迭代方法能获得更大的吸引域估计。. 同时，项目负责人积极参与国内外学术合作与交流，并指导博士研究生4名、硕士研究生2名。另外，本项目严格按照《资助计划书》规定的经费预算支出，所有支出范围都严格遵循《国家自然科学基金项目经费管理办法》的规定。