公开(公告)号：CN107292027A

公开(公告)日：2017-10-24

申请号：CN201710474771.8

申请日：2017-06-21

Applicant: 同济大学

Inventor： 张苗苗 ,  徐立云 ,  张剑 ,  朱芳来 ,  施枫

IPC: G06F17/50

CPC classification number: G06F17/504 ,  G06F2217/06

Abstract: 本发明涉及一种基于扩展的线性时段不变式的有界模型检验方法，包括以下步骤：S1，根据给定离散时间语义下时间自动机T和扩展的线性时段不变式公式Φ，构建辅助自动机H；S2，在观测时间设定的范围内，检测各整数时间点的时间自动机T是否满足公式Φ，获取不满足公式Φ的状态的集合；S3，定义计算树时序逻辑公式，用于描述集合的性质；S4，检测时间自动机T和辅助自动机H的组成产品是否满足计算树时序逻辑公式，若不满足，则时间自动机T满足扩展的线性时段不变式公式Φ，否则时间自动机T不满足扩展的线性时段不变式公式Φ。与现有技术相比，本发明具有更加好的效率以及更加低的算法复杂度。