A decidable dense branching-time temporal logic

Abstract

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.