Verifying LTL Properties of Hybrid Systems with K-Liveness