Probabilistic Bisimulations for PCTL Model Checking of Interval MDPs (extended version)
The result's identifiers
Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F14%3A00074493" target="_blank" >RIV/00216224:14330/14:00074493 - isvavai.cz</a>
Result on the web
<a href="http://arxiv.org/abs/1403.2864v3" target="_blank" >http://arxiv.org/abs/1403.2864v3</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.4204/EPTCS.145.4" target="_blank" >10.4204/EPTCS.145.4</a>
Alternative languages
Result language
angličtina
Original language name
Probabilistic Bisimulations for PCTL Model Checking of Interval MDPs (extended version)
Original language description
Verification of PCTL properties of MDPs with convex uncertainties has been investigated recently by Puggelli et al. However, model checking algorithms typically suffer from state space explosion. In this paper, we address probabilistic bisimulation to reduce the size of such an MDPs while preserving PCTL properties it satisfies. We discuss different interpretations of uncertainty in the models which are studied in the literature and that result in two different definitions of bisimulations. We give algorithms to compute the quotients of these bisimulations in time polynomial in the size of the model and exponential in the uncertain branching. Finally, we show by a case study that large models in practice can have small branching and that a substantialstate space reduction can be achieved by our approach.
Czech name
—
Czech description
—
Classification
Type
D - Article in proceedings
CEP classification
IN - Informatics
OECD FORD branch
—
Result continuities
Project
<a href="/en/project/GBP202%2F12%2FG061" target="_blank" >GBP202/12/G061: Center of excellence - Institute for theoretical computer science (CE-ITI)</a><br>
Continuities
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)
Others
Publication year
2014
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Article name in the collection
Proceedings 1st International Workshop on Synthesis of Continuous Parameters
ISBN
—
ISSN
2075-2180
e-ISSN
—
Number of pages
15
Pages from-to
19-33
Publisher name
Electronic Proceedings in Theoretical Computer Science
Place of publication
Grenoble, France
Event location
Grenoble, France
Event date
Jan 1, 2014
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
—