基于線性誤差斷言的推理方法

武 鵬，吳盡昭，2，3，4*

（1.北京交通大學(xué)計算機與信息技術(shù)學(xué)院，北京 100044；2.中國科學(xué)院成都計算機應(yīng)用研究所，成都 610041；3.廣西大學(xué)計算機與電子信息學(xué)院，南寧 530004；4.廣西民族大學(xué)人工智能學(xué)院，南寧 530006）

0 引言

形式化驗證屬于形式化方法的范疇，形式化驗證主要包含兩種方法，模型檢驗和定理證明。模型檢測是由Clarke和Emerson提出的，主要通過搜索系統(tǒng)狀態(tài)空間來驗證系統(tǒng)的正確性的一種方法［1］。而定理證明主要解決如何利用邏輯和數(shù)學(xué)推理證明的手段驗證軟件的關(guān)鍵性質(zhì)。這兩種方法優(yōu)勢互補，在學(xué)術(shù)界［2-3］、工業(yè)界［4］得到了廣泛應(yīng)用。定理證明中的推理方法是演繹推理范疇，其中語法、語義、推理規(guī)則涉及其中，許多學(xué)者在這一領(lǐng)域有廣泛的深入研究［5-6］。標(biāo)簽變遷系統(tǒng)或其相似結(jié)構(gòu)廣泛應(yīng)用在模型檢驗和定理證明相關(guān)的驗證領(lǐng)域，它是刻畫系統(tǒng)的變遷行為的常用技術(shù)手段［7］。其中，系統(tǒng)各個狀態(tài)及變遷條件通過相應(yīng)邏輯賦值及其滿足的條件來刻畫。然而，二值或多值邏輯在描述復(fù)雜系統(tǒng)的狀態(tài)并不完全有效［8］。實多項式代數(shù)變遷系統(tǒng)將二值邏輯和多值邏輯的狀態(tài)空間擴展到Rn域，這在描述復(fù)雜系統(tǒng)行為和驗證復(fù)雜系統(tǒng)安全性質(zhì)上更有效［9］。近年來，在混成系統(tǒng)的驗證領(lǐng)域，微分多項式代數(shù)和不變量理論［10-11］相繼被提出，這進(jìn)一步地拓寬了基于定理證明的推理方法的應(yīng)用領(lǐng)域。

另一方面，在復(fù)雜系統(tǒng)中，系統(tǒng)參數(shù)有時并不是精確確定的，大多數(shù)情況下只知道這些參數(shù)的取值范圍，這增加了這些系統(tǒng)的推理驗證工作的難度。例如，許多基于多項式的定理證明系統(tǒng)中廣泛運用了Grobner基方法，然而多項式方程組的Grobner基對系數(shù)是不連續(xù)的［12］，這大大增加了推理驗證方法處理誤差參數(shù)多項式系統(tǒng)的難度。而系統(tǒng)的誤差又是普遍存在的。工程上，在驗證系統(tǒng)某些性質(zhì)的過程中，對變遷條件的刻畫是確定的數(shù)值，而這恰恰是工程上無法做到的。例如，當(dāng)系統(tǒng)溫度等于90°時，停止供熱。但實際中，無法精確測量溫度剛好到達(dá)90°，測量的過程都伴隨著一定的誤差。在系統(tǒng)變遷的過程中，往往有若干個閾值條件來觸發(fā)系統(tǒng)的變遷，這就需要對這若干個系統(tǒng)參數(shù)精確測量。而事實上，這是不可能做到的，測量的過程總是伴隨著一定的誤差。多個誤差變量的累計和傳遞過程中，系統(tǒng)可能出現(xiàn)錯誤的變遷行為。是否能定量地將誤差參數(shù)結(jié)合到推理方法中，并應(yīng)用于含誤差參數(shù)系統(tǒng)的推理驗證工作中？筆者在文獻(xiàn)［13］中給出了線性誤差斷言零點集的凸集性的證明，但未給出求線性誤差斷言所有頂點的方法和相關(guān)證明；而求取這些頂點是文本方法步驟的必不可少的環(huán)節(jié)，也是實現(xiàn)本文方法的難點。本文給出了求線性誤差斷言頂點的具體方法并證明了該方法的正確性，之后給出文本方法在驗證火車加速狀態(tài)的應(yīng)用，求取了火車加速狀態(tài)的參數(shù)化頂點，將看似非線性問題處理為線性問題，進(jìn)一步擴大了本文方法的應(yīng)用范圍。這在以往的文獻(xiàn)中是鮮有報道的。本文給出的推理方法可用于線性誤差系統(tǒng)的推理驗證工作中。

1 誤差的區(qū)間數(shù)刻畫

誤差是普遍存在的，有時也是必不可免的。在推理方法中引入誤差，就需要對誤差做定量刻畫。誤差常常是限定的一個區(qū)域，而區(qū)間數(shù)是數(shù)的推廣，區(qū)間數(shù)在許多方面已經(jīng)成功應(yīng)用［14-16］，下面介紹區(qū)間數(shù)的運算規(guī)則。

區(qū)間數(shù)是實數(shù)的推廣，當(dāng)a-=a+時，-a為實數(shù)。然而上述定義的區(qū)間數(shù)的四則運算是不可逆的，下面給出例子。

若a為實數(shù)，則式（1）則一定成立。然而若a，b為區(qū)間數(shù)，式（1）不一定成立。

但這并不意味著包含上述四則運算的推理過程是錯誤的，只是推理過程不可逆，即推理的結(jié)論是前提的一個必要條件，而非充分必要條件。在包含誤差的推理的過程中，運算次數(shù)的增多，可能會導(dǎo)致結(jié)果沒有實際意義，所以在推理過程中，要嘗試其他方法。本文的方法提供了一種思路。

2 線性誤差斷言及蘊含關(guān)系

2.1 線性誤差斷言

2.2 蘊含關(guān)系

蘊含關(guān)系是基于定理證明的形式化驗證領(lǐng)域重要環(huán)節(jié)，也是推理規(guī)則的基礎(chǔ)問題。φ1蘊含φ2表示：如果φ1為真，則φ2一定為真。記作φ1|=φ2。例如：φ1：x-1=0，φ2：x2-1=0，顯然有：φ1|=φ2?；诙囗検綌嘌缘奶N含關(guān)系［17］中有這樣一個充要條件：φ1|=φ2的充分必要條件為Zero(φ1)?Zero(φ2)。這同樣適用于線性誤差斷言。下面給出線性誤差斷言的蘊含關(guān)系的充分必要條件。

3 推理方法

4 實例分析

4.1 火車加速狀態(tài)分析

下面以火車加速運動為例分析。為了便于分析，假設(shè)火車有2個車廂（8車廂和16車廂問題可由兩車廂問題遞歸得到），兩車廂各有動力輸出?；疖囋诩铀龠^程中，當(dāng)————guard為v=80 m s=288km h滿足時，火車由加速狀態(tài)轉(zhuǎn)變?yōu)閯蛩贍顟B(tài)（由圖1所示），-φ、-?為加速狀態(tài)和勻速狀態(tài)各自正常工作滿足的條件。在火車的加速狀態(tài)中，如果-φ不滿足，則火車加速狀態(tài)異常，需立即檢測異常。

圖1 火車狀態(tài)變遷Fig.1 Train state transition

f1、f2分別表示車廂1與車廂2各自提供的牽引力。f12為車廂1對車廂2的作用力，為一區(qū)間數(shù)。m1、m2代表每個車廂的初始質(zhì)量。Δm1、Δm2代表車廂的質(zhì)量變化（由于乘客和行李的變化），為區(qū)間數(shù)。ζ是一個關(guān)聯(lián)空氣密度壓強的系數(shù)，由于風(fēng)、海拔等因素的變化，ζ為區(qū)間數(shù)。a表示加速度。g為重力加速度。

下面給出上述變量值，m1=50 000 kg，Δm1=[0，0.2m1]，m2=50 000 kg， Δm2=[0，0.2m2]，ζ=[1.5，1.6]kg m，μ=0.01，a=0.4 m s2，f12=[0，2 000]N，g=10 m s2。

由力學(xué)知識，可有式（20）：

由第3章的推理方法的步驟2得式（21）：

圖2 的空間區(qū)域Fig.2 Spatial region of Zero(-φ)

4.2 模擬與測試

將式（22）代入式（20），可得到n個解，表示如式（23）：

將式（23）中的n個解分別代入式（21），來驗證是否滿足該不等式組。分別測試了n=1 000，n=10 000，n=100 000的情況。其中圖3和圖4為1 000個解的空間位置（n=1000）。圖5為10 000個解的空間位置（n=10 000）。圖6為100 000個解的空間位置（n=100 000）。

圖3 1 000個測試用例Fig.3 A thousand test cases

圖4 圖3的另一角度Fig.4 Another angleof Fig.3

圖5 10 000個測試用例Fig.5 Ten thousand test cases

圖6 100 000個測試用例Fig.6 Onehundred thousand test cases

經(jīng)測試，所有的解都在式（21）表示的區(qū)域內(nèi)。這個區(qū)域表示由不確定誤差系數(shù)導(dǎo)致的可能的動力分配區(qū)域，以保證列車平穩(wěn)加速行駛。如果列車平穩(wěn)加速過程中的動力分配不在這個區(qū)域內(nèi)部，或始終接近該區(qū)域的邊界時，則表示存在非誤差因素對動力系統(tǒng)的影響。這時需要排除是否存在機械故障，比如車軸軸承或電機軸承是否需要更換潤滑脂。

4.3 推理分析

其中t∈[0，200]。

5 結(jié)語

對于系數(shù)和變量有誤差的系統(tǒng)，大多數(shù)以前的推理方法都不適用。但是文獻(xiàn)［18］方法對具有單個誤差變量的多項式系統(tǒng)有非常高的理論價值。在多個誤差變量的推理方法上，已有的文獻(xiàn)還少有報道。另一方面，針對誤差的模糊推理［19］也有一些學(xué)者在研究，這類方法最終給出了推理結(jié)論正確性的模糊程度或類似結(jié)論，這與本文提出的推理方法是有區(qū)別的，本文的推理方法最終可以給出推理結(jié)論是否正確的確定性回答。

本文推理方法可對給定誤差區(qū)間的線性斷言進(jìn)行可靠的推理。此外，對于那些零點不完全非負(fù)的線性誤差斷言，可用變量替換將其零點全部做非負(fù)處理。例如，攝氏溫度c是有可能出現(xiàn)負(fù)值的，可以用一個變量替換c'=c+273.15，其中c'表示其相應(yīng)的開爾文溫度（絕對溫度）。然而，在非線性誤差多項式斷言的推理方法上，目前仍沒有有效的解決方法。結(jié)合控制點生成方法，有望將非線性誤差多項式斷言的零點集作線性化包含處理，這樣可以進(jìn)一步擴大該方法應(yīng)用范圍，這也是今后的工作方向。