*banner
 

Model-Checking omega-Regular Properties of Interval Markov Chains
Krishnendu Chatterjee, Tom Henzinger, Koushik Sen

Citation
Krishnendu Chatterjee, Tom Henzinger, Koushik Sen. "Model-Checking omega-Regular Properties of Interval Markov Chains". Foundations of Software Science and Computation Structure (FoSSaCS) 2008, Roberto M. Amadio (ed.), 302-317, March, 2008.

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 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. 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 be 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.

Electronic downloads

Citation formats  
  • HTML
    Krishnendu Chatterjee, Tom Henzinger, Koushik Sen. <a
    href="http://chess.eecs.berkeley.edu/pubs/469.html"
    >Model-Checking omega-Regular Properties of Interval
    Markov Chains</a>, Foundations of Software Science and
    Computation Structure (FoSSaCS) 2008, Roberto M. Amadio
    (ed.), 302-317, March, 2008.
  • Plain text
    Krishnendu Chatterjee, Tom Henzinger, Koushik Sen.
    "Model-Checking omega-Regular Properties of Interval
    Markov Chains". Foundations of Software Science and
    Computation Structure (FoSSaCS) 2008, Roberto M. Amadio
    (ed.), 302-317, March, 2008.
  • BibTeX
    @inproceedings{ChatterjeeHenzingerSen08_ModelCheckingOmegaRegularPropertiesOfIntervalMarkov,
        author = {Krishnendu Chatterjee and Tom Henzinger and
                  Koushik Sen},
        title = {Model-Checking omega-Regular Properties of
                  Interval Markov Chains},
        booktitle = {Foundations of Software Science and Computation
                  Structure (FoSSaCS) 2008},
        editor = {Roberto M. Amadio},
        pages = {302-317},
        month = {March},
        year = {2008},
        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 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. 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 be 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.},
        URL = {http://chess.eecs.berkeley.edu/pubs/469.html}
    }
    

Posted by Krishnendu Chatterjee, PhD on 24 Jun 2008.
Groups: chess
For additional information, see the Publications FAQ or contact webmaster at chess eecs berkeley edu.

Notice: This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright.

©2002-2018 Chess