  We formalize the semantics of hybrid systems as sets of hybrid trajectories,
including those generated by an hybrid transition system. We study the
abstraction of hybrid trajectory semantics for verification, static analysis,
and refinement. We mainly consider abstractions of hybrid semantics which
establish a correspondence between trajectories derived from a correspondence
between states such as homomorphisms, simulations, bisimulations, and
preservations with progress. We also consider abstractions that cannot be
defined stepwise like discretization. All these abstractions are Galois
connections between concrete and abstract hybrid trajectory or discrete trace
semantics. In contrast to semantic based abstractions, we investigate the
problematic trace-based composition of abstractions.
