Model-checking markov chains in the presence of uncertainties
By
We investigate the problem of model checking Interval-valued Discrete-time Markov Chains (IDTMC). IDTMCs are discrete-time finite Markov Chains for which the exact transition probabilities are not known. Instead in IDTMCs, each transition is associated with an interval in which the actual transition probability must lie. We consider two semantic interpretations for the uncertainty in the transition probabilities of an IDTMC. In the first interpretation, we think of an IDTMC as representing a (possibly uncountable) family of (classical) discrete-time Markov Chains, where each member of the family is a Markov Chain whose transition probabilities lie within the interval range given in the IDTMC. This semantic interpretation we call Uncertain Markov Chains (UMC). In the second semantics for an IDTMC, which we call Interval Markov Decision Process (IMDP), we view the uncertainty as being resolved through non-determinism. In other words, each time a state is visited, we adversarially pick a transition distribution that respects the interval constraints, and take a probabilistic step according to the chosen distribution. We show that the PCTL model checking problem for both Uncertain Markov Chain semantics and Interval Markov Decision Process semantics is decidable in PSPACE. We also prove lower bounds for these model checking problems.
BibTeX
@inproceedings{conf/tacas/SenVA06,
author = "Sen, Koushik and Viswanathan, Mahesh and Agha, Gul",
editor = "Hermanns, Holger and Palsberg, Jens",
title = "Model-Checking Markov Chains in the Presence of
Uncertainties",
booktitle = "TACAS",
crossref = "conf/tacas/2006",
ee = "http://dx.doi.org/10.1007/11691372_26",
keywords = "formal methods",
pages = "394-410",
year = "2006",
}
@proceedings{conf/tacas/2006,
editor = "Hermanns, Holger and Palsberg, Jens",
title = "Tools and Algorithms for the Construction and Analysis of
Systems, 12th International Conference, TACAS 2006 Held as Part of
the Joint European Conferences on Theory and Practice of Software,
ETAPS 2006, Vienna, Austria, March 25 - April 2, 2006,
Proceedings",
isbn = "3-540-33056-9",
publisher = "Springer",
series = "Lecture Notes in Computer Science",
volume = "3920",
year = "2006",
}