基于隨機障礙驗證的隨機連續系統安全性驗證

沈敏捷，曾振柄，林 望，楊爭峰

(1.上海市高可信計算重點實驗室(華東師范大學)，上海200062; 2.上海大學 數學系，上海200444;3.溫州大學數學與信息科學學院，浙江溫州325035)

(*通信作者電子郵箱zbzeng@shu.edu.cn)

0 引言

嵌入式系統是一種嵌入機械或電氣系統內部，具有專一功能和實時計算性能的計算機系統，被廣泛應用于電信、交通、商業、工業、醫療等重要領域。區別于通用計算機，嵌入式系統是為某些特定任務設計的。其中一些系統具有低功耗低成本的要求，因此對其軟硬件資源要求較為嚴格。另一些系統對實時性有很高的要求，如數控機床、列車控制系統、飛機導航系統等。一旦系統的響應時間未能達到要求，可能會造成嚴重的后果。

在嵌入式實時系統中，廣泛存在一類既包含連續動態行為又包含離散事件行為，且兩者互相作用的系統。其動力學行為既隨時間而連續變化，又受事件而離散驅動。以列車自動控制(Automatic Train Control，ATC)系統［1－2］為例，ATC 系統是一個完整的列車速度監督系統，它可以控制列車行進的速度。當列車行駛速度超過容許的速度時，剎車設備應強制減慢其速度，以保證行車安全。在這樣的系統中，離散變化的邏輯控制和實時連續行為結合在一起，共同構成一種復雜的動力系統，稱為混成系統［3］。混成系統通常采用微分方程來描述其連續動態系統，采用狀態自動機來描述系統模式之間的變遷。混成系統的安全性驗證是指，從給定初始狀態區域出發的任意軌線不會到達指定的不安全區域。由于混成系統在安全攸關系統中廣泛存在，對混成系統安全性的研究已經成為一個非常重要的課題［4］。

目前大部分關于混成系統的工作都集中在確定性模型上。然而，由于未知輸入、外界干擾、內部錯誤等因素的存在，嵌入式系統中不可避免存在不確定性因素。如何對相關不確定或隨機因素建模，是混成系統中的一個重要的研究方向。不確定性混成系統可以對離散變遷或連續演化進行一些非確定性的選擇。一般而言，其局限在于在很多情況下結論過于粗糙，無法給出令人滿意的回答。相比之下，隨機混成系統［5］可以對安全性給出一些概率性的保證，且在實際當中應用范圍更廣。通過為初始狀態、離散變遷與連續演變添加隨機因素，近年來已經提出一系列隨機或不確定性混成系統模型。文獻［6－8］考慮了具有隨機初始狀態的隨機混成系統，文獻［9－10］討論了具有隨機性離散變遷的混成系統。在文獻［11］中，使用隨機微分方程來刻畫系統的連續動態。通過將幾種隨機因素結合起來，可以得到較為一般的隨機混成系統［12－13］。除此以外，還有各種其他形式的混成系統，例如文獻［14］在仿射混成自動機中加入不確定性的向量場。文獻［15］在實時自動機中引入離散概率分布，稱為概率實時自動機。

對于隨機混成系統來說，安全性驗證問題是指對計算系統狀態到達不安全區域的概率。文獻［16］考慮離散時間的隨機混成系統，首先將其近似為有限狀態馬爾可夫鏈，然后計算安全性概率。文獻［7］利用逐段決定馬爾可夫過程來研究具有隨機初始狀態的混成系統。文獻［17］使用 SSMT(Stochastic Satisfiability Modulo Theory)來計算隨機或不確定混成自動機安全性概率的上下界。對于具有隨機初始條件的混成系統，ProbReach［6］將初始區域分割成足夠小的區間然后分段進行驗證，其不足在于計算負擔較重，而相比之下SReach［18］雖然利用統計檢驗可以處理大規模問題，但只能得到統計意義下的結果。此外，以上兩種工具都只能驗證在有界時間有限步內的安全性。

障礙驗證［19］是混成系統安全性驗證中的一種重要的方法，其主要思想是尋找一個障礙函數，將可達集與不安全區域分開，從而確保系統的安全性，與其他方法相比，障礙驗證具有計算簡單，易于驗證的特點。文獻［11］將其推廣到連續動態由隨機微分方程刻畫的混成系統中。對于同時具有隨機連續動態和離散動態的隨機混成系統［12］，文獻［20］進一步給出了障礙驗證條件。對于具有隨機初始狀態的隨機連續系統，文獻［8］給出了一種基于初始集選擇的障礙驗證方法。然而，對于同時在初始狀態、離散變遷與連續演變方面具有隨機性的一般隨機混成系統，目前尚未有文獻給出基于障礙驗證的方法。為了對這類系統進行研究，一種自然的想法是對單個隨機連續系統進行研究，然后結合這些連續系統的性質和離散跳轉的條件得出隨機混成系統的性質。

受文獻［8］啟發，本文基于初始集選擇的方法提出一種隨機連續系統障礙驗證方法，從而驗證隨機連續系統的安全性。本文的主要工作為:給出隨機連續系統安全性驗證的充分條件，并對半代數隨機連續系統給出隨機障礙函數求解的方法。

1 預備知識

本章主要介紹本領域的基礎知識與本文中需要用到的基本概念，包括連續動力系統、隨機連續系統、障礙驗證、平方和分解等;然后闡明本文希望解決的問題。在后文中，R代表實數集，x=(x1，x2，…，xn)T表示變量， x表示變量x對時間t的導數。除非特別說明，以下提到的X、I以及XU均默認為有界閉集，f和g為連續函數。

1.1 連續系統

自治的連續系統通常由以下常微分方程組刻畫:

其中f:Rn→Rn稱為向量場，或微分規則。通常要求f滿足Lipschitz連續性，即存在常數K，使得:

連續系統的定義如下:

定義1 連續系統。連續系統S由多元組〈X，D，I，XU〉構成，其中:

1)X Rn稱為位置不變集;

2)D定義了X上的微分規則 x=f(x)，其中f滿足X上的Lipschitz連續性;

3)I Rn表示初始狀態集合;

4)XURn為不安全區域。

對于連續系統S，從初始點x0∈I出發的軌線指的是方程限制在X中的解，所有從初始狀態集出發的軌線的并集稱為連續系統S的可達集。

在連續系統中，常常關心如下的安全性驗證問題:對于給定的連續系統S，從初始區域I出發的軌線是否會進入不安全區域XU。如果任意從初始區域出發的軌線不會進入不安全區域，則稱該連續系統是安全的。

1.2 障礙驗證

對于連續系統的安全性驗證問題，一種簡單的想法是尋找一條曲線，將系統的可達集與不安全區域分開，從而證明系統的軌線不可能進入不安全區域，如圖1所示。為此，只需要尋找一個實函數B(x)，使其將可達集中的所有狀態映成負數，將不安全區域映成正數，從而證明可達集與不安全區域交集為空。在障礙驗證中，障礙函數B(x)可利用系統的一些性質求出，從而避免了直接計算系統可達集的困難。文獻［19］給出了連續系統障礙驗證的一個充分條件，現陳述如下。

定理1 對于連續系統S=〈X，D，I，XU〉，如果存在連續可微函數B:Rn→R滿足:

一般來說，障礙函數的構造與驗證并非一件容易的事，但是當連續系統為半代數系統，即微分規則D由多項式給出，并且位置不變集X，初始區域I與不安全區域XU由多項式的等式或不等式給出時，可以利用平方和規劃求解出多項式形式的障礙函數。

圖1 連續系統障礙驗證Fig.1 Barrier certificates of continuous system

1.3 平方和

多項式的非負性判定是很多領域中的基本問題，例如動力系統的穩定性分析問題可歸結為驗證某些條件非負。然而，多項式的非負性判定問題是NP-hard問題［21］，這促使人們使用一些易于判斷的充分條件。平方和(Sum of Squares，SOS)分解就是這樣一種可在多項式時間內驗證的條件。

首先介紹平方和多項式的基本概念。對于給定的多項式p(x)，如果存在一組多項式 p1(x)，p2(x)，…，pm(x)，滿足p(x)的平方和分解。顯然，如果p(x)為平方和多項式，那么p(x)≥0，反之則不一定成立，例如考慮Motzkin多項式［22］:

該多項式是非負多項式，但是無法表示成平方和的形式。事實上，只有在以下三種情況下非負多項式才一定能寫成平方和多項式的形式:一元多項式，2次多項式，或者次數為4的二元多項式，在其他情況下非負多項式不一定存在平方和分解。

對于給定的多項式是否可以存在平方和分解的問題，有以下結論［23］:設 p(x) ∈ R［x］，次數為 deg p=2d，則判斷p(x)是否為平方和多項式等價于判斷p(x)能否寫成二次型ZTQZ的形式，其中Z是由次數不大于d的單項式構成的向量，Q為半正定矩陣，稱為p(x)的Gram矩陣。半正定Gram矩陣的存在性可由半定規劃(Semidefinite Programming，SDP)的方法求解。

例1［24］試將多項式 p(x1，x2) =+－－－表示平方和多項式的形式。

于是p(x1，x2)=ZTQZ轉化為以下半定規劃可行性問題:q11=5，q22=2，2q12+q33= － 1，q13= － 1，q23= － 1，Q 0。利用SeDuMi［25］等軟件包求解上述半定規劃問題，得到Q的一個可行解:當q12=－1且q33=1時Q為半正定矩陣，且Q=LTL，其中L。于是有以下平方和分解:

根據上面的討論可知，多項式的非負性判斷非常困難，而判定多項式是否為平方和多項式可以轉化為半定規劃問題，從而可以在多項式時間內完成驗證。

以下基于平方和松弛方法給出半代數連續系統障礙驗證的充分條件。

定理2 設半代數連續系統S的位置不變集X、初始區域I與不安全區域XU分別由下式給出:

其中θX(x)、θI(x)、θU(x)表示多項式向量。如果存在多項式B(x)∈R［x］，常數ε＞0以及平方和多項式向量σX(x)、σI(x)、σU(x)，滿足:

其中，S表示平方和多項式全體構成的集合，那么連續系統S是安全的，且B(x)為障礙函數。

上述定理的正確性依賴于以下事實:如果 p(x)=σ1(x)+σ2(x)q(x)，σ1(x)，σ2(x)∈S，那么由q(x) ≥0可推出 p(x)≥ 0。類似地，如果 p(x) = ε+σ1(x) +σ2(x)q(x)，ε ＞ 0，σ1(x)，σ2(x) ∈ S，那么 q(x) ≥ 0 p(x) ＞0。

為了將定理2應用到實際的半代數連續系統的安全性驗證中，首先要確定所要尋找的障礙函數次數的上界(可以隨意決定，但是次數的提高會導致計算復雜度的提高)，假設要尋找次數為2d的障礙函數，則可以將障礙函數寫成B(x)=的形式，其中，bi(x)為次數不超過d

的單項式，ci∈R是未知量。接下來，人為取定乘子σX(x)、σI(x)與σU(x)的次數，并將乘子表示為單項式的線性組合，單項式的系數為未知數。將障礙函數B(x)以及乘子σX、σI、σU代入式(3)并將問題寫成二次型的形式，得到關于未知系數的線性方程組以及關于平方和多項式Gram矩陣正定的條件，于是可以通過半定規劃求解得到障礙函數B(x)。由于半定規劃問題具有多項式時間的解法，故上述的步驟可在多項式時間內完成。事實上，可以通過專門的平方和規劃軟件，如SOSTOOLS［26－27］等，直接對式(3) 進行求解。只需給定障礙函數與平方和多項式的次數上界，軟件會自動將問題轉化為半定規劃的形式，并使用內點法求解。一旦計算得到滿足式(3)的B(x)，則系統的安全性得證。如果沒有找到滿足條件的B(x)，則可以嘗試提高障礙函數次數的上界以擴大搜索范圍。同時也應考慮到，由于平方和多項式與非負多項式之間存在天然的不等價性，對于半代數連續系統，可能存在多項式障礙函數B(x)滿足定理1的條件卻不滿足定理2的條件的情況，此時，通過本文中描述的算法無法證明系統的安全性。

1.4 隨機連續系統

在混成系統安全性驗證的研究中，對單個連續系統的研究是極為重要的。為了研究一般性隨機混成系統的安全性驗證問題，必須考慮一個具有一定隨機性的連續系統。例如，可以考慮帶有不確定參數的連續系統，即系統的初始狀態由隨機變量定義，并且系統的連續動態行為由確定性微分方程刻畫。對于這類隨機連續系統，已有相關文獻對其進行研究。

本文中所考慮的隨機連續系統是一類具有隨機初始值，并且其連續動態由隨機微分方程刻畫的連續系統。具體定義如下。

定義2 隨機連續系統。隨機連續系統S由多元組〈X，D，Ω，XU〉構成，其中:

1)X Rn稱為位置不變集;

2)D=〈f，g〉定義了 X上的隨機微分方程 dx=f(x)dt+g(x)dw(t)，其中w(t)為n維布朗運動;

3)Ω是系統初始值所服從的分布;

4)XU是給定的不安全區域。

通常要求定義中的f和g滿足某些條件以確保解的存在唯一性［28］，例如 Lipschitz條件:

以及線性增長條件:

其中K1和K2為某常數。

設x0～Ω是給定的初始隨機變量，隨機連續系統S由x0出發的軌線指的是如下隨機微分方程限制在X上的解:

正式地說，設x(t)是X上滿足式(4)的隨機過程，停時τ為x(t)第一次離開X的內部的時間，則隨機連續系統的軌線是滿足如下條件的隨機過程:

1.5 問題描述

本文考慮半代數隨機連續系統，其約束條件由多項式給出。

定義3 半代數隨機連續系統。半代數隨機連續系統是一個隨機連續系統〈X，D，Ω，XU〉，滿足:

1)隨機微分方程的漂移項f和擴散項g都是多項式;

2)位置不變集X和不安全區域XU都是半代數集(由多項式等式與不等式給出)。

對于給定的半代數隨機連續系統S，本文所研究的安全性驗證問題指的是從x0～Ω出發的軌線不進入不安全區域XU的概率的下界。換句話說，即尋找p∈［0，1］使得:

2 隨機連續系統安全性分析

由于本文所討論的隨機連續系統同時在初始狀態和連續動態方面具有隨機性，故對其進行安全性驗證時，需要同時考慮這兩方面的隨機性，較為復雜。為了解決概率安全性驗證問題，本文首先將問題轉化為相應的具有確定性初始狀態區域的隨機連續系統，其連續動態由隨機微分方程刻畫。然后利用隨機障礙函數驗證的方法求解該隨機連續系統并使用平方和松弛的方法計算出安全性概率下界。具體而言包含以下幾個步驟:

1)根據隨機連續系統S的初始分布Ω確定帶參數的初始狀態集I(α);

2)計算具有確定性初始狀態集I(α)的隨機連續系統的安全性概率的下界;

3)通過調整α的取值，可以找到安全性概率盡可能好的下界。

2.1 初始狀態集

為了克服隨機連續系統同時具有隨機性的初始狀態和隨機微分方程的難點，首先將系統轉化為具有確定性初始狀態集的隨機連續系統，即考慮軌線從初始狀態集I中的某個狀態出發的隨機連續系統，其中I Rn是有界閉集。與本文中定義的隨機連續系統S相比，該系統僅僅在刻畫其連續動態時引入了隨機微分方程。以下將初始狀態集為I的隨機連續系統記為SI。對于給定的初始分布Ω，本文考慮如下形式的初始區域:

其中:α是待定的參數;I(α)是有界閉集。

考慮到不同的概率分布具有不同的密度函數，一種自然的想法是根據其密度函數來選擇系統的初始區域。以下通過四種不同的初始概率分布為例來闡述其思想。

2.1.1 均勻分布

均勻分布，或稱為連續型均勻分布，是一種簡單的連續型概率分布，其密度函數在支集上處處相等。均勻分布在概率統計中有許多應用，例如根據最大熵原理，如果對某個隨機變量的性質一無所知，則可假設其服從均勻分布。

設初始狀態 x0= ［x1，x2，…，xn］T為隨機向量，其中 x1，x2，…，xn為獨立隨機變量。對于每個 i∈ {1，2，…，n}，xi服從［li，ui］上的均勻分布，即xi～ U(li，ui)，則x0的密度函數為:

隨機向量x0在超立方體{x∈Rn|li≤xi≤ui，1≤i≤n}中等可能性地取值。因此，對于均勻分布，選擇初始狀態集:

其中ci=(ui+li)/2，ri=(ui－ri)/2，α為0到1之間的參數。顯然，初始狀態落在IU(α)中的概率為:

2.1.2 指數分布

在概率論中，指數分布常用來表示獨立事件發生的間隔，如旅客進機場的時間間隔等。此外，許多電子設備的壽命也服從指數分布，有些系統的壽命也近似服從指數分布。指數分布的特點在于，隨著間隔時間變長，事件發生的概率急劇下降。

設 x1，x2，…，xn為獨立隨機變量，xi－ μi服從參數為 λi的指數分布，即xi－ μi～ E(λi)，其中i=1，2，…，n。則xi的密度函數可以表示為:

其中λi為大于0的常數。初始狀態x0的聯合密度函數為:

為了反映指數型分布的特性，考慮如下形式的初始區域:

其中β為給定的閾值。通過簡單的計算可知，ρ(x)≥β等價于:

其中α≥0。

根據文獻［8］，初始狀態x0落在IE(α)中的概率可由式(11)計算:

2.1.3 正態分布

在概率論中，正態分布是一種極為重要的連續型概率分布，其密度函數曲線常被稱為鐘形曲線。正態分布具有許多良好的性質，例如，兩個正態隨機變量的和差服從正態分布。根據中心極限定理，在某些條件下，大量相互獨立的隨機變量，其均值的分布以正態分布為極限。因此，在自然科學與社會科學的領域中，有時常用正態分布來近似某些未知的分布。另外，由于正態分布的熵在所有的已知均值及方差的分布中最大，這使得它作為一種均值以及方差已知的分布的自然選擇。

以下考慮x0的每個分量是獨立的正態隨機變量的情況。設x1，x2，…，xn為獨立的隨機變量，分別服從均值為μi、方差為σ2i的正態分布，其密度函數為:

其中1≤i≤n。于是x0的聯合密度函數可表示為:

考慮ρ(x)的β上水平集:

上式等價于:

即:

其中α為大于0的參數。

2.1.4 聯合正態分布

聯合正態分布可以看成是正態分布的一般情況。若隨機向量珘g是k維標準高斯隨機向量，即其元素為獨立的隨機變量，服從均值為0、方差為1的標準正態分布，如果存在矩陣A ∈Rn×k及向量 μ ∈Rn，使n元隨機向量x滿足x=A珘g+μ，則稱x為高斯向量，或稱其滿足聯合正態分布。向量μ為x的均值，協方差矩陣為Σ =AAT。

現假設初始狀態x0服從n元聯合正態分布，其均值為μ∈Rn，協方差矩陣為Σ∈Rn×n。根據定義，如果Σ為正定矩陣，則x0的密度函數為:

其中，|Σ|表示Σ的行列式。

考慮ρ(x)的β上水平集:

等價于:

不難看出，2.1.3節定義的IN(α)是IJN(α)的特殊情況。事實上，如果獨立的隨機變量x1，x2，…，xn分別服從均值為μ1，μ2，…，μn和方差為，，…，的正態分布，則 x0=［x1，x2，…，xn］T服從均值為μ = ［μ1，μ2，…，μn］T及協方差矩陣為 Σ =diag(，σ22，… ，σ2n)的聯合正態分布。此時IN(α)與IJN(α)定義一致。

根據文獻［29］，初始狀態x0落在IJN(α)的概率為:

其中Γ為伽瑪函數。注意到式(14)中的概率與μ和Σ無關，故對于x0的分量為獨立的正態隨機變量的情況，同樣有:

2.2 安全性驗證

2.2.1 隨機障礙驗證

對于隨機連續系統，也可以借鑒障礙驗證的思想，求出滿足特定條件的隨機障礙函數以驗證系統的安全性。然而，由于此時系統的軌線是一個隨機過程，因此使用障礙函數分離初始區域和不安全區域的思想在此不適用。類比于確定性連續系統S障礙驗證的條件中要求B(x(t))隨著時間t增長而遞減的性質，在隨機連續系統障礙驗證中要求B(x(t))是上鞅(相關內容可參考文獻［28］)，即對于任意s≤t，B(x(t))關于s之前的所有時刻的期望小于B(x(s))。直觀地說，B(x(t))在期望的意義下關于時間t遞減或保持不變。

以下陳述對于具有確定性初始狀態的隨機連續系統障礙驗證的結論。

定理 3［11］對于隨機連續系統 SI= 〈X，D，I，XU〉，其中D=〈f，g〉表示隨機微分方程 dx=f(x)dt+g(x)dw(t)，且軌線x(t)從x0∈I出發。如果存在二次連續可微函數B:Rn→R滿足:

則系統不安全的概率滿足:

由式(15)可知，任意從初始集I出發的軌線滿足0≤B(x0)≤γ，且B(x)不安全區域U上取值至少為1。此外，隨著時間演變，隨機過程B(x(t))始終非負。另外事實上由式(16)可以推出B(x(t))是上鞅，因此從直觀上說，如果γ越小，那么隨著時間t的演變，隨機過程B(x(t))的值從γ增長到1的概率越小，從而軌線x(t)進入不安全區域XU的概率越小。

利用定理3，可以得到關于隨機連續系統S安全性驗證的結論。

定理4 設S=〈X，D，Ω，XU〉是給定的隨機連續系統，其中 D =〈f，g〉表示隨機微分方程:dx = f(x)dt+g(x)dw(t)，區域I X是根據初始分布Ω所選擇的初始狀態區域。如果存在二次連續可微函數B:Rn→R滿足式(15)與(16)，則系統的安全性概率可由如式(19)計算:

證明 由于I是系統的初始狀態區域，由定理3知，任意從I出發的軌線滿足:

P{x(t) XU， t≥0|x(0)=x0}≥1－γ從而有:

由I X可知:

因此安全性概率下界得證。

2.1 節中分別對隨機連續系統S的幾種常見的初始分布進行討論。如果初始狀態服從獨立的均勻分布，則選取初始狀態集I(α)為式(8)。如果初始狀態服從其他三種分布，則考慮其密度函數的上水平集，分別選取初始狀態集為式(10)、(12)、(13)。初始狀態落在選定的初始狀態集的概率可由相應公式計算。安全性概率的下界為:

其中γα表示初始集為I(α)時由定理3得出的不安全的上界。若記:

則根據式(19)，系統安全性概率的下界計算式如下:

2.2.2 求解隨機障礙函數

由于式(16)和(17)是障礙驗證的充分條件，這意味著可以通過尋找不同的B(x)與γ使得Psafe的下界盡可能大，因此問題可以表述成如下形式:

其中:I(α) Rn是根據分布Ω選定的初始集;A R是參數α的取值范圍，例如對于均勻分布有A=(0，1］，而對于其他三種分布有A=(0，+∞)。

由于式(21)中的隨機障礙函數B(x)∈C2(X)，故其本質上是個無窮維的優化問題。為了便于求解，將問題轉化為給定次數上界的平方和規劃問題，從而可以使用SOSTOOLS等求解平方和規劃的軟件對問題進行求解。

設半代數集X、XU和I(α)分別定義如下:

則可以對式(21)進行平方和松弛:

其中S表示平方和多項式全體構成的集合。不難看出，如果p和分別是問題(21)與(22)的解，那么安全性概率滿足:

根據式(22)及(23)，設計求解隨機連續系統S安全性概率Psafe下界的算法1如下。

算法1 計算安全性概率的下界。

輸入 半代數隨機連續系統S，多項式隨機障礙函數B(x)的次數 k，平方和多項式 σX(x)，σU(x)，σI(x)(x) 的次數 d;

輸出 安全性概率的下界^p。

1) 根據初始分布Ω給出初始狀態集的模板I(α)并確定α的取值范圍A。

2)根據d與k分別設定σX(x)，σU(x)，σI(x)，珘σX(x)與B(x)的模板。

3) 將A離散化并在其中取若干α值作循環:

b) 利用SOSTOOLS求解以下問題:

c) 對第b)步中得到的結果進行平方和檢驗:如果σX(x)，σU(x)，σI(x)，珘σX(x)可以進行平方和分解，則記^p←(1－γ)Pα。

4) 將第3)步中選取的最大的^p值作為安全性概率的下界。

需要特別說明的是，算法中的第c)步的平方和檢驗是為了避免在b)步中由于數值誤差可能得到不正確的結果。這種情況經常在deg(B(x))較高、計算誤差較大的情況下出現。對于次數較低的情況，省略平方和檢驗的步驟對結果的正確性影響不大。

2.2.3 算法復雜度分析

算法1可以分成兩個部分:確定初始集I(α)并計算初始狀態的概率Pα，以及基于平方和松弛的方法求解初始集為I(α)的隨機連續系統。

關于前者，如果選定的初始集I(α) X，那么可以直接利用2.1 節中給出的式(9)、(11)、(14)、(15) 計算 Pα，否則需要對Pα另行計算，例如可以通過蒙特卡羅法求概率的近似值，復雜度為O(1)。

后者的關鍵在于求解一個平方和問題。通過將問題中的多項式用二次型的形式表示，判斷多項式是否為平方和多項式可以轉化為判斷對應的Gram矩陣是否半正定的問題，據此可以將第b)步中的平方和問題轉化為半定規劃可行性問題，運用內點法可以對其進行求解，復雜度為O(+)，其中N代表半定規劃問題中優化變vars量個數，Ncons代表限制條件的個數。為簡便起見，以下假設θX、θU、θI的維數至多為K。不難看出，問題的變量個數為:

約束條件個數為:

其中:

因此有 Nvars=O(nk+Knd)以及 Ncons=O(n「d'/2?+Knd/2)。如果位置不變集X和不安全區域XU由超立方體或者橢球給出，則對于本文中給出的四種初始狀態集均有K≤n，此時有 Nvars～ nk，Ncons～ n「d'/2?。設s=max{k，deg f，2deg g －1}，此時第b)步平方和規劃的復雜度可以表示為O(n4s)。類似可得，第c)步的平方和檢驗復雜度為O(n3.5d+1)。如果算法在第3)步中取了m個α的值，那么整個算法的復雜度可表示為O(mn4s)。

3 數值實驗與分析

本章中選取多個隨機連續系統的例子求解其安全性下界。實驗中使用的計算機的處理器為2.5 GHz Intel Core i7，內存為16 GB，開發環境為 Matlab R2015b，SOSTOOLS的版本為 3.01。

例2［11］考慮以下隨機連續系統:

其中w(t)是1維Wiener過程。設不變式為:

初始狀態為:

不安全區域為:

取系統的初始集為:

設定隨機障礙函數的次數，使用算法1進行安全性驗證，結果如表1所示，“*”號表示SOSTOOLS得到的解未通過平方和檢驗，這代表結果可能存在一定的誤差。

表1 例2的安全性驗證結果Tab.1 Safety verification results of Eg.2

在表1中，當系統式(24)的擴散項越小時，安全性概率的下界也就越高。而對于固定的σ來說，提高B(x)的次數有助于尋找到更高的安全性下界。與此同時，deg B的提高會導致較高的計算復雜度與較大的數值誤差，因此在進行數值實驗時并未使用較高的次數。

例3［30］考慮隨機連續系統:

不變式為 X=［－1，1］2，不安全區域為:

初始分布分別為:

表2給出了對于四種分布的安全性驗證結果。

表2 例3的安全性驗證結果Tab.2 Safety verification results of Eg.3

為了進一步測試算法的性能，選擇多個隨機連續系統的例子，算法的結果與耗時如表3所示。

表3 隨機連續系統安全性驗證結果Tab.3 Safety verification results of stochastic continuous system

表3中:n代表變量的個數;m代表實驗中取的α的個數;^p代表隨機連續系統安全性的下界;T代表實驗的耗時。表3中前四行的結果來自同一個連續系統，而后四行的結果來自不同的連續系統，從表3中可以看出，初始分布對算法的性能影響不大，而隨機障礙函數次數的提高或是變量的增加都會顯著增加耗時。

4 結語

在以往混成系統或連續系統障礙驗證的工作中，只有對具有隨機初始狀態或隨機微分方程的系統的研究，然而對同時具有多種隨機因素的一般性系統進行驗證也是有必要的。本文針對具有隨機初始狀態以及隨機微分方程的隨機連續系統進行安全性驗證，基于初始集選擇的方法將問題轉化為具有確定性初始狀態的隨機連續系統，然后基于障礙驗證以及平方和松弛的方法得出系統安全性的理論下界，基于此可以對連續系統安全性進行分析。下一步，我們將研究如何利用本文所提方法對隨機混成系統進行安全性驗證。