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

J4 ›› 2013, Vol. 35 ›› Issue (3): 128-133.

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

张君华1,黄志球2,肖芳雄3

(1.宁波大学职业技术教育学院，浙江宁波 315100;
2.南京航空航天大学计算机科学与技术学院，江苏南京 210016;
3.广西财经学院信息与统计学院，广西南宁 530003)

收稿日期:2012-08-06 修回日期:2012-11-15 出版日期:2013-03-25 发布日期:2013-03-25
基金资助:
国家自然科学基金资助项目(61272083，61262002)；宁波市自然科学基金资助项目(2012A610063)

Assumeguarantee verification of probabilistic systems
based on abstraction refinement

ZHANG Junhua1,HUANG Zhiqiu2,XIAO Fangxiong3

(1.Vocational Education Faculty,Ningbo University,Ningbo 315100;
2.College of Computer Science and Technology,Nanjing University of Aeronautics and Astronautics,Nanjing 210016;
3.School of Information and Statistics,Guangxi University of Finance and Economics,Nanning 530003,China)

Received:2012-08-06 Revised:2012-11-15 Online:2013-03-25 Published:2013-03-25

摘要/Abstract

摘要：

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

关键词: 假设-保证验证, 抽取精化, 概率自动机, 概率时间自动机, 组合验证

Abstract:

Assume-Guarantee reasoning is an efficient means of synthetic verification of label transition 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 obtained to prove the correctness of the conclusion, or a counterexample is obtained to prove that the conclusion is incorrect.

Key words: assume-guarantee verification;abstraction refinement;probabilistic automata;probabilistic timed automata;compositional verification

张君华1,黄志球2,肖芳雄3. 基于抽取-精化的概率系统假设-保证验证[J]. J4, 2013, 35(3): 128-133.

ZHANG Junhua1,HUANG Zhiqiu2,XIAO Fangxiong3. Assumeguarantee verification of probabilistic systems
based on abstraction refinement [J]. J4, 2013, 35(3): 128-133.