[發明專利]一種搜索帶前綴的邊界條件的方法

在審

• 申請號: 202110741024.2
• 申請日: 2021-06-30
• 公開（公告）號: CN113590916A
• 公開（公告）日: 2021-11-02
• 發明（設計）人: 萬海;楊濱好;羅煒麟;曾娟
• 申請（專利權）人: 中山大學
• 主分類號: G06F16/953
• 分類號: G06F16/953
• 代理公司: 廣州粵高專利商標代理有限公司 44102
• 代理人: 劉俊

1.一種搜索帶前綴的邊界條件的方法，其特征在于，包括以下步驟：

S1：定義帶前綴的邊界條件；

S2：從領域屬性Dom和目標條件Goal中提取變量集合V；

S3：初始化候選解C，設定初始解路徑長度為L；

S4：從初始解C出發局部搜索帶前綴的邊界條件P，設定搜索邊界條件最大步數為S；

S5：在設定的搜索時間內，重復步驟S3-S4，返回得到的帶前綴的邊界條件P。

2.根據權利要求1所述的搜索帶前綴的邊界條件的方法，其特征在于，所述步驟S1的具體過程是：

F(S)表示S在未來某一時刻為真，G(S)表示S在未來任一時刻都為真；

定義1：形如F(s₁∧G(s₂|s₃|…|s_m))的LTL公式稱為帶環公式，其中s_i為公式的項或者True或者False；

定義2帶前綴的邊界條件滿足邊界條件的三個條件：邏輯不一致性、極小性、非平凡性，且滿足F(s1L)形式，其中L為帶環公式，s₁為LTL公式中的項：

F(p∧r)

F(p∧G(！q|！p))

由定義可知，帶前綴的BC能夠直觀表示出路邊界條件的路徑遷移狀態，比任意的LTL公式更具有可讀性。

3.根據權利要求2所述的搜索帶前綴的邊界條件的方法，其特征在于，所述步驟S2中，從領域屬性Dom和目標條件Goal中提取公式中出現的變量集合，提取出的變量集合可以用來生成帶前綴的邊界條件初始的候選解。

4.根據權利要求3所述的搜索帶前綴的邊界條件的方法，其特征在于，所述步驟S3中，完全隨機生成形如F(uG(m))的候選解，其中u為路徑公式，u_i為路徑上第i個狀態，路徑長度為L,m為環內公式。

5.根據權利要求4所述的搜索帶前綴的邊界條件的方法，其特征在于，所述步驟S3中，對于u_i的生成：

a)、對于每個變量v∈V，從等概率取文字；

b)、將取的文字合取(∧)作為u_i。

6.根據權利要求5所述的搜索帶前綴的邊界條件的方法，其特征在于，所述步驟S3中，對于環內公式m的生成：

a)、對于每個變量v∈V，從等概率取文字；

b)、將取的文字析取(∨)作為m。

7.根據權利要求6所述的搜索帶前綴的邊界條件的方法，其特征在于，所述步驟S4的過程是：

S41：設定當前步數CurStep為0，搜索結果集合為P；

S42：當前步數CurStep自增1；

S43：判斷初始解C是否為帶前綴的邊界條件，如果不是，返回違反的是哪個特性；

S44：判斷當前步數CurStep是否小于搜索邊界條件最大步數S，若小于則執行S42，否則返回搜索結果集合P。

8.根據權利要求7所述的搜索帶前綴的邊界條件的方法，其特征在于，所述步驟S43中，如果C是帶前綴的邊界條件：

1)、將當前步數CurStep設為0；

2)、對C進行極小化操作，保證極小化后仍然為帶前綴的邊界條件；

3)、將C加入搜索結果P中；

4)、對C進行隨機擾動操作。

9.根據權利要求8所述的搜索帶前綴的邊界條件的方法，其特征在于，所述步驟S43中，如果C不滿足極小性：

1)、對C執行abstract操作，以保證得到更接近滿足極小值的公式；

2)、若操作結果C為帶前綴的BC：當前步數CurStep設為0；C加入搜索結果集合P；對C進行隨機擾動。

10.根據權利要求8所述的搜索帶前綴的邊界條件的方法，其特征在于，所述步驟S43中，如果C不滿足邏輯不一致性：

1)、對C執行refine操作，以保證得到更可能滿足不相容性的公式；

2)、若操作結果C為帶前綴的BC：當前步數CurStep設為0；C加入搜索結果集合P；對C進行隨機擾動。