HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
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 Connect in order to contact the contributor
Submitted on : Thursday, October 5, 2006 - 5:56:19 PM
Last modification on : Monday, November 29, 2021 - 7:46:02 PM

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 Datacite

Share

Metrics

Record views

21

 

Contact                    Legal Notice                    Personal Data