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
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.
Document type :
Journal articles
Complete list of metadata

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



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⟩



Record views