[發明專利]一種運行時驗證中性質的可監控性概率的度量方法

有效

• 申請號: 202010157636.2
• 申請日: 2020-03-09
• 公開（公告）號: CN111352848B
• 公開（公告）日: 2021-07-20
• 發明（設計）人: 陳哲;陳云云;吳逸凡
• 申請（專利權）人: 南京航空航天大學
• 主分類號: G06F11/36
• 分類號: G06F11/36;G06F11/30
• 代理公司: 南京經緯專利商標代理有限公司 32200
• 代理人: 施昊

1.一種運行時驗證中性質的可監控性概率的度量方法，其特征在于，包括以下步驟：

(1)將給定的性質轉化為對應的監控器性質對應的監控器被表示為五元組的有限狀態機其中，Q是一個非空且有限的狀態集合；α＝2^AP是字母表，AP是被監控的全部事件集合，α中的元素被稱為符號，其中α^*表示所有有限符號序列的集合，α^ω表示所有無限符號序列的集合；δ：Q×α→Q是狀態遷移函數；q₀∈Q是初始狀態；λ：Q→是輸出函數，其中是三種輸出值，分別表示性質被滿足、違反和待定；

具體的轉化過程如下：

(101)構造的否定

(102)分別構造和對應的非確定性Büchi自動機和其中和接受同樣的無限符號序列集合，和接受同樣的無限符號序列集合；

(103)分別構造非確定性Büchi自動機和對應的非確定性有限自動機和其中，的狀態集合和狀態遷移函數與相同；當且僅當中存在一條從狀態q出發的被接受的無限符號序列，中的狀態q是接受狀態；和的關系與和的關系一致；

然后將非確定性有限自動機和確定化為確定性有限自動機和

(104)計算兩個確定性有限自動機和的笛卡爾積得到監控器其中的一個狀態由的狀態和的狀態構成；如果不是接受狀態，則狀態輸出如果不是接受狀態，則狀態輸出否則狀態輸出

(2)遍歷監控器獲取的初始狀態、遷移上的標簽公式、不可監控狀態集合U和不可監控狀態集合的前驅狀態集合其中，Pre*(U)表示集合U中所有狀態的所有前驅狀態的并集，\表示集合減法運算；在監控器中，如果狀態q∈Q滿足：λ(q)＝？且對于所有狀態r∈Post^*(q)都有λ(r)＝？，則狀態q被稱為不可監控狀態，其中，Post*(q)表示狀態q的所有后繼狀態的集合；

(3)根據不可監控狀態集合U判斷是否提前返回性質的可監控性概率結果；

(4)將監控器轉換為對應的離散時間馬爾可夫鏈其中，P：Q×Q→[0，1]是根據遷移上的標簽公式計算得到的遷移概率分布函數，兩個狀態q與q′之間的遷移概率等于監控器中二者之間遷移上的標簽公式對應的符號數量占字母表α中所有符號數量的比例，且對于所有狀態q∈Q，∑_q′∈QP(q，q′)＝1；是初始概率分布函數，其中只有q₀的初始概率不為0，即且對于所有狀態q∈Q\{q₀}，\表示集合減法運算；是標簽函數，即在所有狀態q∈Q上標注狀態名q和監控器中的輸出值λ(q)；

(5)根據監控器的不可監控狀態集合U、不可監控狀態集合的前驅狀態集合以及離散時間馬爾可夫鏈的遷移概率分布函數和初始概率分布函數，列出關于可監控性概率的線性方程組E：

x＝Ax+b

其中，表示從中每個狀態q出發到達集合U的概率x_q所組成的的矩陣，為一個的矩陣，表示從中狀態r到狀態s的遷移概率，為一個的矩陣，表示從中狀態t通過一次遷移到達集合U的遷移概率，其中b_t＝P(t，U)＝∑_q∈UP(t，q)；是從狀態q₀出發到達集合U的概率，是性質的可監控性概率；

(6)求解線性方程組E，得到性質的可監控性概率。

2.根據權利要求1所述運行時驗證中性質的可監控性概率的度量方法，其特征在于，在步驟(3)中，如果即監控器中沒有不可監控狀態，則性質是可監控的，即可監控性概率為1，直接返回1；如果U＝Q，即監控器中的所有狀態都是不可監控狀態，則性質是弱不可監控的，即可監控性概率為0，直接返回0。

3.根據權利要求1所述運行時驗證中性質的可監控性概率的度量方法，其特征在于，在步驟(6)中，求解線性方程組E，得到y的值即為性質的可監控性概率；求解方法包括人工求解和計算機自動求解。