擴展的線性時段不變式的模型檢驗

中文摘要

擴展的線性時段不變式（ELDI）是時段演算中描述系統區間性質的一類重要公式，然而因ELDI的決策問題在離散和連續時間下是不可判定的，對ELDI的模型檢驗仍然存在許多待解決的理論問題且與實際套用還有一定差距。因此本項目將主要致力於解決ELDI的模型檢驗，主要研究內容有：（1）最佳化離散時間語義下ELDI的有界模型檢驗算法，包括（a）研究一類帶有切變和與運算符結合的ELDI性質的反轉；（b）研究原系統自動機A的反轉自動機A'；（c）驗證結果的等價性和反向思想的擴展。（2）連續時間語義下ELDI的有界模型檢驗算法，包括（a）只含有一個切變運算的檢驗；（b）含有多個切變運算以及和邏輯運算符結合的檢驗。（3）離散時間語義下無界觀測區間的ELDI的模型檢驗算法，包括（a）帶有單個切變運算符的檢驗算法；（b）帶有多個切變運算符以及與其他邏輯運算符結合的檢驗算法。（4）模型檢驗的工具實現以及具體工業實例分析。

結題摘要

在標準離散時間語義和連續時間語義下，我們研究擴展的現行時段不變式（ELDI）的有界和無界模型檢驗。同時, 我們還研究了凸二分圖動態匹配、混合系統驗證以及實時自動機的不透明度和模型學習等相關問題。發表了8篇較高水平論文，目前培養博士2名和碩士8名。主要研究成果如下： 1. 基於時間自動機的連續時間ELDI的有界模型檢驗 ELDI的模型檢查問題在標準連續時間和離散時間語義方面都是不可判定的，我們證明這個問題在連續時間語義中仍然是可判定的。方法主要是通過轉化為量詞線性實算術公式（QLRA）並求解來實現。一些示例說明了我們的方法的效率。 2. 基於實時自動機的連續時段演算的驗證 我們將擴展線性時段不變式的有界模型檢驗問題轉化為量詞線性算術公式的正確性問題，從而可以採用量詞消去技術進行求解。降低了驗證複雜度並且加速了驗證過程的實際速度。 3. 凸二分圖動態匹配問題的解決研究兩種帶權凸二分圖中動態權值匹配問題，以及提高凸二分圖動態基數匹配問題中查詢操作的效率。（1）提出了一個解決二分圖動態匹配問題的方法框架。（2）解決左側頂點帶權凸二分圖動態權值匹配問題（3）解決兩側頂點帶權凸二分圖動態權值匹配 4. 基於證明的使用微分不變數的混合系統開發方法從混合系統連續行為的建模方法、連續行為模型的證明義務規則、證明技術、證明工具等四個方面進行了研究，提出了一種基於Event-B框架的混合系統開發方法。 5. 設計基於屏障證書的相連混成系統的安全性驗證我們提出了一個數值方法驗證互聯混合動力系統的約束狀態的安全性。該方法是一種數值方法，狀態約束基於雙線性平方和規劃。可以驗證互聯混合系統的安全性。 6. 實時自動機的學習（論文已投）我們提出了一種在連續時間語義和離散時間語義上的確定性實時自動機（DRTA）的主動學習算法。對於一個由DRTA A能識別的目標語言，我們將學習DRTA A的問題轉化為正交實時自動機A’的學習，並且 L（A'）= L（A）。 7. 實時自動機的不透明性研究了實時自動機（RTA）的不透明度問題，這是一種用於實時系統的模型。證明RTA的語言不透明問題是可判定的。 8. ELDI模型檢驗工具和模型學習軟體實現

擴展的線性時段不變式的模型檢驗

基本介紹

中文摘要

結題摘要

相關詞條

熱門詞條