Model-checking omega-regular properties of interval Markov chains Conference Paper

Author(s): Chatterjee, Krishnendu; Henzinger, Thomas A; Sen, Koushik
Title: Model-checking omega-regular properties of interval Markov chains
Title Series: LNCS
Abstract: We study 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 riot 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. We call this semantic interpretation 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 introduce a logic omega-PCTL that can express liveness, strong fairness, and omega-regular properties (such properties cannot be expressed in PCTL). We show that the omega-PCTL model checking problem for Uncertain Markov Chain semantics is decidable in PSPACE (same as the best known upper bound for PCTL) and for Interval Markov Decision Process semantics is decidable in coNP (improving the previous known PSPACE bound for PCTL). We also show that the qualitative fragment of the logic can lie solved in coNP for the UMC interpretation, and can be solved in polynomial time for a sub-class of UMCs. We also prove lower bounds for these model checking problems. We show that the model checking problem of IDTMCs with LTL formulas can be solved for both UMC and IMDP semantics by reduction to the model checking problem of IDTMC with omega-PcTL formulas.
Conference Title: FoSSaCS: Foundations of Software Science and Computation Structures
Volume: 4962
Conference Dates: March 29 - April 6, 2008
Conference Location: Budapest, Hungary
Publisher: Springer  
Location: Berlin, Heidelberg
Date Published: 2008-03-01
Start Page: 302
End Page: 317
DOI: 10.1007/978-3-540-78499-9_22
Open access: no
IST Austria Authors
  1. Thomas A. Henzinger
    415 Henzinger
Related IST Austria Work