Consistency and refinement for Interval Markov Chains

Interval Markov Chains (IMC), or Markov Chains with probability intervals in the transition matrix, are the base of a classic specification theory for probabilistic systems [18]. The standard semantics of IMCs assigns to a specification the set of all Markov Chains that satisfy its interval constraints. The theory then provides operators for deciding emptiness of conjunction and refinement (entailment) for such specifications.In this paper, we study complexity of several problems for IMCs, that stem from compositional modeling methodologies. In particular, we close the complexity gap for thorough refinement of two IMCs and for deciding the existence of a common implementation for an unbounded number of IMCs, showing that these problems are EXPTIME-complete.We discuss suitable notions of determinism for specifications, and show that for deterministic IMCs the syntactic refinement operators are complete with respect to model inclusion. Finally, we show that deciding consistency (emptiness) for an IMC is polynomial and that existence of common implementation can be established in polynomial time for any constant number of IMCs.