Article ID: | iaor20131661 |
Volume: | 113 |
Issue: | 7 |
Start Page Number: | 210 |
End Page Number: | 216 |
Publication Date: | Apr 2013 |
Journal: | Information Processing Letters |
Authors: | Chen Taolue, Han Tingting, Kwiatkowska Marta |
Keywords: | markov processes, programming: markov decision |
We investigate the complexity of model checking (finite) interval‐valued discrete time Markov chains, that is, discrete time Markov chains where each transition is associated with an interval in which the actual transition probability must lie. Two semantics are considered, the uncertain Markov chain (UMC) semantics and the interval Markov decision process (IMDP) semantics. We show that, for reachability, these two semantics coincide and the problem is P‐complete. This entails that PCTL model checking problem under the IMDP semantics is also P‐complete. We also show that model checking PCTL under the UMC semantics is