University of Illinois Urbana-Champaign

Model-Checking Markov Chains in the presence of Uncertainties

Sen, Koushik; Viswanathan, Mahesh; Agha, Gul A.

Content Files
Model-Checking Markov Chains in the presence of Uncertainties.pdf

Permalink

https://hdl.handle.net/2142/11149

Description

Title
Model-Checking Markov Chains in the presence of Uncertainties
Author(s)
  • Sen, Koushik
  • Viswanathan, Mahesh
  • Agha, Gul A.
Issue Date
2006-01
Keyword(s)
computer science
Date of Ingest
2009-04-20T19:27:31Z
Abstract
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.
Type of Resource
text
Genre of Resource
Technical Report
Permalink
http://hdl.handle.net/2142/11149
Copyright and License Information
You are granted permission for the non-commercial reproduction, distribution, display, and performance of this technical report in any format, BUT this permission is only for a period of 45 (forty-five) days from the most recent time that you verified that this technical report is still available from the University of Illinois at Urbana-Champaign Computer Science Department under terms that include this permission. All other rights are reserved by the author(s).

Owning Collections

Research and Tech Reports - Computer Science PRIMARY