Probabilistic Bisimulations for PCTL Model Checking of Interval MDPs

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

Full description

Bibliographic Details
Main Authors: Vahid Hashemi, Hassan Hatefi, Jan Krčál
Format: Article
Language:English
Published: Open Publishing Association 2014-03-01
Series:Electronic Proceedings in Theoretical Computer Science
Online Access:http://arxiv.org/pdf/1403.2864v3