Polynomial-time alternating probabilistic bisimulation for interval MDPs

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

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

2 Scopus citations

Abstract

Interval Markov decision processes (IMDPs) extend classical MDPs by allowing intervals to be used as transition probabilities. They provide a powerful modelling tool for probabilistic systems with an additional variation or uncertainty that relaxes the need of knowing the exact transition probabilities, which are usually difficult to get from real systems. In this paper, we discuss a notion of alternating probabilistic bisimulation to reduce the size of the IMDPs while preserving the probabilistic CTL properties it satisfies from both computational complexity and compositional reasoning perspectives. Our alternating probabilistic bisimulation stands on the competitive way of resolving the IMDP nondeterminism which in turn finds applications in the settings of the controller (parameter) synthesis for uncertain (parallel) probabilistic systems. By using the theory of linear programming, we improve the complexity of computing the bisimulation from the previously known EXPTIME to PTIME. Moreover, we show that the bisimulation for IMDPs is a congruence with respect to two facets of parallelism, namely synchronous product and interleaving. We finally demonstrate the practical effectiveness of our proposed approaches by applying them on several case studies using a prototypical tool.

Original languageBritish English
Title of host publicationDependable Software Engineering
Subtitle of host publicationTheories, Tools, and Applications - 3rd International Symposium, SETTA 2017, Proceedings
EditorsJi Wang, Kim Guldstrand Larsen, Oleg Sokolsky
PublisherSpringer Verlag
Pages25-41
Number of pages17
ISBN (Print)9783319694825
DOIs
StatePublished - 2017
Event3rd International Symposium on Dependable Software Engineering: Theories, Tools and Applications, SETTA 2017 - Changsha, China
Duration: 23 Oct 201725 Oct 2017

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume10606 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference3rd International Symposium on Dependable Software Engineering: Theories, Tools and Applications, SETTA 2017
Country/TerritoryChina
CityChangsha
Period23/10/1725/10/17

Fingerprint

Dive into the research topics of 'Polynomial-time alternating probabilistic bisimulation for interval MDPs'. Together they form a unique fingerprint.

Cite this