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
Journal articles

On the expressivity and complexity of quantitative branching-time temporal logics.

François Laroussinie 1 Philippe Schnoebelen 1 Mathieu Turuani 2
1 LSV - Laboratoire Spécification et Vérification [Cachan]
2 CASSIS - Combination of approaches to the security of infinite states systems
FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174), Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
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.
Keywords : CTL Branching-time temporal logic Discrete time Expressivity Model checking Complexity
Document type :
Journal articles
Complete list of metadata
https://hal.inria.fr/inria-00104145
Contributor : Mathieu Turuani Connect in order to contact the contributor
Submitted on : Thursday, October 5, 2006 - 6:01:58 PM
Last modification on : Friday, January 21, 2022 - 3:08:57 AM

Links full text

openaccess

Identifiers

Collections

INRIA | CNRS | UNIV-FCOMTE | INRIA2 | UNIV-BM | FEMTO-ST | UNIV-BM-THESE | ENS-CACHAN | LORIA | UNIV-LORRAINE | LORIA-FM | ENS-PARIS-SACLAY

Citation

François Laroussinie, Philippe Schnoebelen, Mathieu Turuani. On the expressivity and complexity of quantitative branching-time temporal logics.. Theoretical Computer Science, Elsevier, 2003, Theoretical Computer Science, 1-3 (297), pp.297-315. ⟨10.1016/S0304-3975(02)00644-8⟩. ⟨inria-00104145⟩

Export

BibTeX TEI DC DCterms EndNote Datacite

Share

Metrics

Record views

86

 

Contact                    Legal Notice                    Personal Data