仿射混合自动机phase-portrait近似验证的关键是抽象模型精化的方向和策略.本文提出了一种基于定性推理的双向精化策略,给出了依据系统动态特性的模态划分方法,抽象模型的精化基于精化线性式在前向可达集和后向可达集两个方向上迭代执行,实现了精化过程的局部优化.实验结果表明,基于定性推理的双向精化策略显著地提高了验证的效率.
科研之友
微信
新浪微博
Facebook
分享链接
