2000 | OriginalPaper | Buchkapitel
A Decidable Dense Branching-Time Temporal Logic
verfasst von : Salvatore La Torre, Margherita Napoli
Erschienen in: FST TCS 2000: Foundations of Software Technology and Theoretical Computer Science
Verlag: Springer Berlin Heidelberg
Enthalten in: Professional Book Archive
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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.