混合系統(tǒng)的形式化驗(yàn)證.pdf

1、混合系統(tǒng)是連續(xù)變量和離散事件非平凡混合的計(jì)算系統(tǒng)，典型的例子有空中交通管制，汽車控制，機(jī)器人，載人航天等等。特別是對(duì)安全性要求極高的應(yīng)用領(lǐng)域，混合系統(tǒng)的形式化驗(yàn)證逐漸成為一種保證系統(tǒng)正確性的重要方法?；旌舷到y(tǒng)的形式化驗(yàn)證主要包括定理證明和模型檢查。其中，可達(dá)性分析是模型檢查的基礎(chǔ)。 由于混合系統(tǒng)是無窮狀態(tài)空間上的復(fù)雜系統(tǒng)，目前關(guān)于混合系統(tǒng)的模型檢查問題的研究還集中在可達(dá)性分析領(lǐng)域。因?yàn)榧幢闶强蛇_(dá)性問題，也只有很小的一類混合系統(tǒng)子

2、集(矩形混合系統(tǒng))是可判定的。對(duì)于混合系統(tǒng)的可達(dá)性問題，大多數(shù)研究者都采用普通多面體或類似于普通多面體的結(jié)構(gòu)來表示狀態(tài)集，用量詞消去運(yùn)算計(jì)算可達(dá)集。量詞消去運(yùn)算的計(jì)算復(fù)雜度是雙指數(shù)級(jí)的。對(duì)于混合系統(tǒng)模型檢查問題的研究，還集中在實(shí)時(shí)系統(tǒng)(可以看作是最簡(jiǎn)單的混合系統(tǒng))領(lǐng)域。本文主要包含如下四個(gè)方面的工作。 首先解決了有界整數(shù)域上的一階投影時(shí)序邏輯的可滿足性問題。同時(shí)，定義了一種基于稠密時(shí)間的時(shí)間區(qū)間時(shí)序邏輯來描述實(shí)時(shí)和混合系統(tǒng)的性質(zhì)

3、。通過轉(zhuǎn)換為有界整數(shù)域上一階投影時(shí)序邏輯的可滿足性問題，證明了稠密的時(shí)間區(qū)間時(shí)序邏輯的可滿足性問題是可判定的。 提出了一種稱作混合區(qū)域的約束系統(tǒng)，它可用于矩形混合系統(tǒng)的符號(hào)化可達(dá)性分析?；旌蠀^(qū)域是由滿足嚴(yán)格限制條件的線性不等式聯(lián)立表示的多面體區(qū)域。這些線性不等式都由一個(gè)線性表達(dá)式和一個(gè)有理數(shù)通過不等號(hào)連接而成，其中線性表達(dá)式中的變量不超過兩個(gè)，并且變量的系數(shù)與混合系統(tǒng)中相應(yīng)斜率的取值范圍有關(guān)。使用混合區(qū)域進(jìn)行矩形混合系統(tǒng)可達(dá)性分

4、析，必須保證其對(duì)于矩形自動(dòng)機(jī)可達(dá)性操作的封閉性。本文用了很大篇幅證明了混合區(qū)域?qū)τ诰匦巫詣?dòng)機(jī)兩種類型的轉(zhuǎn)換操作是封閉的，即一個(gè)混合區(qū)域經(jīng)過一個(gè)延遲轉(zhuǎn)換，或一個(gè)跳躍轉(zhuǎn)換后所有可達(dá)的狀態(tài)仍可用一個(gè)混合區(qū)域來表示。為了在計(jì)算機(jī)中存儲(chǔ)混合區(qū)域，我們定義了一種稱作不同上限矩陣的矩陣數(shù)據(jù)結(jié)構(gòu)。把不同上限矩陣轉(zhuǎn)換為標(biāo)準(zhǔn)型之后，矩形混合系統(tǒng)的可達(dá)性運(yùn)算就變得很直接。這樣，使用不同上限矩陣進(jìn)行矩形混合系統(tǒng)的可達(dá)性分析，主要的運(yùn)算就是計(jì)算標(biāo)準(zhǔn)型。而標(biāo)準(zhǔn)型問

5、題是線性優(yōu)化問題，可以利用多項(xiàng)式復(fù)雜度的算法加以解決。我們還定義了一種稱作矩形混合圖表的結(jié)構(gòu)處理混合區(qū)域的并。此外，我們還介紹的一種用矩形自動(dòng)機(jī)近似模擬非線性混合系統(tǒng)的方法，然后使用混合區(qū)域判定矩形自動(dòng)機(jī)的可達(dá)性問題進(jìn)而近似地判定非線性混合系統(tǒng)的可達(dá)性問題。 提出了多速率混合系統(tǒng)的一種模型檢查算法，用來判定一個(gè)多速率自動(dòng)機(jī)M描述的系統(tǒng)是否滿足某個(gè)稠密的時(shí)間區(qū)間時(shí)序邏輯公式φ描述的性質(zhì)。我們定義了多速率自動(dòng)機(jī)賦值集上的一種等價(jià)關(guān)系