Skip to main content
SpringerLink
Log in

Playing Optimally on Timed Automata with Random Delays

  • Conference paper
Formal Modeling and Analysis of Timed Systems (FORMATS 2012)

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

Abstract

We marry continuous time Markov decision processes (CTMDPs) with stochastic timed automata into a model with joint expressive power. This extension is very natural, as the two original models already share exponentially distributed sojourn times in locations. It enriches CTMDPs with timing constraints, or symmetrically, stochastic timed automata with one conscious player. Our model maintains the existence of optimal control known for CTMDPs. This also holds for a richer model with two players, which extends continuous time Markov games. But we have to sacrifice the existence of simple schedulers: polyhedral regions are insufficient to obtain optimal control even in the single-player case.

This work was supported by the Engineering and Physical Science Research Council grant EP/H046623/1 ‘Synthesis and Verification in Markov Game Structures’ and a Leverhulme Trust Visiting Fellowship.

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

Access this chapter

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 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 49.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

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Alur, R., Dill, D.L.: A Theory of Timed Automata. Theoretical Computer Science 126(2), 183–235 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  2. Asarin, E., Maler, O., Pnueli, A., Sifakis, J.: Controller Synthesis for Timed Automata. In: Proc. of SCC 1998, pp. 469–474. Elsevier (1998)

    Google Scholar 

  3. Baier, C., Bertrand, N., Bouyer, P., Brihaye, T., Größer, M.: Probabilistic and Topological Semantics for Timed Automata. In: Arvind, V., Prasad, S. (eds.) FSTTCS 2007. LNCS, vol. 4855, pp. 179–191. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  4. Baier, C., Bertrand, N., Bouyer, P., Brihaye, Th., Größer, M.: Almost-Sure Model Checking of Infinite Paths in One-Clock Timed Automata. In: Proc. of LICS 2008, pp. 217–226. IEEE (2008)

    Google Scholar 

  5. Baier, C., Hermanns, H., Katoen, J.-P., Haverkort, B.R.: Efficient Computation of Time-Bounded Reachability Probabilities in Uniform Continuous-Time Markov Decision Processes. Theoretical Computer Science 345(1), 2–26 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  6. Bouyer, P., Brihaye, Th., Jurdziński, M., Menet, Q.: Almost-Sure Model-Checking of Reactive Timed Automata. In: Proc. of QEST 2012. IEEE (to appear, 2012)

    Google Scholar 

  7. Bouyer, P., Forejt, V.: Reachability in Stochastic Timed Games. In: Albers, S., Marchetti-Spaccamela, A., Matias, Y., Nikoletseas, S., Thomas, W. (eds.) ICALP 2009, Part II. LNCS, vol. 5556, pp. 103–114. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  8. Brázdil, T., Forejt, V., Krcál, J., Kretínský, J., Kucera, A.: Continuous-Time Stochastic Games with Time-Bounded Reachability. In: Proc. of FSTTCS 2009. LIPIcs, vol. 4, pp. 61–72. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2009)

    Google Scholar 

  9. Brázdil, T., Krčál, J., Křetínský, J., Kučera, A., Řehá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 

  10. 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:12), 1–34 (2011)

    MathSciNet  Google Scholar 

  11. Chen, T., Han, T., Katoen, J.-P., Mereacre, A.: Observing Continuous-Time MDPs by 1-Clock Timed Automata. In: Delzanno, G., Potapov, I. (eds.) RP 2011. LNCS, vol. 6945, pp. 2–25. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  12. Chen, T., Han, T., Katoen, J.-P., Mereacre, A.: Reachability Probabilities in Markovian Timed Automata. In: Proc. of CDC-ECC 2011, pp. 7075–7080. IEEE (2011)

    Google Scholar 

  13. Fearnley, J., Rabe, M.N., Schewe, S., Zhang, L.: Efficient Approximation of Optimal Control for Continuous-Time Markov Games. In: Proc. of FSTTCS 2011. LIPIcs, vol. 13, pp. 399–410. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2011)

    Google Scholar 

  14. Kwiatkowska, M.Z., Norman, G., Segala, R., Sproston, J.: Automatic Verification of Real-Time Systems with Discrete Probability Distributions. Theoretical Computer Science 282(1), 101–150 (2002)

    Article  MathSciNet  MATH  Google Scholar 

  15. Neuhäußer, M.R., Zhang, L.: Time-Bounded Reachability Probabilities in Continuous-Time Markov Decision Processes. In: Proc. of QEST 2010, pp. 209–218. IEEE (2010)

    Google Scholar 

  16. Rabe, M.N., Schewe, S.: Finite Optimal Control for Time-Bounded Reachability in CTMDPs and Continuous-Time Markov Games. Acta Informatica 48(5-6), 291–315 (2011)

    Article  MathSciNet  MATH  Google Scholar 

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

  18. Zhang, L., Neuhäußer, M.R.: Model Checking Interactive Markov Chains. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 53–68. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Inria Rennes Bretagne Atlantique, France

    Nathalie Bertrand

  2. University of Liverpool, UK

    Nathalie Bertrand & Sven Schewe

Authors
  1. Nathalie Bertrand
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Sven Schewe
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, University of Warwick, CV4 7AL, Coventry, UK

    Marcin Jurdziński

  2. Business Unit Safe and Autonomous Systems, Department of Safety and Security, AIT Austrian Institute of Technology, Donau-City-Str. 1, 1220, Vienna, Austria

    Dejan Ničković

Rights and permissions

Reprints and permissions

Copyright information

© 2012 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Bertrand, N., Schewe, S. (2012). Playing Optimally on Timed Automata with Random Delays. In: Jurdziński, M., Ničković, D. (eds) Formal Modeling and Analysis of Timed Systems. FORMATS 2012. Lecture Notes in Computer Science, vol 7595. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-33365-1_5

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-33365-1_5

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-33364-4

  • Online ISBN: 978-3-642-33365-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation