Abstract
Since their introduction by Merlin??in 1974, Time Petri nets have been widely used for the specification and verification of time constrained systems. The state??spaces of Time Petri nets are typically infinite. Model checking them first requires to produce finite abstractions for their state spaces preserving the properties of interest. The paper overviews the essential available abstractions.