矩形phase-portralt近似的关键是控制模态的有效划分.本文提出了基于定性推理的phase-portrait近似,给出了一种基于向量场、感兴趣多项式及其李导数动态特性的模态空间划分方法,并进一步给出了基于精化多项式的抽象模犁精化方法.实验结果表明,基于定性推理划分的phase-portrait近似验证明显地减少了模态空间的划分数目,提高了验证的效率.
The core of the rectangular phase-portrait approximation is the efficient partition of the control model. The phase-portrait approximation based on quality reasoning is proposed. An approach for mode partition is then presented based on the characteristic of the vector field, interesting polynomials and their Lie-derivative. A method for the refinement of the abstract model based on the refined polynomials is also given. Experiment shows that the phase-portrait approxi-marion based on the qualitative-reasoning partition obviously reduces the partition number of the mode state space, and enhances the verification efficiency.