基于混合邏輯動(dòng)態(tài)模型的預(yù)測控制與形式驗(yàn)證技術(shù).pdf

1、在現(xiàn)代流程工業(yè)中,過程控制對(duì)象日益復(fù)雜以及對(duì)控制精度的要求日益提高,工業(yè)過程控制中連續(xù)過程動(dòng)態(tài)和離散事件動(dòng)態(tài)的混雜特性越來越明顯,傳統(tǒng)的理論方法對(duì)這些系統(tǒng)進(jìn)行建模和控制,已很難滿足控制要求。針對(duì)這種情況,本文采用混合邏輯動(dòng)態(tài)(Mixed Logical Dynamical,MLD)模型理論,進(jìn)行混雜系統(tǒng)的建模、控制與形式驗(yàn)證研究。
　　 本文在前人研究工作的基礎(chǔ)上,對(duì)混雜系統(tǒng)理論作了進(jìn)一步的研究和探索。研究的內(nèi)容包括基于MLD的

2、混雜系統(tǒng)控制和形式驗(yàn)證研究兩個(gè)部分,主要體現(xiàn)在以下幾個(gè)方面:
　　 深入研究了混合邏輯動(dòng)態(tài)系統(tǒng)建模機(jī)理,討論了邏輯命題的轉(zhuǎn)換及其線性整數(shù)規(guī)劃的方法,分別以機(jī)理建模和Hysdel方法建立了CSTR系統(tǒng)的MLD模型,總結(jié)了混雜系統(tǒng)不同模型之間的等價(jià)性。
　　 將傳統(tǒng)的模型預(yù)測控制應(yīng)用到基于MLD模型的混雜系統(tǒng)中,研究了混合邏輯動(dòng)態(tài)系統(tǒng)的開環(huán)約束最優(yōu)控制,分別探討了基于MIQP和MILP問題的模型預(yù)測控制,通過數(shù)值仿真驗(yàn)證了兩

3、種算法的有效性。
　　 探討了定理證明和模型檢驗(yàn)兩種混雜系統(tǒng)形式驗(yàn)證方法,詳細(xì)介紹了基于模型檢驗(yàn)的形式驗(yàn)證工具,利用CheckMate驗(yàn)證工具對(duì)彈跳球系統(tǒng)進(jìn)行了形式驗(yàn)證的仿真研究。
　　 研究了混合邏輯動(dòng)態(tài)系統(tǒng)的形式驗(yàn)證問題,針對(duì)混合邏輯動(dòng)態(tài)系統(tǒng),在理論上深入研究了基于數(shù)學(xué)規(guī)劃的混雜系統(tǒng)形式驗(yàn)證算法,將該算法應(yīng)用到非線性CSTR系統(tǒng)中,探討了CSTR系統(tǒng)的安全性問題,對(duì)混雜系統(tǒng)控制的正確性和可靠性進(jìn)行了有益的探索。