Reachability in continuous-time Markov reward decision processes

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

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

    124 Downloads (Pure)


    Continuous-time Markov decision processes (CTMDPs) are widely used for the control of queueing systems, epidemic and manufacturing processes. Various results on optimal schedulers for discounted and average reward optimality criteria in CTMDPs are known, but the typical game-theoretic winning objectives have received scant attention so far. This paper studies various sorts of reachability objectives for CTMDPs. Memoryless schedulers are optimal for simple reachability objectives as it suffices to consider the embedded MDP. Schedulers that may count the number of visits to states are optimal---when restricting to time-abstract schedulers---for timed reachability in uniform CTMDPs. The central result is that for any CTMDP, reward reachability objectives are dual to timed ones. As a corollary, epsilon-optimal schedulers for reward reachability objectives in uniform CTMDPs can be obtained in polynomial time using a simple backward greedy algorithm.
    Original languageEnglish
    Title of host publicationLogic and Automata
    Subtitle of host publicationHistory and Perspectives
    EditorsJörg Flum, Erich Grädel, Thomas Wilke
    Place of PublicationAmsterdam
    PublisherAmsterdam University Press
    Number of pages19
    ISBN (Print)978-90-5356-576-6
    Publication statusPublished - Feb 2008
    EventLogic and Automata: History and Perspectives - Aachen, Germany
    Duration: 14 Dec 200715 Dec 2007

    Publication series

    NameTexts in Logic and Games
    PublisherAmsterdam University Press


    WorkshopLogic and Automata: History and Perspectives
    Other14-15 Dec 2007


    • Continuous-time Markov decision process (CTMDP)


    Dive into the research topics of 'Reachability in continuous-time Markov reward decision processes'. Together they form a unique fingerprint.

    Cite this