Efficient probabilistic model checking of systems with ranged probabilities

We introduce a new technique to model check reachability properties on Interval Discrete-Time Markov Chains (IDTMC). We compute a sound over-approximation of the probabilities of satisfying a given property where the accuracy is characterized in terms of error bounds. We leverage affine arithmetic to propagate the first-order error terms. Higher-order error terms are bounded using interval arithmetic.