Skip to main content
SpringerLink
Log in
Book cover

International Workshop on Reachability Problems

RP 2011: Reachability Problems pp 2–25Cite as

Observing Continuous-Time MDPs by 1-Clock Timed Automata

  • Conference paper

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 6945))

Abstract

This paper considers the verification of continuous-time Markov decision process (CTMDP s) against single-clock deterministic timed automata (DTA) specifications. The central issue is to compute the maximum probability of the set of timed paths of a CTMDP \(\mathcal{C}\) that are accepted by a DTA \(\mathcal{A}\). We show that this problem can be reduced to a linear programming problem whose coefficients are maximum timed reachability probabilities in a set of CTMDPs, which are obtained via a graph decomposition of the product of the CTMDP \(\mathcal{C}\) and the region graph of the DTA \(\mathcal{A}\).

This research is partially supported by the EU FP7 Project MoVeS and the ERC Advanced Grant VERIWARE.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   54.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   69.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Aceto, L., Bouyer, P., Burgueño, A., Larsen, K.G.: The power of reachability testing for timed automata. Theor. Comput. Sci. 300(1-3), 411–475 (2003)

    Article  MathSciNet  MATH  Google Scholar 

  2. Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183–235 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  3. Baier, C., Cloth, L., Haverkort, B.R., Kuntz, M., Siegle, M.: Model checking Markov chains with actions and state labels. IEEE Trans. Software Eng. 33(4), 209–224 (2007)

    Article  Google Scholar 

  4. Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.-P.: Model-checking algorithms for continuous-time Markov chains. IEEE Trans. Software Eng. 29(6), 524–541 (2003)

    Article  MATH  Google Scholar 

  5. Baier, C., Hermanns, H., Katoen, J.-P., Haverkort, B.: Efficient computation of time-bounded reachability probabilities in uniform continuous-time Markov decision processes. Theor. Comput. Sci. 345(1), 2–26 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  6. Baier, C., Kwiatkowska, M.: Model checking for a probabilistic branching time logic with fairness. Distrib. Comput. 11, 125–155 (1998)

    Article  Google Scholar 

  7. Barbot, B., Chen, T., Han, T., Katoen, J.-P., Mereacre, A.: Efficient CTMC model checking of linear real-time objectives. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 128–142. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  8. Bellman, R.: Dynamic Programming. Princeton University Press, Princeton (1957)

    MATH  Google Scholar 

  9. Bianco, A., de Alfaro, L.: Model checking of probabilistic and nondeterministic systems. In: Thiagarajan, P.S. (ed.) FSTTCS 1995. LNCS, vol. 1026, pp. 499–513. Springer, Heidelberg (1995)

    Chapter  Google Scholar 

  10. Brázdil, T., Forejt, V., Krcál, J., Kretínský, J., Kucera, A.: Continuous-time stochastic games with time-bounded reachability. In: FSTTCS, pp. 61–72 (2009)

    Google Scholar 

  11. Brázdil, T., Krcál, J., Kretínský, J., Kucera, A., Rehák, V.: Stochastic real-time games with qualitative timed automata objectives. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol. 6269, pp. 207–221. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  12. Brázdil, T., Krcál, J., Kretínský, J., Kucera, A., Rehák, V.: Measuring performance of continuous-time stochastic processes using timed automata. In: HSCC, pp. 33–42. ACM Press, New York (2011)

    Google Scholar 

  13. Buchholz, P., Schulz, I.: Numerical analysis of continuous time Markov decision processes over finite horizons. Computers & OR 38(3), 651–659 (2011)

    Article  MathSciNet  MATH  Google Scholar 

  14. Chatterjee, K., de Alfaro, L., Henzinger, T.A.: Trading memory for randomness. In: Quantitative Evaluation of Systems (QEST), pp. 206–217. IEEE Computer Society, Los Alamitos (2004)

    Google Scholar 

  15. Chen, T., Han, T., Katoen, J.-P., Mereacre, A.: Quantitative model checking of continuous-time Markov chains against timed automata specifications. In: LICS, pp. 309–318 (2009)

    Google Scholar 

  16. Chen, T., Han, T., Katoen, J.-P., Mereacre, A.: Model checking of continuous-time Markov chains against timed automata specifications. Logical Methods in Computer Science 7(1–2), 1–34 (2011)

    MathSciNet  MATH  Google Scholar 

  17. Chen, T., Han, T., Katoen, J.-P., Mereacre, A.: Reachability probabilities in Markovian timed automata. Technical report, RR-11-02, OUCL (2011)

    Google Scholar 

  18. Ciesinski, F., Baier, C.: Liquor: A tool for qualitative and quantitative linear time analysis of reactive systems. In: Quantitative Evaluation of Systems (QEST), pp. 131–132. IEEE Computer Society, Los Alamitos (2006)

    Google Scholar 

  19. Courcoubetis, C., Yannakakis, M.: The complexity of probabilistic verification. J. ACM 42(4), 857–907 (1995)

    Article  MathSciNet  MATH  Google Scholar 

  20. Davis, M.H.A.: Markov Models and Optimization. Chapman and Hall, Boca Raton (1993)

    Book  MATH  Google Scholar 

  21. de Alfaro, L.: How to specify and verify the long-run average behavior of probabilistic systems. In: LICS, pp. 454–465 (1998)

    Google Scholar 

  22. Donatelli, S., Haddad, S., Sproston, J.: Model checking timed and stochastic properties with CSL\(^{\footnotesize \mathrm{TA}}\). IEEE Trans. Software Eng. 35(2), 224–240 (2009)

    Article  Google Scholar 

  23. Guo, X., Hernández-Lerma, O., Prieto-Rumeau, T.: A survey of recent results on continuous-time Markov decision processes. TOP 14(2), 177–257 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  24. Howard, R.A.: Dynamic Programming and Markov Processes. MIT Press, Cambridge (1960)

    MATH  Google Scholar 

  25. Katoen, J.-P., Zapreev, I., Hahn, E.M., Hermanns, H., Jansen, D.N.: The ins and outs of the probabilistic model checker MRMC. Perf. Ev. 68(2), 90–104 (2011)

    Article  Google Scholar 

  26. Knast, R.: Continuous-time probabilistic automata. Information and Control 15(4), 335–352 (1969)

    Article  MathSciNet  MATH  Google Scholar 

  27. Laroussinie, F., Markey, N., Schnoebelen, P.: Model checking timed automata with one or two clocks. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol. 3170, pp. 387–401. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  28. Martin-Löfs, A.: Optimal control of a continuous-time Markov chain with periodic transition probabilities. Operations Research 15, 872–881 (1967)

    Article  MathSciNet  MATH  Google Scholar 

  29. Miller, B.L.: Finite state continuous time Markov decision processes with a finite planning horizon. SIAM Journal on Control 6(2), 266–280 (1968)

    Article  MathSciNet  MATH  Google Scholar 

  30. Neuhäußer, M.R., Stoelinga, M., Katoen, J.-P.: Delayed nondeterminism in continuous-time Markov decision processes. In: de Alfaro, L. (ed.) FOSSACS 2009. LNCS, vol. 5504, pp. 364–379. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  31. Neuhäußer, M.R., Zhang, L.: Time-bounded reachability probabilities in continuous-time Markov decision processes. In: Quantitative Evaluation of Systems (QEST), pp. 209–218. IEEE Computer Society, Los Alamitos (2010)

    Google Scholar 

  32. Puterman, M.L.: Markov Decision Processes. Wiley, Chichester (1994)

    Book  MATH  Google Scholar 

  33. Rabe, M., Schewe, S.: Finite optimal control for time-bounded reachability in CTMDPs and continuous-time Markov games. CoRR, abs/1004.4005 (2010)

    Google Scholar 

  34. Vardi, M.Y.: Automatic verification of probabilistic concurrent finite-state programs. In: FOCS, pp. 327–338. IEEE Computer Society, Los Alamitos (1985)

    Google Scholar 

  35. 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)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, University of Oxford, United Kingdom

    Taolue Chen, Tingting Han & Alexandru Mereacre

  2. Software Modeling and Verification Group, RWTH Aachen University, Germany

    Joost-Pieter Katoen

Authors
  1. Taolue Chen
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Tingting Han
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Joost-Pieter Katoen
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Alexandru Mereacre
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Dipartimento di Informatica e Scienze dell’Informazione, Università di Genova, via Dodecaneso 35, 16146, Genoa, Italy

    Giorgio Delzanno

  2. Department of Computer Science, University of Liverpool, Ashton St, Ashton Building, L69 3BX, Liverpool, UK

    Igor Potapov

Rights and permissions

Reprints and permissions

Copyright information

© 2011 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Chen, T., Han, T., Katoen, JP., Mereacre, A. (2011). Observing Continuous-Time MDPs by 1-Clock Timed Automata. In: Delzanno, G., Potapov, I. (eds) Reachability Problems. RP 2011. Lecture Notes in Computer Science, vol 6945. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-24288-5_2

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-24288-5_2

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-24287-8

  • Online ISBN: 978-3-642-24288-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation