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

K Jensen (Editor), Christel Baier, Boudewijn R.H.M. Haverkort, A. Podelski (Editor), H. Hermanns, Joost P. Katoen

Research output: Contribution to conferencePaperAcademicpeer-review

5 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. This work is supported by the NWO-DFG bilateral project Validation of Stochastic Systems.
Original languageUndefined
Pages61-76
Number of pages16
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

Conference

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

Keywords

  • FMT-PM: PROBABILISTIC METHODS
  • FMT-MC: MODEL CHECKING
  • IR-63329
  • FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS
  • EWI-6539

Cite this

Jensen, K. (Ed.), Baier, C., Haverkort, B. R. H. M., Podelski, A. (Ed.), Hermanns, H., & Katoen, J. P. (2004). Efficient computation of time-bounded reachability probabilities in uniform continuous-time Markov decision processes. 61-76. Paper presented at 10th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2004, Barcelona, Spain. https://doi.org/10.1007/b96393, https://doi.org/10.1007/978-3-540-24730-2_5
Jensen, K (Editor) ; Baier, Christel ; Haverkort, Boudewijn R.H.M. ; Podelski, A. (Editor) ; Hermanns, H. ; Katoen, Joost P. / Efficient computation of time-bounded reachability probabilities in uniform continuous-time Markov decision processes. Paper presented at 10th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2004, Barcelona, Spain.16 p.
@conference{da5aa520acc14bc39534fea0178613e0,
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. This work is supported by the NWO-DFG bilateral project Validation of Stochastic Systems.",
keywords = "FMT-PM: PROBABILISTIC METHODS, FMT-MC: MODEL CHECKING, IR-63329, FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS, EWI-6539",
author = "K Jensen and Christel Baier and Haverkort, {Boudewijn R.H.M.} and A. Podelski and H. Hermanns and Katoen, {Joost P.}",
year = "2004",
doi = "10.1007/b96393",
language = "Undefined",
pages = "61--76",
note = "null ; Conference date: 29-03-2004 Through 02-04-2004",

}

Jensen, K (ed.), Baier, C, Haverkort, BRHM, Podelski, A (ed.), Hermanns, H & Katoen, JP 2004, 'Efficient computation of time-bounded reachability probabilities in uniform continuous-time Markov decision processes' Paper presented at 10th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2004, Barcelona, Spain, 29/03/04 - 2/04/04, pp. 61-76. https://doi.org/10.1007/b96393, https://doi.org/10.1007/978-3-540-24730-2_5

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

2004. 61-76 Paper presented at 10th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2004, Barcelona, Spain.

Research output: Contribution to conferencePaperAcademicpeer-review

TY - CONF

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.

A2 - Jensen, K

A2 - Podelski, A.

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. This work is supported by the NWO-DFG bilateral project Validation of Stochastic Systems.

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. This work is supported by the NWO-DFG bilateral project Validation of Stochastic Systems.

KW - FMT-PM: PROBABILISTIC METHODS

KW - FMT-MC: MODEL CHECKING

KW - IR-63329

KW - FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS

KW - EWI-6539

U2 - 10.1007/b96393

DO - 10.1007/b96393

M3 - Paper

SP - 61

EP - 76

ER -

Jensen K, (ed.), Baier C, Haverkort BRHM, Podelski A, (ed.), Hermanns H, Katoen JP. Efficient computation of time-bounded reachability probabilities in uniform continuous-time Markov decision processes. 2004. Paper presented at 10th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2004, Barcelona, Spain. https://doi.org/10.1007/b96393, https://doi.org/10.1007/978-3-540-24730-2_5