基于抽取-精化的概率系统假设-保证验证

Assume-guarantee verification of probabilistic systems based on abstraction refinement

假设-保证推理是标记迁移系统组合验证的有效手段,近期,假设-保证推理在概率系统的验证中也得到了应用。在推理中,假设的学习是通过Lstar算法来完成的。针对概率系统的假设-保证推理,提出了一种新的方法:首先直接对组合系统的一个组件进行抽取,得到一个初步的假设;通过与假设-保证规则进行多次交互,不断精化该假设;最后,要么得到一个适当的假设以证明结论的正确性,要么得到一个反例来证明结论不成立。

Assume-Guarantee reasoning is an efficient means of synthetic verification of label transi- tion systems. Recently, Assume-Guarantee reasoning has been used in verifying probabilistic systems. In the phase of reasoning, the learning of assume is accomplished by L start algorithm. In the paper, we propose a new method of Assume-Guarantee Reasoning for probabilistic systems. Firstly, a component of the composed system is abstracted directly to obtain an initial hypothesis. Secondly, by iterating with the Assume-Guarantee rule, the hypothesis is refined repeatedly. At last, a proper hypothesis is ob- tained to prove the correctness of the conclusion, or a counterexample is obtained to prove that the con- clusion is incorrect.