In previous works, the timed logic TCTL was extended with importants modalities, in order to abstract transient states that last for less than k time units. For all modalities of this extension, called TCTL Delta, the decidability of the model-checking problem has been proved with an appropriate extension of Alur and Dill's region graph. But this theoretical result does not support a natural implementation due to its state-space explosion problem. This is not surprising since, even for TCTL timed logics, the model checking algorithm that is implemented in tools like UPPAAL or KRONOS is based on a so-called zone algorithm and data structures like DBMs, rather than on explicit sets of regions. In this paper, we propose a symbolic model-checking algorithm which computes the characteristic sets of some TCTL Delta formulae and checks their truth values. This algorithm generalizes the zone algorithm for TCTL timed logics. We also present a complete correctness proof of this algorithm, and we describe its implementation using the DBM data structure.