[發(fā)明專利]一種基于Büchi自動機化簡運行時驗證監(jiān)控器的方法

在審

• 申請?zhí)枺?/td>: 201811359544.1
• 申請日: 2018-11-15
• 公開（公告）號: CN109522713A
• 公開（公告）日: 2019-03-26
• 發(fā)明（設計）人: 錢俊彥;葉玲玲
• 申請（專利權）人: 桂林電子科技大學
• 主分類號: G06F21/52
• 分類號: G06F21/52;G06F9/448
• 代理公司: 桂林市持衡專利商標事務所有限公司 45107
• 代理人: 陳躍琳

1.一種基于Büchi自動機化簡運行時驗證監(jiān)控器的方法，其特征是，具體包括如下步驟：

步驟1、將線性時態(tài)邏輯公式描述的屬性轉換為非確定Büchi自動機；

步驟2、對于步驟2所得到的非確定Büchi自動機的狀態(tài)集合中的每個狀態(tài)，判斷以該狀態(tài)開始時，非確定Büchi自動機接受的語言是否為空：若為空，則對該狀態(tài)進行冗余標記；否則，該狀態(tài)不作標記；

步驟3、將步驟2所得到的有冗余標記的狀態(tài)從非確定Büchi自動機的狀態(tài)集合中刪除，得到初步簡化的非確定Büchi自動機；

步驟4、在步驟3所得到的初步簡化的非確定Büchi自動機中尋找互相滿足公平模擬關系的狀態(tài)對；

步驟5、對步驟4所得到的狀態(tài)對進行合并，得到最終簡化的非確定Büchi自動機；

步驟6、將步驟5所得到的最終簡化的非確定Büchi自動機轉化成非確定有限狀態(tài)自動機，再對非確定有限狀態(tài)自動機進行確定化后，得到確定性有限狀態(tài)自動機；

步驟7、將步驟6所得到的確定性有限狀態(tài)自動機作用于系統(tǒng)驗證的監(jiān)控器。

2.根據(jù)權利要求1所述的一種基于Büchi自動機化簡運行時驗證監(jiān)控器的方法，其特征是，步驟1的具體過程如下：首先，將線性時態(tài)邏輯公式描述的屬性轉化為交錯自動機；接著，將交錯自動機轉化成廣義的Büchi自動機；最后，把廣義的Büchi自動機轉化為非確定Büchi自動機。

3.根據(jù)權利要求1所述的一種基于Büchi自動機化簡運行時驗證監(jiān)控器的方法，其特征是，步驟5，在進行狀態(tài)對的合并時，需要檢查合并狀態(tài)對后是否會改變初步簡化的非確定Büchi自動機接受的語言：如果接受的語言沒有改變，則對該對狀態(tài)對進行合并，并移除合并后多余的轉移關系；否則，不進行狀態(tài)對的合并。