  Timed automata (TA) are a well-established formalism for specifying
discrete-state/continuous-time behavior of time-critical reactive systems.
Concerning the fundamental analysis problem of comparing a candidate
implementation against a specification, both given as TA, it has been shown
that timed trace equivalence is undecidable, whereas timed bisimulation
equivalence is decidable. The corresponding proof utilizes region graphs, a
finite, but generally very space-consuming characterization of TA semantics.
Hence, most practical TA tools utilize zone graphs instead, a symbolic and
generally more efficient representation of TA semantics, to automate analysis
tasks. However, zone graphs only produce sound results for analysis tasks being
reducible to plain reachability problems thus being too imprecise for checking
timed bisimilarity. In this paper, we propose bounded zone-history graphs, a
novel characterization of TA semantics facilitating an adjustable trade-off
between precision and scalability of timed-bisimilarity checking. Our tool
TimBrCheck is, to the best of our knowledge, the only currently available tool
for effectively checking timed bisimilarity and even supports non-deterministic
TA with silent moves. We further present experimental results gained from
applying our tool to a collection of community benchmarks, providing insights
into trade-offs between precision and efficiency, depending on the bound value.
