Skip to Main content Skip to Navigation
Conference papers

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.
Document type :
Conference papers
Complete list of metadata
https://hal.inria.fr/inria-00104142
Contributor : Mathieu Turuani <>
Submitted on : Thursday, October 5, 2006 - 5:56:19 PM
Last modification on : Monday, February 15, 2021 - 10:39:33 AM

Identifiers

  • HAL Id : inria-00104142, version 1

Collections

ENS-CACHAN | CNRS | ENS-PARIS-SACLAY

Citation

François Laroussinie, Philippe Schnoebelen, Mathieu Turuani. On the Expressivity and Complexity of Quantitative Branching-Time Temporal Logics.. LATIN 2000: Theoretical Informatics, 4th Latin American Symposium, Apr 2000, Punta del Este, Uruguay, pp.437-446. ⟨inria-00104142⟩

Export

BibTeX TEI DC DCterms EndNote

Share

Metrics

Record views

53

 

Contact                    Legal Notice                    Personal Data