Advertisement

Delayed Nondeterminism in Continuous-Time Markov Decision Processes

  • Martin R. Neuhäußer
  • Mariëlle Stoelinga
  • Joost-Pieter Katoen
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5504)

Abstract

Schedulers in randomly timed games can be classified as to whether they use timing information or not. We consider continuous-time Markov decision processes (CTMDPs) and define a hierarchy of positional (P) and history-dependent (H) schedulers which induce strictly tighter bounds on quantitative properties on CTMDPs. This classification into time abstract (TA), total time (TT) and fully time-dependent (T) schedulers is mainly based on the kind of timing details that the schedulers may exploit. We investigate when the resolution of nondeterminism may be deferred. In particular, we show that TTP and TAP schedulers allow for delaying nondeterminism for all measures, whereas this does neither hold for TP nor for any TAH scheduler. The core of our study is a transformation on CTMDPs which unifies the speed of outgoing transitions per state.

Keywords

Sojourn Time Markov Decision Process Exit Rate Time Positional Probability Bound 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

References

  1. 1.
    Knast, R.: Continuous-time probabilistic automata. Inform. and Control 15, 335–352 (1969)MathSciNetCrossRefzbMATHGoogle Scholar
  2. 2.
    Guo, X., Hernández-Lerma, O., Prieto-Rumeau, T.: A survey of recent results on continuous-time Markov decision processes. TOP 14, 177–261 (2006)MathSciNetCrossRefzbMATHGoogle Scholar
  3. 3.
    Baier, C., Hermanns, H., Katoen, J.P., Haverkort, B.R.: Efficient computation of time-bounded reachability probabilities in uniform continuous-time Markov decision processes. Theor. Comp. Sci. 345(1), 2–26 (2005)MathSciNetCrossRefzbMATHGoogle Scholar
  4. 4.
    Puterman, M.L.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. John Wiley and Sons, Chichester (1994)CrossRefzbMATHGoogle Scholar
  5. 5.
    Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.P.: Model-checking algorithms for continuous-time Markov chains. IEEE TSE 29(6), 524–541 (2003)zbMATHGoogle Scholar
  6. 6.
    Wolovick, N., Johr, S.: A characterization of meaningful schedulers for continuous-time Markov decision processes. In: Asarin, E., Bouyer, P. (eds.) FORMATS 2006. LNCS, vol. 4202, pp. 352–367. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  7. 7.
    Grassmann, W.K.: Finding transient solutions in Markovian event systems through randomization. In: Stewart, W.J. (ed.) Numerical Solutions of Markov Chains, pp. 357–371 (1991)Google Scholar
  8. 8.
    Gross, D., Miller, D.R.: The randomization technique as a modeling tool and solution procedure for transient Markov processes. Oper. Res. 32(2), 343–361 (1984)MathSciNetCrossRefzbMATHGoogle Scholar
  9. 9.
    Jensen, A.: Markov chains as an aid in the study of Markov processes. Skand. Aktuarietidskrift 3, 87–91 (1953)zbMATHGoogle Scholar
  10. 10.
    Ash, R., Doléans-Dade, C.: Probability & Measure Theory, 2nd edn. Academic Press, London (2000)zbMATHGoogle Scholar
  11. 11.
    Neuhäußer, M.R., Katoen, J.P.: Bisimulation and logical preservation for continuous-time Markov decision processes. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol. 4703, pp. 412–427. Springer, Heidelberg (2007)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2009

Authors and Affiliations

  • Martin R. Neuhäußer
    • 1
    • 2
  • Mariëlle Stoelinga
    • 2
  • Joost-Pieter Katoen
    • 1
    • 2
  1. 1.MOVES GroupRWTH Aachen UniversityGermany
  2. 2.FMT GroupUniversity of TwenteThe Netherlands

Personalised recommendations