On the Expressivity and Complexity of Quantitative Branching-Time Temporal Logics.

François Laroussinie 1 Philippe Schnoebelen 1 Mathieu Turuani 1
1 LSV - Laboratoire Spécification et Vérification [Cachan]
Abstract : We investigate extensions of CTL allowing to express quantitative requirements about an abstract notion of time in a simple discrete-time framework, and study the expressive power of several relevant logics. When only subscripted modalities are used, polynomial-time model checking is possible even for the largest logic we consider, while the introduction of freeze quantifiers leads to a complexity blow-up.
Type de document :
Communication dans un congrès
Gaston H. Gonnet and Daniel Panario and Alfredo Viola. LATIN 2000: Theoretical Informatics, 4th Latin American Symposium, Apr 2000, Punta del Este, Uruguay, Springer, 1776, pp.437-446, 2000, Lecture Notes in Computer Science
Liste complète des métadonnées
https://hal.inria.fr/inria-00104142
Contributeur : Mathieu Turuani <>
Soumis le : jeudi 5 octobre 2006 - 17:56:19
Dernière modification le : jeudi 11 janvier 2018 - 06:20:13

Identifiants

  • HAL Id : inria-00104142, version 1

Collections

ENS-CACHAN

Citation

François Laroussinie, Philippe Schnoebelen, Mathieu Turuani. On the Expressivity and Complexity of Quantitative Branching-Time Temporal Logics.. Gaston H. Gonnet and Daniel Panario and Alfredo Viola. LATIN 2000: Theoretical Informatics, 4th Latin American Symposium, Apr 2000, Punta del Este, Uruguay, Springer, 1776, pp.437-446, 2000, Lecture Notes in Computer Science. 〈inria-00104142〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

31

Contact


archive-ouverte@inria.fr