In this report, we elaborate on the work done on showing max-plus polyhedra capable of representing the clock space for reachability checking of timed models. We show that there exist models where max-plus overaproximation is exact, but DBM overapproximation is not. We prove an extrapolation algorithm for single-dimensional max-plus polyhedra, and describe principles for an extrapolation algorithm for general max-plus polyhedra. Finally, we implement our max-plus polyhedra representation on top of a model checker for timed-arc Petri nets, and show that for some models where DBM overapproximation fails to provide correct results, max-plus overapproximation is faster than exact DBM analysis.