买专利卖专利找龙图腾，真高效！ 查专利查商标用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或微信搜索“龙图腾网”。