Exploiting Robust Optimization for Interval Probabilistic Bisimulation

Ernst Moritz Hahn, Vahid Hashemi, Holger Hermanns, Andrea Turrini

Research output: Chapter in Book/Report/Conference proceedingConference contribution

2 Citations (Scopus)

Abstract

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.
Original languageEnglish
Title of host publicationQuantitative Evaluation of Systems - 13th International Conference, QEST 2016, Quebec City, QC, Canada, August 23-25, 2016, Proceedings
Pages55-71
Number of pages17
DOIs
Publication statusPublished - 2016
Externally publishedYes

Fingerprint Dive into the research topics of 'Exploiting Robust Optimization for Interval Probabilistic Bisimulation'. Together they form a unique fingerprint.

Cite this