面向复杂随机系统的启发式统计模型检测方法

统计模型检测是一种高效的验证技术,常用于复杂的随机系统验证,如分布式算法等,而在超长路径上对性质进行验证时,其验证效率会急剧降低。为解决这个问题,提出一种启发式的统计模型检测算法。在对路径进行验证时,会查找帮助剪枝的最短前缀;在后续抽样时,利用前缀信息直接判定路径是否满足给定性质,避免进入费时的路径验证阶段。在与PRISM的比较中,它的路径验证次数相对更少,且平均抽样路径长度更短。因此统计模型检测技术可应用于超长路径上的性质验证。