The Satisfiability Problem for a Quantitative Fragment of PCTL

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.