Text this: Reducción de orden parcial en model checking probabilista simbólico