《基於代數分析與符號計算的混成系統自動驗證》是依託北京航空航天大學，由佘志坤擔任項目負責人的青年科學基金項目。
基本介紹
- 中文名：基於代數分析與符號計算的混成系統自動驗證
- 依託單位：北京航空航天大學
- 項目負責人：佘志坤
- 項目類別：青年科學基金項目
項目摘要,結題摘要,
項目摘要
混成系統是一種同時包含連續狀態和離散事件的動力系統。隨著信息科學的發展，混成系統與人們的日常關係日益密切，促使人們更加關注混成系統的研究。特別地，對混成系統自動驗證的研究更是目前國際研究的熱點之一。相關的大型項目有德國的AVACS、歐盟的HYCON等。我們在該方向的理論和套用研究中業已取得了不少成果。例如，我們曾通過構造約束條件對非線性混成系統的安全性驗證問題進行了直接處理，突破了現有理論通常採用線性近似來處理的局限，並開發了驗證軟體HSolver。. 本課題將在已有成果上深入研究非線性混成系統自動驗證理論及其套用。我們希望在抽象精化、模型檢查及Lyapunov穩定下，通過採用安全性和穩定性的代數分析理論和方法，並結合符號計算，在程式化驗證混成系統安全性和穩定性的理論與方法等方面取得新的進展，並進行實例研究,如分析運行火車間的碰撞問題、空間飛行器的軌道安全問題、生物系統穩定性問題等。
結題摘要
隨著信息科學的快速發展，混成系統研究備受關注。在國家自然科學基金項目的資助下，本項目主要圍繞混成系統安全性驗證、穩定性分析以及兩者的關聯性展開研究，在Journal of Symbolic Computation、European Journal of Control等國際期刊以及ISSAC、HSCC等國際會議上共發表標註國家自然科學基金項目資助的學術論文14篇，其中SCI收錄6篇，ISTP收錄3篇，EI收錄3篇（不重複計算），完滿地完成了申請書里設定的預期目標。特別地，作為第三完成人參與的“複雜信息系統行為與結構的若干科學問題研究”獲2013年度高等學校科學研究優秀成果獎（自然科學獎）一等獎（鄭志明、許可、佘志坤等）。本項目的主要學術成果可歸納如下： (1)基於遞歸推理與量詞消去，對非線性混成系統的安全性驗證問題設計了新的算法，該算法消除了區間算法的“滾雪球”效應，並且對於魯棒式安全系統的驗證是可終止的；基於混成自動機與機率自動機，提出了一種保全全屬性的有限機率自動機的普適構造方法，該方法進一步發展了驗證機率混成系統安全性的抽象精化理論。美國Vanderbilt大學Prof . X. Koutsoukos對該工作專門寫了三頁的Discussion。 (2)基於符號計算中的實根分類，考慮了多項式Lyapunov函式的自動生成；進一步，結合投影運算元，考慮了多重Lyapunov函式的自動生成。與國際上現有的穩定性分析方法相比，我們的基於實根分類的代數方法彌補了線性矩陣不等式法只能處理非退化系統的局限性，克服了平方和分解法的數值不可信性，並降低了普適量詞消去的計算複雜性。 (3)利用類Lyapunov函式，設計了可疊代生成儘可能大的帶目標區域的不變核心的理論框架，並基於平方和方法進行了算法實現。該疊代生成的不變核心可以看成是目標區域的一個吸引域估計，也可以看成由目標區域出發的向後可達集的下近似。特別地，當給定的目標區域為吸引域的一初估計時，與國際上最新方法的比較，我們的數值疊代方法能獲得更大的吸引域估計。同時，項目負責人積極參與國內外學術合作與交流，並指導博士研究生4名、碩士研究生2名。另外，本項目嚴格按照《資助計畫書》規定的經費預算支出，所有支出範圍都嚴格遵循《國家自然科學基金項目經費管理辦法》的規定。
