Inevitability properties in branching temporal logics are of the syntax ∀◊φ, where φ is an arbitrary (timed) CTL formula. Such inevitability properties in dense-time logics can be analyzed with greatest fixpoint calculation. We present algorithms to model-check inevitability properties both with and without non-Zeno computation requirement. We discuss a technique for early decision on greatest fixpoint calculation. Our algorithms come with a d-parameter for the measurement of time-progress. We have experimented with various issues, which may affect the performance of TCTL inevitability analysis. Specifically, we report the performance of our implementation w.r.t. various d-parameter values and with or without the non-Zeno computation requirement in the evaluation of greatest fixpoints. We have also experimented with safe abstration techniques for model-checking TCTL inevitability properties. Analysis of experiment data helps clarify how various techniques can be used to improve verification of inevitability properties.