[发明专利]一种面向限界检测技术的系统模型构造方法

摘要

本发明涉及一种面向限界检测技术的系统模型构造方法，是基于概率模型检测工具PRISM。包括以下步骤：对于局部空间搜索深度k，在建模语言的全局变量声明处引入新的整数型变量newv，初始值为0；对语言中的每一条命令，依据符号“+”表示的概率分布将其分解成若干只包含一条赋值语句的命令；依据各命令中值为真的谓词数量以及谓词之间组合的不同分别添加新命令。新命令中谓词是三个部分的合取：值为真的谓词保持不变；值为假的谓词取其否定；对于任意谓词值为真的两条命令，令第一条命令对变量的赋值等于第二条命令对变量的赋值来构建新谓词。本发明可实施性强，工作量小，且保证了利用限界检测技术约简状态空间的效果，可应用于随机系统建模。

主权项

一种面向限界检测技术的系统模型构造方法，其特征在于包括以下步骤：步骤一，设整数k为所需构造的局部空间的深度，在建模语言的全局变量声明处引入一个新的全局变量newv，并设置成整数型，初始值为0，即添加语句newv : [0..k] init 0；步骤二，对语言中的每一条命令，依据符号“+”表示的概率分布进行分解，具体分解规则如下：原始命令：[] guard_1 ‑> prob_1 : update_1 + ... + prob_n : update_n分解后的命令：[] guard_1 ‑> prob_1 : update_1；[] guard_1 ‑> prob_2 : update_2；……[] guard_1 ‑> prob_n : update_n；步骤三,对每一个模块，依据各命令中值为真的谓词的数量以及谓词之间组合的不同重新构造模型；步骤四,为了防止出现死循环，在每一个模块的末尾添加如下命令： newv=k‑> newv’=newv；步骤五,将所有模块重新组合在一起构成新的建模语言。