The key to model checking algorithm is the computation of strongest post condition.This article encodes the bounded model checking problem for linear hybrid automata as formula of SAT Modulo theories for linear arithmetic.We divided the formula into two specific parts to obtain the interpolation with a linear time complexity.According to the properties of Craig interpolation theorem for first order logic

the interpolation as an over-approximation strongest post condition and can replace the original strongest post condition used in symbolic model checking for hybrid automata with exponential time complexity.This method does not require to the transition relation is fully expanded the same as bounded model checking to check satisfiability

also.We implement the hybrid systems model checking algorithm without false counter-example using the over-approximation strongest post condition operator together with bounded model checking algorithm.Experiments show that our approach can be more efficient than bounded model checking for hybrid systems.