On the complexity of model checking interval-valued discrete time Markov chains

On the complexity of model checking interval-valued discrete time Markov chains

0.00 Avg rating0 Votes
Article ID: iaor20131661
Volume: 113
Issue: 7
Start Page Number: 210
End Page Number: 216
Publication Date: Apr 2013
Journal: Information Processing Letters
Authors: , ,
Keywords: markov processes, programming: markov decision
Abstract:

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 Square‐Root‐Sum hard, meaning that one can reduce the Square‐Root‐Sum problem to it.

Reviews

Required fields are marked *. Your email address will not be published.