Timed computation tree logic (TCTL) extends
CTL by allowing timing constraints on the temporal operators.
The semantics of TCTL is defined on a dense tree.
The satisfiability of TCTL-formulae is undecidable even if
the structures are restricted to dense trees obtained from
timed graphs. According to the known results there are two possible
causes of such undecidability:
the denseness of the underlying structure and the equality in the
timing constraints. We prove that the second one is the only source
of undecidability when the structures are defined by timed graphs.
In fact, if the equality is not allowed in the timing
constraints of TCTL-formulae then the finite satisfiability
in TCTL is decidable. We show this result by reducing this problem
to the emptiness problem of timed tree automata,
so strengthening the already well-founded connections between
finite automata and temporal logics.
