Probabilistic Bisimulations for PCTL Model Checking of Interval MDPs (extended version)

Kód výsledku v 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>

Výsledek na webu

<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>

Jazyk výsledku

angličtina

Název v původním jazyce

Probabilistic Bisimulations for PCTL Model Checking of Interval MDPs (extended version)

Popis výsledku v původní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.

Název v anglickém jazyce

Probabilistic Bisimulations for PCTL Model Checking of Interval MDPs (extended version)

Popis výsledku anglicky

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.

Druh

D - Stať ve sborníku

CEP obor

IN - Informatika

OECD FORD obor

—

Projekt

<a href="/cs/project/GBP202%2F12%2FG061" target="_blank" >GBP202/12/G061: Centrum excelence - Institut teoretické informatiky (CE-ITI)</a><br>

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Rok uplatnění

2014

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název statě ve sborníku

Proceedings 1st International Workshop on Synthesis of Continuous Parameters

ISBN

—

ISSN

2075-2180

e-ISSN

—

Počet stran výsledku

15

Strana od-do

19-33

Název nakladatele

Electronic Proceedings in Theoretical Computer Science

Místo vydání

Grenoble, France

Místo konání akce

Grenoble, France

Datum konání akce

1. 1. 2014

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

—