多項式混成系統(tǒng)不變式生成

多項式混成系統(tǒng)不變式生成第1頁，共28頁，2023年，2月20日，星期四主要內容背景介紹微分不變式判別準則和計算方法應用第2頁，共28頁，2023年，2月20日，星期四主要內容背景介紹微分不變式判別準則和計算方法應用第3頁，共28頁，2023年，2月20日，星期四系統(tǒng)分類離散：x:=1; while(x<=10){x:=x+1;}q3q1q2第4頁，共28頁，2023年，2月20日，星期四系統(tǒng)分類連續(xù):時間，速度，溫度……（常）微分方程

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

x≥1not(x≤0)第12頁，共28頁，2023年，2月20日，星期四主要內容背景介紹微分不變式判別準則和計算方法應用第13頁，共28頁，2023年，2月20日，星期四連續(xù)歸納X0dx/dt=f(x)連續(xù)系統(tǒng)的可達集計算微分不變式x0x(t)InvX0第14頁，共28頁，2023年，2月20日，星期四主要內容背景介紹微分不變式判別準則和計算方法應用第15頁，共28頁，2023年，2月20日，星期四判別準則x:=1; while(x<=10){x:=x+1;}x(i)≥1x(i+1)≥1x(i+1)=x(i)+1第16頁，共28頁，2023年，2月20日，星期四判別準則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第17頁，共28頁，2023年，2月20日，星期四判別準則dx/dt=f(x),f(x)多項式p(x)≥0,p(x)多項式p(x)=0邊界dp(x(t))/dtp(x)>0<0>0第18頁，共28頁，2023年，2月20日，星期四判別準則dp/dx=0p(x)>0=0第19頁，共28頁，2023年，2月20日，星期四完備判別準則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第20頁，共28頁，2023年，2月20日，星期四計算方法設定模板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，…第21頁，共28頁，2023年，2月20日，星期四混成一族微分不變式初始狀態(tài)關于遷移關系一致不變式蘊含安全性質f3f1f2第22頁，共28頁，2023年，2月20日，星期四應用背景介紹微分不變式判別準則和計算方法應用第23頁，共28頁，2023年，2月20日，星期四例第24頁，共28頁，2023年，2月20日，星期四例第25頁，共28頁，2023年，2月20日，星期四總結混成系統(tǒng)包含連續(xù)與離散行為（歸納）不變式與安全性驗證多項式連續(xù)系統(tǒng)微分不變式生成完備的判別準則