Bidirectional refinement of affine hybrid systems based on qualitative reasoning

The core of phase-portrait approximation verification of affine hybrid system is the refinement direction and strategy of the abstract model. In this paper, a bidirectional refinement strategy based on qualitative reasoning is proposed, an approach for mode partition is presented based on the dynamic properties of the system. Refinement of abstract model iterates between the computation of forward- and backward-reachability based on refined linear expressions, realizing the local optimization of the refinement. Experiment shows that bidirectional refinement based on qualitative reasoning distinctly enhances the verification efficiency.