多項(xiàng)式混成系統(tǒng)不變式生成第一頁，共二十八頁，編輯于2023年，星期五主要內(nèi)容背景介紹微分不變式判別準(zhǔn)則和計(jì)算方法應(yīng)用第二頁，共二十八頁，編輯于2023年，星期五主要內(nèi)容背景介紹微分不變式判別準(zhǔn)則和計(jì)算方法應(yīng)用第三頁，共二十八頁，編輯于2023年，星期五系統(tǒng)分類離散：x:=1; while(x<=10){x:=x+1;}q3q1q2第四頁，共二十八頁，編輯于2023年，星期五系統(tǒng)分類連續(xù):時間，速度，溫度……（常）微分方程

dx/dt=f(x,t)(1)x(0)=x0x(t)dx/dt=1ds/dt=v;dv/dt=a第五頁，共二十八頁，編輯于2023年，星期五系統(tǒng)分類混成：第六頁，共二十八頁，編輯于2023年，星期五系統(tǒng)分類混成：dx/dt=f1dx/dt=f2dx/dt=f3第七頁，共二十八頁，編輯于2023年，星期五安全性質(zhì)驗(yàn)證系統(tǒng)S狀態(tài)空間X非安全集合U系統(tǒng)的初始狀態(tài)結(jié)合X0系統(tǒng)的可達(dá)狀態(tài)集合R(X0,S)R(X0,S)∩U=?第八頁，共二十八頁，編輯于2023年，星期五例x:=1; while(x<=10){x:=x+1;}{1,2,3,4,5,6,7,8,9,10,11}1≤x≤11x≤0第九頁，共二十八頁，編輯于2023年，星期五While循環(huán)x:=1;while(x<=109){x:=x+1;}{1,2,3,……}可達(dá)狀態(tài)集的近似：如抽象解釋第十頁，共二十八頁，編輯于2023年，星期五Hoare邏輯（歸納）不變式X0InvInv{S}InvInv∩U=?第十一頁，共二十八頁，編輯于2023年，星期五例x:=1; while(x<=10){x:=x+1;}x=1x≥1x≥1x+1≥1

x≥1not(x≤0)第十二頁，共二十八頁，編輯于2023年，星期五主要內(nèi)容背景介紹微分不變式判別準(zhǔn)則和計(jì)算方法應(yīng)用第十三頁，共二十八頁，編輯于2023年，星期五連續(xù)歸納X0dx/dt=f(x)連續(xù)系統(tǒng)的可達(dá)集計(jì)算微分不變式x0x(t)InvX0第十四頁，共二十八頁，編輯于2023年，星期五主要內(nèi)容背景介紹微分不變式判別準(zhǔn)則和計(jì)算方法應(yīng)用第十五頁，共二十八頁，編輯于2023年，星期五判別準(zhǔn)則x:=1; while(x<=10){x:=x+1;}x(i)≥1x(i+1)≥1x(i+1)=x(i)+1第十六頁，共二十八頁，編輯于2023年，星期五判別準(zhǔn)則x(i)≥1x(i+1)≥1x(i+1)=x(i)+1x(t)∈Invx(t+Δt)

∈Invx(t+Δt)=x(t)+x’(t)

ΔtΔt>0,

Δt0Δt第十七頁，共二十八頁，編輯于2023年，星期五判別準(zhǔn)則dx/dt=f(x),f(x)多項(xiàng)式p(x)≥0,p(x)多項(xiàng)式p(x)=0邊界dp(x(t))/dtp(x)>0<0>0第十八頁，共二十八頁，編輯于2023年，星期五判別準(zhǔn)則dp/dx=0p(x)>0=0第十九頁，共二十八頁，編輯于2023年，星期五完備判別準(zhǔn)則dp/dt=0d2p/dt2>0,=0d3p/dt3>0,=0……上界N(p,f)LiuJiang,ZhanNaijun,ZhaoHengjun:Computingsemi-algebraicinvariantsforpolynomialdynamicalsystems.In:EMSOFT’11.pp.97–106.ACM,NewYork,NY,USA(2011)p(x)>0第二十頁，共二十八頁，編輯于2023年，星期五計(jì)算方法設(shè)定模板p(u,x)>=0p=0(dp/dt>0\/dp/dt=0/\d2p/dt2>0\/

dp/dt=0/\d2p/dt2=0/\d3p/dt3=0\/dp/dt=0/\.../\dNp/dtN≥0)Forallx.Φ(u,x)量詞消去，SOS，…第二十一頁，共二十八頁，編輯于2023年，星期五混成一族微分不變式初始狀態(tài)關(guān)于遷移關(guān)系一致不變式蘊(yùn)含安全性質(zhì)f3f1f2第二十二頁，共二十八頁，編輯于2023年，星期五應(yīng)用背景介紹微分不變式判別準(zhǔn)則和計(jì)算方法應(yīng)用第二十三頁，共二十八頁，編輯于2023年，星期五例第二十四頁，共二十八頁，編輯于2023年，星期五例第二十五頁，共二十八頁，編輯于2023年，星期五總結(jié)混成系統(tǒng)包含連續(xù)與離散行為（歸納）不變式與安全性驗(yàn)證多項(xiàng)式連續(xù)系統(tǒng)微分不變式生成完備的判別準(zhǔn)則