Affordable Access

Publisher Website

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

Authors
Journal
Theoretical Computer Science
0304-3975
Publisher
Elsevier
Publication Date
Volume
297
Identifiers
DOI: 10.1016/s0304-3975(02)00644-8
Keywords
  • Ctl
  • Branching-Time Temporal Logic
  • Discrete Time
  • Expressivity
  • Model Checking
  • Complexity

Abstract

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.

There are no comments yet on this publication. Be the first to share your thoughts.