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

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

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

本文編號(hào)：1284021