---
OA_type: closed access
_id: '3875'
abstract:
- lang: eng
  text: 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.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
- first_name: Koushik
  full_name: Sen, Koushik
  last_name: Sen
citation:
  ama: 'Chatterjee K, Henzinger TA, Sen K. Model-checking omega-regular properties
    of interval Markov chains. In: <i>Foundations of Software Science and Computational
    Structures - 11th International Conference</i>. Vol 4962. Springer Nature; 2008:302-317.
    doi:<a href="https://doi.org/10.1007/978-3-540-78499-9_22">10.1007/978-3-540-78499-9_22</a>'
  apa: 'Chatterjee, K., Henzinger, T. A., &#38; Sen, K. (2008). Model-checking omega-regular
    properties of interval Markov chains. In <i>Foundations of Software Science and
    Computational Structures - 11th International Conference</i> (Vol. 4962, pp. 302–317).
    Budapest, Hungary: Springer Nature. <a href="https://doi.org/10.1007/978-3-540-78499-9_22">https://doi.org/10.1007/978-3-540-78499-9_22</a>'
  chicago: Chatterjee, Krishnendu, Thomas A Henzinger, and Koushik Sen. “Model-Checking
    Omega-Regular Properties of Interval Markov Chains.” In <i>Foundations of Software
    Science and Computational Structures - 11th International Conference</i>, 4962:302–17.
    Springer Nature, 2008. <a href="https://doi.org/10.1007/978-3-540-78499-9_22">https://doi.org/10.1007/978-3-540-78499-9_22</a>.
  ieee: K. Chatterjee, T. A. Henzinger, and K. Sen, “Model-checking omega-regular
    properties of interval Markov chains,” in <i>Foundations of Software Science and
    Computational Structures - 11th International Conference</i>, Budapest, Hungary,
    2008, vol. 4962, pp. 302–317.
  ista: 'Chatterjee K, Henzinger TA, Sen K. 2008. Model-checking omega-regular properties
    of interval Markov chains. Foundations of Software Science and Computational Structures
    - 11th International Conference. FoSSaCS: Foundations of Software Science and
    Computation Structures, LNCS, vol. 4962, 302–317.'
  mla: Chatterjee, Krishnendu, et al. “Model-Checking Omega-Regular Properties of
    Interval Markov Chains.” <i>Foundations of Software Science and Computational
    Structures - 11th International Conference</i>, vol. 4962, Springer Nature, 2008,
    pp. 302–17, doi:<a href="https://doi.org/10.1007/978-3-540-78499-9_22">10.1007/978-3-540-78499-9_22</a>.
  short: K. Chatterjee, T.A. Henzinger, K. Sen, in:, Foundations of Software Science
    and Computational Structures - 11th International Conference, Springer Nature,
    2008, pp. 302–317.
conference:
  end_date: 2008-04-06
  location: Budapest, Hungary
  name: 'FoSSaCS: Foundations of Software Science and Computation Structures'
  start_date: 2008-03-29
date_created: 2018-12-11T12:05:39Z
date_published: 2008-03-01T00:00:00Z
date_updated: 2026-05-29T10:35:10Z
day: '01'
doi: 10.1007/978-3-540-78499-9_22
extern: '1'
fulldoi: https://doi.org/10.1007/978-3-540-78499-9_22
intvolume: '      4962'
language:
- iso: eng
month: '03'
oa_version: None
page: 302 - 317
publication: Foundations of Software Science and Computational Structures - 11th International
  Conference
publication_identifier:
  eissn:
  - 1611-3349
  issn:
  - 0302-9743
publication_status: published
publisher: Springer Nature
publist_id: '2298'
status: public
title: Model-checking omega-regular properties of interval Markov chains
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 4962
year: '2008'
...