随着信息技术向高性能和智能化方向的发展,处理新生现实物理问题的计算技术应运而生。混杂系统是一种强有力的描述模型。国内外同行对它的发展一贯高度关注,分析与验证工作也十分活跃。目前常用的方法是基于逻辑演算的,往往无法有效处理与时间有关的系统模型。而符号计算是建立在实代数理论上、以绝对准确为目标的,将是解决该难点的有效途径。我们团队在自然科学基金重大研究计划的支持下,从事该相关领域研究有两年多的经验积累,已在线性系统可达性问题上取得了一些成绩。本项目拟以符号计算为主要手段,对一般混杂系统的可达性作进一步深入研究;同时带动对新产生的广义多项式系统进行符号求解方法的发展。计划还包括研制相应的符号验证程序包;并应用于有代表性的安全攸关系统中,如轨道交通的碰撞避免,力图获得一些新的结果。
symbolic computation;hybrid systems;nonlinear systems;reachability analysis;
混杂系统分析与验证是信息物理融合系统领域的研究热点之一。计算机符号计算方法以绝对准确为首要目标,正是有效验证混杂系统的重要途径。本项目基于符号计算方法,研究了混杂系统中若干典型非线性微分方程、非线性差分方程的可达状态集、不变式、零点集等问题。由这些问题驱动,发展了一些新产生的广义多项式系统准确求解、量词消去算法。这些成果已部分扩充到专用验证工具包REACH中。有些成果还在概率模型检测、系统生物学等领域中得到成功运用。因此,本项目所发展起来的理论方法和软件工具将为信息物理融合系统的发展产生积极推进作用。依托项目支持,我们目前完成学术论文10余篇,其中已正式出版或录用7篇,均被SCI检索;培养博士研究生3名(毕业2名、在读1名)。