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 contribution


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 languageEnglish
Title of host publicationDependable Software Engineering. Theories, Tools, and Applications
Subtitle of host publicationDependable Software Engineering. Theories, Tools, and Applications - Third International Symposium, SETTA 2017, Changsha, China, October 23-25, 2017, Proceedings
Number of pages17
Publication statusPublished - 01 Nov 2017
Externally publishedYes

Fingerprint Dive into the research topics of 'Polynomial-Time Alternating Probabilistic Bisimulation for Interval MDPs'. Together they form a unique fingerprint.

Cite this