多项式混成系统不变式生成.pptVIP

多项式混成系统不变式生成第一页，共二十八页，2022年，8月28日 主要内容背景介绍微分不变式判别准则和计算方法应用第二页，共二十八页，2022年，8月28日 主要内容背景介绍微分不变式判别准则和计算方法应用第三页，共二十八页，2022年，8月28日 系统分类离散： x:=1; while (x=10) { x:=x+1; }q3q1q2第四页，共二十八页，2022年，8月28日 系统分类连续:时间，速度，温度 ……（常）微分方程 dx/dt = f(x,t) (1) x(0)=x0 x(t)dx/dt = 1ds/dt = v; dv/dt = a 第五页，共二十八页，2022年，8月28日 系统分类混成：第六页，共二十八页，2022年，8月28日 系统分类混成：dx/dt=f1dx/dt=f2dx/dt=f3第七页，共二十八页，2022年，8月28日 安全性质验证系统S状态空间X非安全集合U系统的初始状态结合X0系统的可达状态集合R(X0,S)R(X0,S) ∩ U = ?第八页，共二十八页，2022年，8月28日 例x:=1; while (x=10) { x:=x+1; }{1,2,3,4,5,6,7,8,9,10,11}1≤x≤11x≤0第九页，共二十八页，2022年，8月28日 While循环x:=1; while (x=109) { x:=x+1; }{1,2,3,……}可达状态集的近似：如抽象解释第十页，共二十八页，2022年，8月28日 Hoare逻辑（归纳）不变式X0?Inv Inv {S} Inv Inv ∩ U = ?第十一页，共二十八页，2022年，8月28日 例x:=1; while (x=10) { x:=x+1; }x=1?x ≥ 1 x ≥ 1?x+1 ≥ 1 x ≥ 1?not(x≤0)第十二页，共二十八页，2022年，8月28日 主要内容背景介绍微分不变式判别准则和计算方法应用第十三页，共二十八页，2022年，8月28日 连续归纳X0dx/dt=f(x)连续系统的可达集计算微分不变式x0x(t)InvX0第十四页，共二十八页，2022年，8月28日 主要内容背景介绍微分不变式判别准则和计算方法应用第十五页，共二十八页，2022年，8月28日 判别准则x:=1; while (x=10) { x:=x+1; }x(i) ≥ 1?x(i+1) ≥1x(i+1)=x(i)+1第十六页，共二十八页，2022年，8月28日 判别准则x(i) ≥ 1?x(i+1) ≥1x(i+1)=x(i)+1x(t) ∈Inv?x(t+Δt) ∈Invx(t+Δt)=x(t)+x’(t) ΔtΔt0, Δt?0Δt第十七页，共二十八页，2022年，8月28日 判别准则dx/dt=f(x), f(x)多项式p(x) ≥ 0, p(x)多项式p(x)=0边界dp(x(t))/dtp(x) 000第十八页，共二十八页，2022年，8月28日 判别准则dp/dx=0p(x) 0=0第十九页，共二十八页，2022年，8月28日 完备判别准则dp/dt=0d2p/dt2 0,=0d3p/dt3 0,=0… …上界N(p,f)Liu Jiang, Zhan Naijun, Zhao Hengjun: Computing semi-algebraic invariants for polynomial dynamical systems. In: EMSOFT’11. pp. 97–106. ACM, New York, NY, USA (2011)p(x) 0第二十页，共二十八页，2022年，8月28日 计算方法设定模板 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，…第二十一页，共二十八页，2022年，8月28日 混成一族微分不变式初始状态关于迁移关系一致不变式蕴含安全性质f3f1f2第二十二页，共二十八页，2022年，8月28日 应用背景介绍微分不变式判别准则和计算方法应用第二十三页，共二十八页，2022年，8月28日 例第二十四页，