作者：张君华 黄志球 肖芳雄抽取精化概率自动机概率时间自动机组合验证
摘要：假设一保证推理是标记迁移系统组合验证的有效手段，近期，假设-保证推理在概率系统的验证中也得到了应用。在推理中，假设的学习是通过Lstar算法来完成的。针对概率系统的假设一保证推理，提出了一种新的方法：首先直接对组合系统的一个组件进行抽取，得到一个初步的假设；通过与假设一保证规则进行多次交互，不断精化该假设；最后，要么得到一个适当的假设以证明结论的正确性，要么得到一个反例来证明结论不成立。
注：因版权方要求，不能公开全文，如需全文，请咨询杂志社
