本文關(guān)鍵詞：近似推理—多項式代數(shù)動態(tài)邏輯研究

  更多相關(guān)文章： 多項式代數(shù)動態(tài)邏輯 近似推理 多項式代數(shù)變遷系統(tǒng) 定理證明 復(fù)雜系統(tǒng)驗證 性能評估

【摘要】：隨著計算機技術(shù)的飛速發(fā)展,復(fù)雜系統(tǒng),例如軌道交通、航空航天、工業(yè)控制等的規(guī)模和結(jié)構(gòu)越來越龐大和復(fù)雜,系統(tǒng)出現(xiàn)缺陷和漏洞的可能性也在不斷增加。任何微小錯誤都足以導(dǎo)致巨大的經(jīng)濟損失,甚至人員傷亡。如何確保復(fù)雜系統(tǒng)設(shè)計的正確性,是學術(shù)界和工業(yè)界一直關(guān)注的問題。已有研究和實踐表明,基于邏輯推理的形式化方法是解決這一問題的有效方法。由于復(fù)雜系統(tǒng)普遍具有數(shù)據(jù)流交換、連續(xù)狀態(tài)、性能指標等特性,傳統(tǒng)的邏輯推理方法面臨一些新挑戰(zhàn),主要包括如何建立系統(tǒng)行為與性質(zhì)斷言的統(tǒng)一邏輯框架,如何支持組合化、層次化刻畫與驗證,如何將數(shù)學計算過程與邏輯推理過程融合,如何在邏輯框架內(nèi)建立系統(tǒng)性能的度量標準等。針對這些問題,本文詳細研究了刻畫系統(tǒng)行為和性質(zhì)斷言的統(tǒng)一邏輯語言,以及邏輯語言的數(shù)學模型、證明系統(tǒng)和近似推理系統(tǒng),并結(jié)合實例深入探討了它們在實際中的應(yīng)用。本文取得的創(chuàng)新成果歸納如下：(1)提出了具有組合化和層次化特性的多項式代數(shù)動態(tài)邏輯(ADL),有效地解決了系統(tǒng)行為與性質(zhì)斷言的統(tǒng)一邏輯刻畫問題。在ADL的框架中,系統(tǒng)行為被刻畫為多項式代數(shù)程序,性質(zhì)斷言被刻畫為ADL邏輯公式。ADL的組合化特性體現(xiàn)為：多項式代數(shù)程序具有組合化的結(jié)構(gòu),通過順序、條件、循環(huán)等符號將各個子程序組合在一起；層次化則體現(xiàn)為：不同層次之間的關(guān)系可被刻畫為ADL模態(tài)公式,如模態(tài)公式[α]φ→[β]φ可表示底層程序a實現(xiàn)了高層程序β的功能。(2)提出了一種更加精細的數(shù)學模型——多項式代數(shù)變遷系統(tǒng)(ATS),有效地解決了數(shù)據(jù)流交換、連續(xù)狀態(tài)等的刻畫問題。通過引入連續(xù)變量,ATS能夠描述連續(xù)狀態(tài),并允許系統(tǒng)具有無限的連續(xù)狀態(tài)空間,因而具有更強的系統(tǒng)刻畫能力;通過在系統(tǒng)變遷上標記多項式表達式,ATS能夠同時刻畫狀態(tài)跳轉(zhuǎn)和數(shù)據(jù)流交換,因而可以刻畫更加精細的系統(tǒng)行為。更加有意義的是,通過建立系統(tǒng)行為與多項式零點之間的聯(lián)系,符號計算等成熟的數(shù)學方法能夠應(yīng)用于復(fù)雜系統(tǒng)的驗證分析。(3)建立了ADL的形式化語義和證明系統(tǒng)(ADL演算),有效地解決了數(shù)學計算過程與邏輯推理過程的交叉融合問題。以ATS為語義模型,構(gòu)造了ADL的形式化語義,包括多項式代數(shù)程序的變遷語義和邏輯公式的滿足關(guān)系,變遷語義和滿足關(guān)系都可用多項式零點定義,因而,邏輯公式的推導(dǎo)問題能夠平滑地轉(zhuǎn)化為符號計算的問題。同時,ADL演算是可靠且部分完備的。(4)建立了ADL的度量語義和近似推理系統(tǒng),有效地解決了系統(tǒng)的性能評估問題。度量語義是對邏輯公式滿足關(guān)系的一種量化描述,反映了公式成立的可能性,度量語義值越大則公式成立的可能性越高;近似推理系統(tǒng)由一組度量規(guī)則構(gòu)成,用于估算系統(tǒng)性質(zhì)在給定狀態(tài)上成立的可能性。同時,近似推理系統(tǒng)是可靠的,而且是對ADL演算的量化擴展：凡是ADL演算可證的公式必定是可近似推導(dǎo)的。最后,本文對兩個實例進行了驗證與分析。實例分析結(jié)果表明,本文所建立的方法能夠有效地刻畫、驗證和分析復(fù)雜系統(tǒng)的性質(zhì)。
【學位授予單位】：北京交通大學
【學位級別】：博士
【學位授予年份】：2016
【分類號】：TP181;N941.4
，

本文編號：1284021