A Decidable Dense Branching-time Temporal Logic

Salvatore La Torre and Margherita Napoli

To appear at Foundations of Software Technology and Theoretical Computer Science (FSTTCS2000), New Delhi, India, December 13-15 2000


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.

Server START Conference Manager
Update Time 14 Aug 2000 at 17:41:23
Maintainer fsttcs20@cse.iitd.ernet.in.
Start Conference Manager
Conference Systems