基于SAT的命题投影时序逻辑限界模型检测方法专利登记公告

专利名称：基于SAT的命题投影时序逻辑限界模型检测方法

摘要：本发明是一种基于SAT的命题投影时序逻辑限界模型检测方法，步骤是：用Kripke结构描述待验证系统模型M；用PPTL公式描述性质P；设定限界k；将PPTL限界模型检测转换为SAT问题；对SAT问题求解：有解，系统M不满足性质P，给出反例，无解，系统M有界满足性质P，增大k值，进入下一个检测周期，直到k值足够大且在每个限界模型检测周期内待验证系统M都有界满足性质P。本发明使用PPTL描述系统性质，解决了CTL和LTL表达能力有限的问题，并通过限制搜索长度减少搜索状态数，缓解了状态空间爆炸，融合了PPTL和B

专利类型：发明专利

专利号：CN201210102064.3

专利申请（专利权）人：西安电子科技大学

专利发明（设计）人：段振华;何佳;田聪;王小兵

主权项：一种基于SAT的命题投影时序逻辑限界模型检测方法，其特征在于：具体检测步骤包括：步骤1.首先为待验证系统建立模型M，M是一个描述待验证系统行为的有限状态迁移系统，采用Kripke结构描述模型M；步骤2.使用命题投影时序逻辑PPTL公式描述待验证系统的性质，得到PPTL描述的性质公式P，并将其等价转换为正则形NF，得到性质公式P的正则形NF(P)，进而得到性质非的正则形步骤3.设定限界模型检测的界限k，k为一个不大于完整区间长度的正整数，用来限定进行限界模型检测时的搜索长度，界限k的值在一个限界模型检测周期

专利地区：陕西