Verification of PCTL properties of MDPs with convex uncertainties has been investigated recently by Puggelli et al. However, model checking algorithms typically suffer from the state space explosion problem. In this paper, we discuss the use of probabilistic bisimulation to reduce the size of such an MDP while preserving the PCTL properties it satisfies. As a core part, we show that deciding bisimilarity of a pair of states can be encoded as adjustable robust counterpart of an uncertain LP. We show that using affine decision rules, probabilistic bisimulation relation can be approximated in polynomial time. We have implemented our approach and demonstrate its effectiveness on several case studies.
CITATION STYLE
Hahn, E. M., Hashemi, V., Hermanns, H., & Turrini, A. (2016). Exploiting robust optimization for interval probabilistic bisimulation. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9826 LNCS, pp. 55–71). Springer Verlag. https://doi.org/10.1007/978-3-319-43425-4_4
Mendeley helps you to discover research relevant for your work.