We consider quantitative model checking in durational Kripke structures
(Kripke structures where transitions have integer durations) with
timed temporal logics where subscripts put quantitative constraints on the
time it takes before a property is satisfied.
We investigate the conditions that allow polynomial-time model checking
algorithms for timed versions of CTL and exhibit an important gap
between logics where subscripts of the form ``=c'' (exact
duration) are allowed, and simpler logics that only allow subscripts of the
form ``<=c'' or ``>=c'' (bounded duration).
A surprising outcome of this study is that it provides the second example of
a Delta_2^p-complete model checking problem.
