《線形時態邏輯的可滿足性理論與套用研究》是依託華東師範大學，由蒲戈光擔任項目負責人的面上項目。
基本介紹
- 中文名：線形時態邏輯的可滿足性理論與套用研究
- 項目類別：面上項目
- 項目負責人：蒲戈光
- 依託單位：華東師範大學
項目摘要,結題摘要,
項目摘要
線性時態邏輯（Linear Temporal Logic, LTL）在系統驗證中扮演著重要的角色，它被廣泛的套用於複雜系統的時態推理與模型檢查。本項目面向線性時態邏輯LTL的基礎理論，研究LTL的可滿足性的判定理論、算法以及潛在的套用。本項目力圖深入挖掘線性時態邏輯的數學特徵，探索新穎並具有高效性能的可滿足性判斷過程。本項目的研究目標包括如下三方面:（1）研究可滿足/不滿足無限序列所具有的數學特徵，如對於給定的LTL公式，一個無限序列滿足/不滿足該公式應該具內在特徵以及與公式的關係;（2）研究LTL可滿足判定的新算法，包括利用SAT技術與機器學習技術加速LTL可滿足判定過程；（3）研究LTL可滿足判定在系統測試及人工智慧邏輯領域的套用，把基於可滿足判定的新算法套用於系統測試的研究，並把該方法學拓展到人工智慧領域邏輯的分析過程（如有限跡的線性時態邏輯的分析與驗證）。
結題摘要
線性時態邏輯（Linear Temporal Logic, LTL）在系統驗證中扮演著重要的角色，它被廣泛的套用於複雜系統的時態推理與模型檢查領域。本項目面向線性時態邏輯LTL 的基礎理論，研究LTL 的可滿足性判定理論、算法以及潛在的套用。本項目在三個方面做了深入的研究：（1）LTL的可滿足性理論與算法，我們研究了LTL公式本身的數學性質，發現了面向SAT的求解框架，研發了Aalta工具，在典型Benchmarks與國際工具對比，總體性能最優；（2）LTL在有限跡下的綜合研究，我們是國際上第一個研究了LTL在有限跡下的綜合算法，包括安全性與公平性制約下的算法研究，實現了相應的工具；（3）面向SAT的模型檢查新算法研究，我們發現了一個新的硬體模型檢查算法，基於模擬逼近的想法，在實驗效果上與主流的驗證工具性能相當，形成互補。研究結果發表在人工智慧與形式化方法的重要期刊與雜誌，如IJCAI、AAAI、HVC、Formal methods in System Design等。培養了2名博士生，5名碩士生，1名博士後。
