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.

翻译：我们给出了充分的条件,使PCTL碎片的每种可满足的公式都有一个最多具有双重倍数的状态模式(因此,该碎片的有限相对性问题出现在2-EXPSPACE中),这是语义性的,其依据是在非底部的SCC中执行一种“进展”形式,有助于满足特定PCTL公式。 我们证明PCTL碎片在现有方法无法达到的范围内满足了这一条件。