一种基于遗传算法的概率假设-保证验证方法与实现

Method for genetic algorithm-based probabilistic assume-guarantee verification and realization

概率假设-保证推理(Probabilistic Assume-Guarantee Reasoning)是一种用于缓解随机模型检测中状态空间爆炸的方法,其将整个系统的验证分解为对较小组件的验证,组合较小组件的验证结果以达到对整个系统的验证。针对目前基于学习的概率假设-保证推理过程的缺陷:因学习假设过程中所有中间结果都需要存储而造成很高的空间复杂度,提出一种基于遗传算法(Genetic Algorithm,GA)学习假设的概率假设-保证推理方法,并将其用于组合验证MDP的正则安全性质。遗传算法本质上是一种随机算法,它的正确性通过满足训练集中的所有约束条件保证。该方法不需要记录中间结果,只需记录问题域和训练集的编码。因此,大大降低了产生假设的空间复杂度。实现了该概率假设-保证推理框架的原型工具,并通过领导人选举协议的实例对比了其有效性。

The probabilistic assume-guarantee reasoning is an efficient method for combating the state space explosion problem in stochastic model checking.It decomposes the verification of a system into its smaller components and composes back the results.Because all the intermediate results need to be stored in the process of learning assumption,the present probabilistic assume-guarantee reasoning is in high space complexity.To deal with this,a novel probabilistic assume-guarantee reasoning framework by learning assumption is presented based on a genetic algorithm(GA),and is used to verify MDP about the regular safe property.GA is essentially a randomized algorithm,in which intermediate results donot be recorded,only the encoding of the problem domain and the training set need to be memorized.Therefore,it reduces the space complexity of reasoning process.The prototype for the probabilistic assume-guarantee reasoning framework is implemented,and results obtained by an example of a leader election protocol are proved to be effective.