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

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 introducing freeze quantifiers leads to a complexity blow-up. © Springer-Verlag Berlin Heidelberg 2000.