基于定性推理仿射混合自动机的矩形精化

摘要

仿射混合自动机phase-portrait近似精化的关键是控制模态的有效划分.本文提出了定性推理的矩形精化，给出了一种基于失败集、向量场特性、感兴趣线性式及其李导数的模态空间划分方法，并进一步给出了基于精化线性式的迭代精化方法。实验结果表明，基于定性推理精化的phase-portrait近似显著地提高了验证的效率。