This paper examines the feasibility of predicate abstraction as a method for the reachability analysis of hybrid systems.
A hybrid system can be abstracted into a purely discrete system by mapping the continuous state space into an equivalent finite
discrete state space using a set of Boolean predicates and a decision procedure in the theory of real closed fields. It is
then possible to find the feasible transitions between these states. In this paper, we propose new conditions for predicate
abstraction which greatly reduce the number of transitions in the abstract discrete system. We also develop a computational
technique for reachability analysis and apply it to a biological system of interest (the Delta-Notch lateral inhibition problem).