Abstract: Abstraction is a dominant approach for verification of hybrid systems. Model transformation is to construct a decidable （or semi-decidable） hybrid automaton to over-approximate the original automaton. In this paper, we extend the linear phase-portrait app

Key words: Hybrid automaton ,Weak time simulation, Phase-portrait approximation