Polynomial-time alternating probabilistic bisimulation for interval MDPs

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

*Corresponding author for this work

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

1 Citation (Scopus)

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 languageEnglish
Title of host publicationDependable Software Engineering. Theories, Tools, and Applications
Subtitle of host publicationThird International Symposium, SETTA 2017, Changsha, China, October 23-25, 2017, Proceedings
EditorsJi Wang, Kim Guldstrand Larsen, Oleg Sokolsky
Place of PublicationCham
PublisherSpringer
Pages25-41
Number of pages17
ISBN (Electronic)978-3-319-69483-2
ISBN (Print)978-3-319-69482-5
DOIs
Publication statusPublished - 2017
Externally publishedYes
Event3rd International Symposium on Dependable Software Engineering: Theories, Tools and Applications, SETTA 2017 - Changsha, China
Duration: 23 Oct 201725 Oct 2017
Conference number: 3
http://lcs.ios.ac.cn/setta2017/

Publication series

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

Conference

Conference3rd International Symposium on Dependable Software Engineering: Theories, Tools and Applications, SETTA 2017
Abbreviated titleSETTA
CountryChina
CityChangsha
Period23/10/1725/10/17
Internet address

Fingerprint

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

Cite this