1. A computer implemented method for determining the validity of a property of interest with respect to a hybrid system, wherein at least one of the property of interest and a guard of a mode change transition of the hybrid system comprise at least one polynomial, said method comprising the steps of: a) abstracting the hybrid system to create an abstract discrete system, wherein abstracting comprises constructing an abstract discrete system over a set of abstract states defined by the positive, negative, and zero valuation of a saturated set of polynomials constructed by saturating an initial set of polynomials selected from the polynomials contained in one or both of the property of interest and the guards of the mode change transitions of the hybrid system, wherein saturating comprises repeatedly choosing a polynomial from the selected set of polynomials and adding a time derivative of the chosen polynomial to the set unless the time derivative is a constant or a constant multiple of a polynomial already in the set; b) analyzing, using the computer, the validity of the property of interest with respect to the abstract discrete system; and c) outputting the validity of the property of interest on the computer display.