报告人：佘志坤（北京航空航天大学）
邀请人：吴付科
报告时间：2023年7月3日（星期一）10:00-11:30
报告地点：科技楼南楼711室
报告题目：基于Lyapunov函数的随机混成系统稳定性分析与验证
报告摘要：本报告主要关注一类非自治随机混成系统矩指数稳定性的分析和验证问题。该类系统不仅包含由随机微分方程描述的连续流，还包括马尔可夫切换和泊松跳跃。首先，我们利用多重李亚普诺夫函数（MLFs），提出了非线性非自治系统的一致p阶矩指数稳定性的充分必要条件，其中不定的标量函数被用来放松经典MLFs的保守性。然后，对于线性非自治系统，基于我们提出的弱保守保守MLFs和不定标量函数，我们进一步提出了一个由可验证的时变线性矩阵不等式描述的充要条件，以达到系统的一致均方指数稳定性。最后，我们提出了一种基于半定规划的可计算方法，实现了有理系统稳定性的机械化验证。我们通过学术实例说明了理论结果和机械方法的有效性和适用性。
报告人简介：佘志坤，北京航空航天大学教授，博士生导师，教育部新世纪优秀人才，国家级人才类项目获得者和国家高层次人才入选者，中国数学会理事兼数学竞赛委员会副主任及全国大学生数学竞赛工作组组长。主要从事混成系统自动验证、智能系统协同控制等方面的研究。在ACM汇刊、IEEE汇刊、SIAM期刊等国际期刊和CAV、HSCC、AAAI等国际会议上发表学术论文80余篇。研究成果获得包含1位图灵奖获得者、1位哥德尔奖获得者、3位自动推理杰出成就奖获得者、15位院士、20余位ACM/IEEE会士在内的国内外学者的正面评价与引用。由图灵奖获得者Edmund M. Clarke等编著并于2018年出版的《Handbook of Model Checking》在第30章“Verification of Hybrid Systems”的第七节“Verification Tools”介绍了其开发的验证工具HSolver。
