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

Logo poskytovatele

Varování

Publikace nespadá pod Ekonomicko-správní fakultu, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.
Autoři

HASHEMI Vahid HATEFI Hassan KRČÁL Jan

Rok publikování 2014
Druh Článek ve sborníku
Konference Proceedings 1st International Workshop on Synthesis of Continuous Parameters
Fakulta / Pracoviště MU

Fakulta informatiky

Citace
www http://arxiv.org/abs/1403.2864v3
Doi http://dx.doi.org/10.4204/EPTCS.145.4
Obor Informatika
Klíčová slova probabilistic bisimulation; interval MDP
Popis 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 substantial state space reduction can be achieved by our approach.
Související projekty:

Používáte starou verzi internetového prohlížeče. Doporučujeme aktualizovat Váš prohlížeč na nejnovější verzi.