Discrete abstractions of hybrid systems