余代數框架下的近似行為等價理論與模態邏輯研究

《余代數框架下的近似行為等價理論與模態邏輯研究》是依託南京航空航天大學，由朱朝暉擔任項目負責人的面上項目。

基本介紹

• 中文名：余代數框架下的近似行為等價理論與模態邏輯研究
• 項目類別：面上項目
• 項目負責人：朱朝暉
• 依託單位：南京航空航天大學

項目摘要

本項目旨在針對當前轉換系統近似等價以及余代數模態邏輯等研究領域中所面臨的問題，探討帶量化信息的余代數的近似行為等價理論，研究余代數模態邏輯的擴張及完備性證明技術。嘗試為帶量化信息的動態轉換系統的近似等價研究提供較一般的理論框架，為余代數模態邏輯相關問題的研究提供新的技術途徑。主要研究內容包括：余代數框架下近似互模擬及其邏輯的模組理論、余代數模態邏輯的正則公式、含不動點的余代數邏輯的完備推理系統以及余代數模態邏輯的PDL擴張。該項目為相關問題的研究提供了新的研究視角和技術手段，其研究有助於加深對余代數模態邏輯基礎性質的把握，使我們對各種不同類型動態轉換系統的近似互模擬與行為度量理論有較統一的認識，更加深入地了解余代數作為動態系統數學模型和模態邏輯一般語義結構所具有的優越性和潛在的局限性。

結題摘要

本項目主要對近似等價、代數與模態邏輯兩種形式化途徑的融合等方面做了較系統的研究，取得的主要成果包括如下方面： （1）將Pola和Tabuada提出的刻畫近似行為等價的概念“交替近似互模擬”推廣到一般情形，研究了一般的交替轉換系統中交替近似互模擬的基本性質，提出了一種近似互模擬模態特徵表述方式，基於交替時序邏輯給出了交替近似互模擬的模態邏輯特徵，從而建立了交替轉換系統間行為近似等價性與其所滿足的邏輯性質之間的內在聯繫。並將此概念用於刻畫帶擾動控制系統與其有限抽象之間的關係，提出了一個控制策略算法並證明了算法的正確性。 （2）基於對偶理論給出了Rank-1模態邏輯都有餘代數語義的一種新的證明方法，並且建立了通過對偶理論構造出來的函子和Schröder所構造的函子的等價性。提出了模態詞帶布爾結構的余代數模態邏輯系統，並基於公理的一步可靠與完備性研究了該類邏輯系統的可靠完備性。建立了具體範疇上的擬終結對象可以刻畫的等價關係的特徵，並給出擬終結對象形成的格結構的性質。 （3）基於邏輯標記轉換系統（LLTS），較深入地研究了含邏輯連線詞、模態詞以及標準進程代數運算元的代數演算系統，這方面的工作不但將Luttgen與Vogler的工作提升到純粹的代數形式， 而且在如下方面深化和擴展了他們的工作：（a）建立了刻畫Luttgen與Vogler提出的模擬關係的可靠和基完備的公理系統；（b）基於余代數終結語義的思想， 給出將模態詞always與unless納入進程代數的兩種不同的途徑，其中基於遞歸運算元的途徑較之Luttgen與Vogler的構造要簡潔得多；（c）建立了CLLT與ACTL（基於動作的計算樹邏輯）之間的內在聯繫，包括CLLT進程項的ACTL邏輯特徵公式表示、ACTL邏輯公式終結模型的CLLT特徵項表示以及CLLT與ACTL之間的伽羅瓦連線；（d）研究了LLTS上的遞歸構造，建立了同餘性以及方程解的唯一性定理。這部分的工作為形式化規範提供了一種可以自由混合使用邏輯連線詞（合取、析取）、模態詞（always，unless）以及標準進程代數運算元的代數演算系統，該系統支持模組化設計與推理，並可將表示安全性性質的ACTL邏輯公式以代數項的形式加以表示和推理。基於上述工作，我們已完成5篇學術論文，其中包括3篇60頁左右的長文。