Efficient computation of time-bounded reachability probabilities in uniform continuous-time Markov decision processes

Christel Baier, Boudewijn Haverkort, Holger Hermanns, Joost-Pieter Katoen

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    7 Downloads (Pure)

    Abstract

    A continuous-time Markov decision process (CTMDP) is a generalization of a continuous-time Markov chain in which both probabilistic and nondeterministic choices co-exist. This paper presents an efficient algorithm to compute the maximum (or minimum) probability to reach a set of goal states within a given time bound in a uniform CTMDP, i.e., a CTMDP in which the delay time distribution per state visit is the same for all states. We prove that these probabilities coincide for (time-abstract) history-dependent and Markovian schedulers that resolve nondeterminism either deterministically or in a randomized way.
    Original languageEnglish
    Title of host publicationTools and Algorithms for the Construction and Analysis of Systems
    Subtitle of host publication10th International Conference, TACAS 2004, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2004, Barcelona, Spain, March 29 - April 2, 2004. Proceedings
    EditorsKurt Jensen, Andreas Podelski
    Place of PublicationBerlin, Heidelberg
    PublisherSpringer
    Pages61-76
    Number of pages16
    ISBN (Electronic)978-3-540-24730-2
    ISBN (Print)978-3-540-21299-7
    DOIs
    Publication statusPublished - 2004
    Event10th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2004 - Barcelona, Spain
    Duration: 29 Mar 20042 Apr 2004
    Conference number: 10

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer
    Volume2988
    ISSN (Print)0302-9743
    ISSN (Electronic)1611-3349

    Conference

    Conference10th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2004
    Abbreviated titleTACAS
    Country/TerritorySpain
    CityBarcelona
    Period29/03/042/04/04

    Keywords

    • FMT-PM: PROBABILISTIC METHODS
    • FMT-MC: MODEL CHECKING
    • FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS
    • Continuous-time Markov decision process (CTMDP)

    Fingerprint

    Dive into the research topics of 'Efficient computation of time-bounded reachability probabilities in uniform continuous-time Markov decision processes'. Together they form a unique fingerprint.

    Cite this