Exploiting robust optimization for interval probabilistic bisimulation

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

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

2 Citations (Scopus)


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
Subtitle of host publication13th International Conference, QEST 2016, Quebec City, QC, Canada, August 23-25, 2016, Proceedings
EditorsBenny Van Houdt, Gul Agha
Place of PublicationCham
Number of pages17
ISBN (Electronic)978-3-319-43425-4
ISBN (Print)978-3-319-43424-7
Publication statusPublished - 2016
Externally publishedYes
Event13th International Conference on Quantitative Evaluation of Systems, QEST 2016 - Hôtel Château Laurier, Quebec City, Canada
Duration: 23 Aug 201625 Aug 2016
Conference number: 13

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference13th International Conference on Quantitative Evaluation of Systems, QEST 2016
Abbreviated titleQEST 2016
CityQuebec City


  • Linear programming problem
  • Robust optimization
  • Uncertain data
  • Robust counterpart
  • Computational tractability


Dive into the research topics of 'Exploiting robust optimization for interval probabilistic bisimulation'. Together they form a unique fingerprint.

Cite this