@article{
 title = {Probabilistic Bisimulations for PCTL Model Checking of Interval MDPs (extended version)},
 type = {article},
 year = {2014},
 identifiers = {[object Object]},
 pages = {19-33},
 volume = {145},
 websites = {http://arxiv.org/pdf/1403.2864.pdf},
 month = {3},
 day = {31},
 id = {e5742389-9253-30b8-bf76-8eac5b1d3967},
 created = {2014-07-08T09:26:48.000Z},
 file_attached = {false},
 profile_id = {4f325e21-a764-32ab-9623-e568e98285be},
 last_modified = {2017-03-25T21:52:16.230Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {true},
 hidden = {false},
 source_type = {CONF},
 notes = {Owner: hhatefi<br/><br/><br/>Added to JabRef: 2014.07.08},
 private_publication = {false},
 abstract = {Verification of PCTL properties of MDPs with convex uncertainties has been investigated recently by<p>Puggelli et al. However, model checking algorithms typically suffer from state space explosion. In<p>this paper, we address probabilistic bisimulation to reduce the size of such an MDPs while preserving<p>PCTL properties it satisfies. We discuss different interpretations of uncertainty in the models which<p>are studied in the literature and that result in two different definitions of bisimulations. We give<p>algorithms to compute the quotients of these bisimulations in time polynomial in the size of the<p>model and exponential in the uncertain branching. Finally, we show by a case study that large models<p>in practice can have small branching and that a substantial state space reduction can be achieved by<p>our approach.},
 bibtype = {article},
 author = {Hashemi, Vahid and Hatefi, Hassan and Krcál, Jan},
 journal = {SynCoP  }
}

{"_id":{"_str":"53bbbace823e1b37040000cd"},"__v":0,"authorIDs":["5457d87e2abc8e9f370007e5","54d6986996f9453b5f00073b"],"author_short":["Hashemi, V.","Hatefi, H.","Krcál, J."],"bibbaseid":"hashemi-hatefi-krcl-probabilisticbisimulationsforpctlmodelcheckingofintervalmdpsextendedversion-2014","bibdata":{"title":"Probabilistic Bisimulations for PCTL Model Checking of Interval MDPs (extended version)","type":"article","year":"2014","identifiers":"[object Object]","pages":"19-33","volume":"145","websites":"http://arxiv.org/pdf/1403.2864.pdf","month":"3","day":"31","id":"e5742389-9253-30b8-bf76-8eac5b1d3967","created":"2014-07-08T09:26:48.000Z","file_attached":false,"profile_id":"4f325e21-a764-32ab-9623-e568e98285be","last_modified":"2017-03-25T21:52:16.230Z","read":false,"starred":false,"authored":"true","confirmed":"true","hidden":false,"source_type":"CONF","notes":"Owner: hhatefi<br/><br/><br/>Added to JabRef: 2014.07.08","private_publication":false,"abstract":"Verification of PCTL properties of MDPs with convex uncertainties has been investigated recently by<p>Puggelli et al. However, model checking algorithms typically suffer from state space explosion. In<p>this paper, we address probabilistic bisimulation to reduce the size of such an MDPs while preserving<p>PCTL properties it satisfies. We discuss different interpretations of uncertainty in the models which<p>are studied in the literature and that result in two different definitions of bisimulations. We give<p>algorithms to compute the quotients of these bisimulations in time polynomial in the size of the<p>model and exponential in the uncertain branching. Finally, we show by a case study that large models<p>in practice can have small branching and that a substantial state space reduction can be achieved by<p>our approach.","bibtype":"article","author":"Hashemi, Vahid and Hatefi, Hassan and Krcál, Jan","journal":"SynCoP ","bibtex":"@article{\n title = {Probabilistic Bisimulations for PCTL Model Checking of Interval MDPs (extended version)},\n type = {article},\n year = {2014},\n identifiers = {[object Object]},\n pages = {19-33},\n volume = {145},\n websites = {http://arxiv.org/pdf/1403.2864.pdf},\n month = {3},\n day = {31},\n id = {e5742389-9253-30b8-bf76-8eac5b1d3967},\n created = {2014-07-08T09:26:48.000Z},\n file_attached = {false},\n profile_id = {4f325e21-a764-32ab-9623-e568e98285be},\n last_modified = {2017-03-25T21:52:16.230Z},\n read = {false},\n starred = {false},\n authored = {true},\n confirmed = {true},\n hidden = {false},\n source_type = {CONF},\n notes = {Owner: hhatefi<br/><br/><br/>Added to JabRef: 2014.07.08},\n private_publication = {false},\n abstract = {Verification of PCTL properties of MDPs with convex uncertainties has been investigated recently by<p>Puggelli et al. However, model checking algorithms typically suffer from state space explosion. In<p>this paper, we address probabilistic bisimulation to reduce the size of such an MDPs while preserving<p>PCTL properties it satisfies. We discuss different interpretations of uncertainty in the models which<p>are studied in the literature and that result in two different definitions of bisimulations. We give<p>algorithms to compute the quotients of these bisimulations in time polynomial in the size of the<p>model and exponential in the uncertain branching. Finally, we show by a case study that large models<p>in practice can have small branching and that a substantial state space reduction can be achieved by<p>our approach.},\n bibtype = {article},\n author = {Hashemi, Vahid and Hatefi, Hassan and Krcál, Jan},\n journal = {SynCoP }\n}","author_short":["Hashemi, V.","Hatefi, H.","Krcál, J."],"urls":{"Website":"http://arxiv.org/pdf/1403.2864.pdf"},"bibbaseid":"hashemi-hatefi-krcl-probabilisticbisimulationsforpctlmodelcheckingofintervalmdpsextendedversion-2014","role":"author","downloads":1},"bibtype":"article","biburl":null,"creationDate":"2014-07-08T09:33:02.254Z","downloads":1,"keywords":[],"search_terms":["probabilistic","bisimulations","pctl","model","checking","interval","mdps","extended","version","hashemi","hatefi","krcál"],"title":"Probabilistic Bisimulations for PCTL Model Checking of Interval MDPs (extended version)","year":2014}