TY - GEN
T1 - Model-checking Markov chains in the presence of uncertainties
AU - Sen, Koushik
AU - Viswanathan, Mahesh
AU - Agha, Gul
PY - 2006
Y1 - 2006
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=33745801332&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=33745801332&partnerID=8YFLogxK
U2 - 10.1007/11691372_26
DO - 10.1007/11691372_26
M3 - Conference contribution
AN - SCOPUS:33745801332
SN - 3540330569
SN - 9783540330561
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 394
EP - 410
BT - Tools and Algorithms for the Construction and Analysis of Systems - 12th International Conference, TACAS 2006. Held as Part of the Joint European Conf. on Theory and Practice of Software, ETAPS 2006
T2 - 12th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2006. Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2006
Y2 - 25 March 2006 through 2 April 2006
ER -