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

被引：76
|
作者：
Baier, C
Hermanns, H
Katoen, JP
Haverkort, BR
机构：
[1] Univ Bonn, D-53117 Bonn, Germany
[2] Univ Saarland, Dept Comp Sci, D-66123 Saarbrucken, Germany
[3] Univ Twente, NL-7500 AE Enschede, Netherlands
来源：
THEORETICAL COMPUTER SCIENCE | 2005年 / 345卷 / 01期
关键词：
continuous-time; Markov decision process; temporal logic; model checking; time-bounded reachability;
D O I：
10.1016/j.tcs.2005.07.022
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
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. It furthermore proves that these probabilities coincide for (time-abstract) history-dependent and Markovian schedulers that resolve nondeterminism either deterministically or in a randomized way. (c) 2005 Published by Elsevier B.V.
引用
收藏
页码：2 / 26
页数：25
相关论文
共 50 条
  • [1] Efficient computation of time-bounded reachability probabilities in uniform continuous-time Markov decision processes
    Baier, C
    Haverkort, B
    Hermanns, H
    Katoen, JP
    [J]. TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PROCEEDINGS, 2004, 2988 : 61 - 76
  • [2] Continuous-time stochastic games with time-bounded reachability
    Brazdil, Tomas
    Forejt, Vojtech
    Krcal, Jan
    Kretinsky, Jan
    Kucera, Antonin
    [J]. INFORMATION AND COMPUTATION, 2013, 224 : 46 - 70
  • [3] Policy Learning for Time-Bounded Reachability in Continuous-Time Markov Decision Processes via Doubly-Stochastic Gradient Ascent
    Bartocci, Ezio
    Bortolussi, Luca
    Brazdil, Tomas
    Milios, Dimitrios
    Sanguinetti, Guido
    [J]. QUANTITATIVE EVALUATION OF SYSTEMS, QEST 2016, 2016, 9826 : 244 - 259
  • [4] Finite optimal control for time-bounded reachability in CTMDPs and continuous-time Markov games
    Markus N. Rabe
    Sven Schewe
    [J]. Acta Informatica, 2011, 48
  • [5] Finite optimal control for time-bounded reachability in CTMDPs and continuous-time Markov games
    Rabe, Markus N.
    Schewe, Sven
    [J]. ACTA INFORMATICA, 2011, 48 (5-6) : 291 - 315
  • [6] Maximal Cost-Bounded Reachability Probability on Continuous-Time Markov Decision Processes
    Fu, Hongfei
    [J]. FOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATION STRUCTURES, 2014, 8412 : 73 - 87
  • [7] Time-Bounded Model Checking of Infinite-State Continuous-Time Markov Chains
    Hahn, E. Moritz
    Hermanns, Holger
    Wachter, Bjoern
    Zhang, Lijun
    [J]. FUNDAMENTA INFORMATICAE, 2009, 95 (01) : 129 - 155
  • [8] Time-Bounded Model Checking of Infinite-State Continuous-Time Markov Chains
    Zhang, Lijun
    Hermanns, Holger
    Hahn, E. Moritz
    Wachter, Bjoern
    [J]. 2008 8TH INTERNATIONAL CONFERENCE ON APPLICATION OF CONCURRENCY TO SYSTEM DESIGN, PROCEEDINGS, 2008, : 98 - 107
  • [9] Continuous-time Markov processes, orthogonal polynomials and Lancaster probabilities
    Mena, Ramses H.
    Palma, Freddy
    [J]. ESAIM-PROBABILITY AND STATISTICS, 2020, 24 : 100 - 112
  • [10] IMPULSIVE CONTROL FOR CONTINUOUS-TIME MARKOV DECISION PROCESSES
    Dufour, Francois
    Piunovskiy, Alexei B.
    [J]. ADVANCES IN APPLIED PROBABILITY, 2015, 47 (01) : 106 - 127
12345