| Identifikační kód | RIV/00216224:14330/14:00074493 |
|---|
| Název v anglickém jazyce | Probabilistic Bisimulations for PCTL Model Checking of Interval MDPs (extended version) |
|---|
| Druh | D - Článek ve sborníku |
|---|
| Jazyk | eng - angličtina |
|---|
| Obor - skupina | I - Informatika |
|---|
| Obor | IN - Informatika |
|---|
| Rok uplatnění | 2014 |
|---|
| Kód důvěrnosti údajů | S - Úplné a pravdivé údaje o výsledku nepodléhající ochraně podle zvláštních právních předpisů. |
|---|
| Počet výskytů výsledku | 1 |
|---|
| Počet tvůrců celkem | 3 |
|---|
| Počet domácích tvůrců | 1 |
|---|
| Výčet všech uvedených jednotlivých tvůrců | Vahid Hashemi (státní příslušnost: IR - Íránská islámská republika)
Hassan Hatefi (státní příslušnost: IR - Íránská islámská republika)
Jan Krčál (státní příslušnost: CZ - Česká republika, domácí tvůrce: A, vedidk: 9668780) |
|---|
| Popis výsledku v anglickém jazyce | 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. |
|---|
| Klíčová slova oddělená středníkem | probabilistic bisimulation; interval MDP |
|---|
| Stránka www, na které se nachází výsledek | http://arxiv.org/abs/1403.2864v3 |
|---|
| DOI výsledku | 10.4204/EPTCS.145.4 |
|---|