Quantitative Analysis of Interval Markov Chains

Interval Markov chains (IMCs), as first introduced by Larsen and Jonsson in 1991 are succinct specifications for probabilistic systems that generalise Markov chains (MCs) by allowing state transition probabilities to lie within an interval. In this work, we address the study of IMCs in a quantitative setting by extending the notion of IMCs by associating with each state a reward that is gained when leaving the state. Specifically, we compare three different semantic interpretations proposed in the literature (once-and-for-all, interval Markov decision process and at-every-step) in the context of model-checking rPCTL, an extension of PCTL where each path-formula is equipped with the specification of a bound on the accumulated reward. We prove that for the full logic, the three semantics are not equivalent, but for the fragment of reward-bounded reachability properties, the interval Markov decision process semantics and the at-every-step semantics are equivalent. Finally, we discuss model-checking algorithms for the three semantics by reduction to the model-checking problem for parametric Markov chains.