  The model-checking problem for probabilistic systems crucially relies on the
translation of LTL to deterministic Rabin automata (DRW). Our recent Safraless
translation for the LTL(F,G) fragment produces smaller automata as compared to
the traditional approach. In this work, instead of DRW we consider
deterministic automata with acceptance condition given as disjunction of
generalized Rabin pairs (DGRW). The Safraless translation of LTL(F,G) formulas
to DGRW results in smaller automata as compared to DRW. We present algorithms
for probabilistic model-checking as well as game solving for DGRW conditions.
Our new algorithms lead to improvement both in terms of theoretical bounds as
well as practical evaluation. We compare PRISM with and without our new
translation, and show that the new translation leads to significant
improvements.
