## Model Checking Omega-regular Properties of Interval Markov Chains

*Krishnendu Chatterjee, Koushik Sen, and
Thomas A. Henzinger*

We study the problem of model checking Interval-valued Discrete-Time
Markov Chains (IDTMCs). 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 the 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 the
IDTMC, which we call *Interval Markov Decision Process* (IMDP),
we view the uncertainty as being resolved through nondeterminism. In
other words, each time a state is visited, an adversary chooses a
transition distribution that respects the interval constraints, and we
take a probabilistic step according to the chosen distribution.

We introduce the logic *omega-PCTL*, which can express
omega-regular properties including weak and strong fairness (such
properties cannot be expressed in PCTL). We show that the omega-PCTL
model-checking problem for UMC semantics is decidable in PSPACE (this
is the same as the best known upper bound for PCTL), and for IMDP
semantics, it is decidable in coNP (this improves the best previously
known PSPACE bound for PCTL). We also show that the qualitative
fragment of the logic can be solved in coNP for the UMC
interpretation, and can be solved in polynomial time for a subclass of
IDTMCs with UMC semantics. We also prove lower bounds for these
model-checking problems. Finally, we show that the LTL model-checking
problem over IDTMCs can be solved for both UMC and IMDP semantics
by reduction to the omega-PCTL model-checking problem.

*Proceedings of the
11th International Conference on Foundations of Software Science and
Computational Structures*
(FOSSACS),
Lecture Notes in Computer Science 4962,
Springer,
2008,
pp. 302-317.

Download inofficial, sometimes updated
PostScript /
PDF document.
© 2008 Springer.