  We give a sufficient condition under which every finite-satisfiable formula
of a given PCTL fragment has a model with at most doubly exponential number of
states (consequently, the finite satisfiability problem for the fragment is in
2-EXPSPACE). The condition is semantic and it is based on enforcing a form of
``progress'' in non-bottom SCCs contributing to the satisfaction of a given
PCTL formula. We show that the condition is satisfied by PCTL fragments beyond
the reach of existing methods.
