買專利賣專利找龍圖騰，真高效！ 查專利查商標用IPTOP,全免費！專利年費監控用IP管家,真方便！

龍圖騰網獲悉上海工業控制安全創新科技有限公司申請的專利一種獲取LTLf最小自動機的方法、設備、計算機可讀存儲介質獲國家發明授權專利權，本發明授權專利權由國家知識產權局授予，授權公告號為：CN114371849B 。

龍圖騰網通過國家知識產權局官網在2025-09-23發布的發明授權授權公告中獲悉：該發明授權的專利申請號/專利號為：202011101650.7，技術領域涉及：G06F8/40；該發明授權一種獲取LTLf最小自動機的方法、設備、計算機可讀存儲介質是由朱淑芳;盧卡斯M.塔巴雅拉;蒲戈光;摩西Y.瓦爾迪;劉虹;倪華;楊昆設計研發完成，并于2020-10-15向國家知識產權局提交的專利申請。

本一種獲取LTLf最小自動機的方法、設備、計算機可讀存儲介質在說明書摘要公布了：本發明提出了一種獲取LTLf最小自動機的方法，所述方法基于Brzozowski最小化自動機構造理論來完成LTLf到最小DFA構造。包括：對于給定的LTLf公式，首先利用工具MONA構造得到LTLf對應的反向確定化自動機，這個自動機可以接收原LTLf接收語言的反向序列；將該反向確定化自動機進行倒置，從而得到一個非確定有限狀態自動機NondeterministicFiniteAutomata,NFA；在NFA上進行子集構造法計算，并在該計算之后進行可達狀態計算，由此刪除所有的不可達狀態。根據Brzozowski理論，該DFA就是LTLf公式對應的最小化DFA。

本發明授權一種獲取LTLf最小自動機的方法、設備、計算機可讀存儲介質在權利要求書中公布了：1.一種獲取LTLf最小自動機的方法，其特征在于，包括如下步驟： 步驟1：將給定的LTLf公式進行時態邏輯運算符替換，得到對應的PLTLf公式；所述PLTLf公式接收的語言為LTLf公式接收語言的反向序列； 步驟2：將步驟1中的PLTLf公式進行一階邏輯編碼，得到一個FOL公式；所述FOL公式接收的語言等價于PLTLf公式的接收語言，是步驟1中LTLf公式接收語言的反向序列； 步驟3：將步驟2中的FOL公式作為工具MONA的輸入，得到一個確定化自動機A，其中，所述A的狀態集合具體化，遷移邊符號化；所述A的接收語言是步驟1中LTLf公式接收語言的反向序列； A＝P1，S1，s01，H1，Acc1，其中： 1P1是一組變量的集合； 2S1是一組狀態的集合； 3s01代表初始狀態； 4H1表示遷移關系，H1： 5是接收狀態的集合； 步驟4：對所述A進行倒置，獲得一個非確定自動機N；在N上進行確定化和可達狀態計算，得到一個步驟1中LTLf公式對應的最小確定化自動機D； N＝P2，S2，Acc2，HR，{s01'}，其中： 1P2是一組變量的集合，和A一致； 2S2是一組狀態的集合，和A一致； 3Acc2代表初始狀態集合，由于自動機倒置，將A中的接收狀態變為N中的初始狀態； 4HR表示遷移關系，HR＝{s',λ,s|s,λ,s'∈HR}； 5{s01'}是接收狀態的集合，由于自動機倒置，將A中的初始狀態變為N中的可接收狀態； 所述步驟4包括： 步驟4.1：對所述N進行子集構造法計算，得到一個確定化的自動機； 所述步驟4.1中，利用工具SPOT提供的API，將N轉化為弱非確定化Buchi自動機WN，具體操作如下： 1引入一個新的狀態sink； 2引入一個新的變量 3對于Acc2中的每個接收狀態s，添加一個從s到sink的遷移邊，遷移條件為 4對于每一條遷移邊，將遷移條件λ改為λ∧alive； 5對于新狀態sink，添加一個遷移條件為的自循環； 6將狀態sink標記為唯一的可接收狀態； 得到WN之后，調用SPOT提供的API函數tgba_powerset完成自動機確定化操作，函數tgba_powerset返回的是弱確定化Buchi自動機WB； 步驟4.2：對步驟4.1得到的確定化的自動機所有狀態進行遍歷，保留可達狀態，刪去所有不可達狀態，得到最小確定化自動機D； 所述步驟4.2中，調用SPOT的API函數來完成可達狀態計算，對應的函數為purge_unreachable_states；將步驟4.1中得到的WB作為輸入，函數purge_unreachable_states返回只包括可達狀態的弱確定化Buchi自動機WB’；隨后將WB’進行裁剪得到對應的有限狀態自動機；具體操作如下： 1將唯一的可接收狀態sink移除，同時移除所有到達和從sink出發的遷移邊； 2將所有留存的遷移邊上的alive變量賦值為true，刪除alive變量； 3將所有在條件下遷移到sink的狀態定義為最終有限狀態自動機的可接收狀態。

如需購買、轉讓、實施、許可或投資類似專利技術，可聯系本專利的申請人或專利權人上海工業控制安全創新科技有限公司，其通訊地址為：200333 上海市普陀區云嶺西路600弄6號樓7層；或者聯系龍圖騰網官方客服，聯系龍圖騰網可撥打電話0551-65771310或微信搜索“龍圖騰網”。