Verification of timed bisimulation equivalence is generally difficult because of the state explosion caused by concrete time values. In this paper, we propose a verification method to verify timed bisimulation equivalence of two timed processes using a symbolic technique similar to [1]. We first propose a new model of timed processes, Alternating Timed Symbolic Labelled Transition System (A-TSLTS). In an A-TSLTS, each state has some parameter variables, whose values determine its behaviour. Each transition in an A-TSLTS has a quard predicate. The transition is executable if and only if its guard predicate is true underspecified parameter values. In the proposed method, we can obtain the weakest condition for a state-pair in a finite A-TSLTS, which the parameter values in the weakest condition must satisfy to make the state-pair be timed bisimulation equivalent.