基于半张量积的完备性阈值求解方法-计算机应用研究.PDFVIP

第３３卷第９期 计 算 机 应 用 研 究 Ｖｏｌ３３Ｎｏ９ ２０１６年９月　 ＡｐｐｌｉｃａｔｉｏｎＲｅｓｅａｒｃｈｏｆＣｏｍｐｕｔｅｒｓ Ｓｅｐ．２０１６ 基于半张量积的完备性阈值求解方法 １，２ １ ２ 许海洋 ，庄　毅 ，刘振斌 （１．南京航空航天大学计算机科学与技术学院，南京２１００１６；２．青岛农业大学理学与信息科学学院，山东青 岛２６６１０９） 摘　要：为了精确地计算Ｋｒｉｐｋｅ模型的完备性阈值，将半张量积引入到有界模型检测的完备性阈值的计算中， 采用离散时间进化系统来研究Ｋｒｉｐｋｅ模型的状态进化拓扑结构，提出了基于半张量积的有界模型检测完备性阈 值的求解算法。通过实例说明了该方法能够求解Ｋｒｉｐｋｅ模型的完备性阈值。结果表明，利用矩阵采用代数方法 能够精确地计算模型的前向半径。 关键词：有界模型检测；完备性阈值；半张量积；离散时间系统 中图分类号：ＴＰ３０１．４　　　文献标志码：Ａ　　　　　文章编号：１００１３６９５（２０１６）０９２６４１０４ ｄｏｉ：１０．３９６９／ｊ．ｉｓｓｎ．１００１３６９５．２０１６．０９．０１７ Ｅｆｆｉｃｉｅｎｔｃｏｍｐｕｔａｔｉｏｎｏｆｃｏｍｐｌｅｔｅｎｅｓｓｔｈｒｅｓｈｏｌｄｖｉａｓｅｍｉｔｅｎｓｏｒｐｒｏｄｕｃｔｍｅｔｈｏｄ １，２ １ ２ ＸｕＨａｉｙａｎｇ ，ＺｈｕａｎｇＹｉ，ＬｉｕＺｈｅｎｂｉｎ （１．ＳｃｈｏｏｌｏｆＣｏｍｐｕｔｅｒＳｃｉｅｎｃｅ＆Ｔｅｃｈｎｏｌｏｇｙ，ＮａｎｊｉｎｇＵｎｉｖｅｒｓｉｔｙｏｆＡｅｒｏｎａｕｔｉｃｓ＆Ａｓｔｒｏｎａｕｔｉｃｓ，Ｎａｎｊｉｎｇ２１００１６，Ｃｈｉｎａ；２．ＳｃｈｏｏｌｏｆＳｃｉｅｎｃｅ＆ Ｉｎｆｏｒｍａｔｉｏｎ，ＱｉｎｇｄａｏＡｇｒｉｃｕｌｔｕｒａｌＵｎｉｖｅｒｓｉｔｙ，ＱｉｎｇｄａｏＳｈａｎｄｏｎｇ２６６１０９，Ｃｈｉｎａ） Ａｂｓｔｒａｃｔ：ＴｏｅｆｆｅｃｔｉｖｅｌｙｃｏｍｐｕｔｅｔｈｅｃｏｍｐｌｅｔｅｎｅｓｓｔｈｒｅｓｈｏｌｄｏｆＫｒｉｐｋｅｍｏｄｅｌ，ｔｈｉｓｐａｐｅｒｉｎｔｒｏｄｕｃｅｄｔｈｅｓｅｍｉｔｅｎｓｏｒｐｒｏｄｕｃｔ ｔｈｅｏｒｙｔｏｔｈｅｃｏｍｐｕｔａｔｉｏｎｏｆｃｏｍｐｌｅｔｅｎｅｓｓｔｈｒｅｓｈｏｌｄ，ａｎｄｓｔｕｄｉｅｄｔｈｅｔｏｐｏｌｏｇｉｃａｌｓｔｒｕｃｔｕｒｅｏｆｓｔａｔｅｅｖｏｌｕｔｉｏｎｏｆＫｒｉｐｋｅｍｏｄｅｌ ｔｈｒｏｕｇｈｔｈｅｄｉｓｃｒｅｔｅｔｉｍｅｅｖｏｌｕｔｉｏｎｓｙｓｔｅｍ．Ｉｔｐｒｏｐｏｓｅｄａｓｏｌｕｔｉｏｎａｐｐｒｏａｃｈｂａｓｅｄｏｎｓｅｍｉｔｅｎｓｏｒｐｒｏｄｕｃｔｆｏｒｃｏｍｐｕｔｉｎｇｔｈｅ ｃｏｍｐｌｅｔｅｎｅｓｓｔｈｒｅｓｈｏｌｄ，ａｎｄｕｓｅｄａｃａｓｅｓｔｕｄｙｔｏｃｏｍｐｕｔｅｔｈｅｃｏｍｐｌｅｔｅｎｅｓｓｔｈｒｅｓｈｏｌｄ．Ｔｈｅｒｅｓｕｌｔｓｈｏｗｓｔｈｅｓｏｌｕｔｉｏｎａｐｐｒｏａｃｈ ｃａｎａｃｃｕｒａｔｅｌｙｃｏｍｐｕｔｅｔｈｅｆｏｒｗａｒｄｒａｄｉｕｓｏｆＫｒｉｐｋｅｍｏｄｅｌｔｈｒｏｕｇｈｍａｔｒｉｘａｎａｌｙｓｉｓ． Ｋｅｙｗｏｒｄｓ：ｂｏｕｎｄｅｄｍｏｄｅｌｃｈｅｃｋｉｎｇ；ｃｏｍｐｌｅｔｅｎｅｓｓｔｈｒｅｓｈｏｌｄ；ｓｅｍｉｔｅｎｓｏｒｐｒｏｄｕｃｔ；ｄｉｓｃｒｅｔｅｔｉｍｅｓｙｓｔｅｍ 　　模型检测是一种形式化验证技术，用于自动验证系统的软 函数变量的次序。但ＢＭＣ是一种受限形式的模型检测，其完 件模型是否满足设计规范。在模型检验中，通常采用有限自动 备性阈值的确定对于ＢＭＣ的完备性具有十分重要的意义。 机的形式来描述系统模