Robust Probabilistic Temporal Logics

TL;DR

This paper enhances probabilistic temporal logics PCTL and PCTL* to be more robust without increasing the computational complexity of model checking, improving their practical reliability.

Contribution

It introduces robustness to PCTL and PCTL* and proves that this does not add complexity to their model-checking procedures.

Findings

Robustness does not increase model-checking complexity.

Enhanced PCTL and PCTL* are more reliable for probabilistic system specifications.

Theoretical validation of robustness in probabilistic logics.

Abstract

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.