Robust probabilistic temporal logics

We robustify PCTL and PCTL ⁎ , the most important specification languages for probabilistic systems, and show that robustness does not increase the complexity of their model-checking problems. • The first robust probabilistic temporal logic for the verification of reactive systems. • Robustness comes for free: model-checking is not harder with robustness than without. • The same intuitive syntax than classical probabilistic logics.