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

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

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

0 引言

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

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

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

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

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

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

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

2 線性誤差斷言及蘊含關系

2.1 線性誤差斷言

2.2 蘊含關系

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

3 推理方法

4 實例分析

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

下面以火車加速運動為例分析。為了便于分析，假設火車有2個車廂（8車廂和16車廂問題可由兩車廂問題遞歸得到），兩車廂各有動力輸出。火車在加速過程中，當————guard為v=80 m s=288km h滿足時，火車由加速狀態(tài)轉變?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ū)間數。m1、m2代表每個車廂的初始質量。Δm1、Δm2代表車廂的質量變化（由于乘客和行李的變化），為區(qū)間數。ζ是一個關聯(lián)空氣密度壓強的系數，由于風、海拔等因素的變化，ζ為區(qū)間數。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。

由力學知識，可有式（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

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

4.3 推理分析

其中t∈[0，200]。

5 結語

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

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