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

Christel Baier, Boudewijn R.H.M. Haverkort, H. Hermanns, Joost P. Katoen

    Research output: Book/ReportReportProfessional

    7 Citations (Scopus)
    47 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 languageUndefined
    Place of PublicationEnschede
    PublisherElektrotechniek, Wiskunde & Informatica
    Number of pages30
    Publication statusPublished - 2004

    Publication series

    Name1381-3625
    PublisherUniversity of Twente, Centre for Telematics and Information Technology (CTIT)
    No.03-50

    Keywords

    • METIS-221438
    • IR-49256

    Cite this

    Baier, C., Haverkort, B. R. H. M., Hermanns, H., & Katoen, J. P. (2004). Efficient computation of time-bounded reachability probabilities in uniform continuous-time Markov decision processes. (1381-3625; No. 03-50). Enschede: Elektrotechniek, Wiskunde & Informatica.
    Baier, Christel ; Haverkort, Boudewijn R.H.M. ; Hermanns, H. ; Katoen, Joost P. / Efficient computation of time-bounded reachability probabilities in uniform continuous-time Markov decision processes. Enschede : Elektrotechniek, Wiskunde & Informatica, 2004. 30 p. (1381-3625; 03-50).
    @book{9506ac857e7943e4b62a533f74e7b000,
    title = "Efficient computation of time-bounded reachability probabilities in uniform continuous-time Markov decision processes",
    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.",
    keywords = "METIS-221438, IR-49256",
    author = "Christel Baier and Haverkort, {Boudewijn R.H.M.} and H. Hermanns and Katoen, {Joost P.}",
    year = "2004",
    language = "Undefined",
    series = "1381-3625",
    publisher = "Elektrotechniek, Wiskunde & Informatica",
    number = "03-50",

    }

    Baier, C, Haverkort, BRHM, Hermanns, H & Katoen, JP 2004, Efficient computation of time-bounded reachability probabilities in uniform continuous-time Markov decision processes. 1381-3625, no. 03-50, Elektrotechniek, Wiskunde & Informatica, Enschede.

    Efficient computation of time-bounded reachability probabilities in uniform continuous-time Markov decision processes. / Baier, Christel; Haverkort, Boudewijn R.H.M.; Hermanns, H.; Katoen, Joost P.

    Enschede : Elektrotechniek, Wiskunde & Informatica, 2004. 30 p. (1381-3625; No. 03-50).

    Research output: Book/ReportReportProfessional

    TY - BOOK

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

    AU - Baier, Christel

    AU - Haverkort, Boudewijn R.H.M.

    AU - Hermanns, H.

    AU - Katoen, Joost P.

    PY - 2004

    Y1 - 2004

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

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

    KW - METIS-221438

    KW - IR-49256

    M3 - Report

    T3 - 1381-3625

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

    PB - Elektrotechniek, Wiskunde & Informatica

    CY - Enschede

    ER -

    Baier C, Haverkort BRHM, Hermanns H, Katoen JP. Efficient computation of time-bounded reachability probabilities in uniform continuous-time Markov decision processes. Enschede: Elektrotechniek, Wiskunde & Informatica, 2004. 30 p. (1381-3625; 03-50).