《多项式混成系统不变式生成》由会员分享,可在线阅读,更多相关《多项式混成系统不变式生成(28页珍藏版)》请在金锄头文库上搜索。
1、多项式混成系统不变式生成多项式混成系统不变式生成报告人:赵恒军中国科学院软件研究所计算机科学国家重点实验室 2012年11月4日主要内容背景介绍微分不变式判别准则和计算方法应用主要内容背景介绍微分不变式判别准则和计算方法应用系统分类离散:x:=1;while (x0, t0t判别准则dx/dt=f(x), f(x)多项式p(x) 0, p(x)多项式p(x)=0边界dp(x(t)/dtp(x) 00判别准则dp/dx=0p(x) 0=0完备判别准则dp/dt=0d2p/dt2 0,=0d3p/dt3 0,=0 上界N(p,f)Liu Jiang, Zhan Naijun, Zhao Hengj
2、un: Computing semi-algebraic invariants for polynomial dynamical systems. In: EMSOFT11. pp. 97106. ACM, New York, NY, USA (2011)p(x) 0计算方法设定模板 p(u,x)=0p=0(dp/dt0 /dp/dt=0 / d2p/dt2 0 /dp/dt=0 / d2p/dt2=0 / d3p/dt3=0 /dp/dt=0/./ dNp/dtN 0 )Forall x. (u,x)量词消去,SOS,混成一族微分不变式初始状态关于迁移关系一致不变式蕴含安全性质f3f1f2应用背景介绍微分不变式判别准则和计算方法应用例例总结混成系统包含连续与离散行为(归纳)不变式与安全性验证多项式连续系统微分不变式生成完备的判别准则多项式混成系统不变式生成存在的问题多项式系统的局限模板的设定依赖于经验极高的复杂性谢谢!