Skip to main content
SpringerLink
Log in

Reachability-Time Games on Timed Automata

(Extended Abstract)

  • Conference paper
Automata, Languages and Programming (ICALP 2007)

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

Included in the following conference series:

Abstract

In a reachability-time game, players Min and Max choose moves so that the time to reach a final state in a timed automaton is minimised or maximised, respectively. Asarin and Maler showed decidability of reachability-time games on strongly non-Zeno timed automata using a value iteration algorithm. This paper complements their work by providing a strategy improvement algorithm for the problem. It also generalizes their decidability result because the proposed strategy improvement algorithm solves reachability-time games on all timed automata. The exact computational complexity of solving reachability-time games is also established: the problem is EXPTIME-complete for timed automata with at least two clocks.

This research was supported in part by EPSRC project EP/E022030/1.

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 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.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. Abdeddaïm, Y., Asarin, E., Maler, O.: Scheduling with timed automata. Theor. Comput. Sci. 354(2), 272–300 (2006)

    Article  MATH  Google Scholar 

  2. Alur, R., Bernadsky, M., Madhusudan, P.: Optimal reachability for weighted timed games. In: Díaz, J., Karhumäki, J., Lepistö, A., Sannella, D. (eds.) ICALP 2004. LNCS, vol. 3142, pp. 122–133. Springer, Heidelberg (2004)

    Google Scholar 

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

    Article  MATH  MathSciNet  Google Scholar 

  4. Asarin, E., Maler, O.: As soon as possible: Time optimal control for timed automata. In: Vaandrager, F.W., van Schuppen, J.H. (eds.) HSCC 1999. LNCS, vol. 1569, pp. 19–30. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  5. Asarin, E., Maler, O., Pnueli, A., Sifakis, J.: Controller synthesis for timed automata. In: IFAC Symp. on System Structure and Control, pp. 469–474. Elsevier, Amsterdam (1998)

    Google Scholar 

  6. Behrmann, G., Fehnker, A., Hune, T., Larsen, K.G., Pettersson, P., Romijn, J., Vaandrager, F.W.: Minimum-cost reachability for priced timed automata. In: Di Benedetto, M.D., Sangiovanni-Vincentelli, A.L. (eds.) HSCC 2001. LNCS, vol. 2034, pp. 147–161. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  7. Bouyer, P.: Weighted timed automata: model-checking and games. Electr. Notes Theor. Comput. Sci. 158, 3–17 (2006)

    Article  Google Scholar 

  8. Bouyer, P., Brihaye, T., Bruyère, V., Raskin, J.-F.: On the optimal reachability problem on weighted timed automata. Form. Method. Syst. Des. (to appear)

    Google Scholar 

  9. Bouyer, P., Brihaye, T., Markey, N.: Improved undecidability results on weighted timed automata. Information Processing Letters 98(5), 188–194 (2006)

    Article  MathSciNet  Google Scholar 

  10. Bouyer, P., Cassez, F., Fleury, E., Larsen, K.G.: Optimal strategies in priced timed game automata. In: Lodaya, K., Mahajan, M. (eds.) FSTTCS 2004. LNCS, vol. 3328, pp. 148–160. Springer, Heidelberg (2004)

    Google Scholar 

  11. Bouyer, P., Larsen, K.G., Markey, N., Rasmussen, J.I.: Almost optimal strategies in one-clock priced timed automata. In: Arun-Kumar, S., Garg, N. (eds.) FSTTCS 2006. LNCS, vol. 4337, pp. 345–356. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  12. Brihaye, T., Henzinger, T.A., Prabhu, V.S., Raskin, J.-F.: Minimum-time reachability in timed games. In: ICALP 2007. LNCS, vol. 4596, Springer, Heidelberg (2007)

    Google Scholar 

  13. Courcoubetis, C., Yannakakis, M.: Minimum and maximum delay problems in real-time systems. Form. Method. Syst. Des. 1, 385–415 (1992)

    Article  MATH  Google Scholar 

  14. de Alfaro, L., Faella, M., Henzinger, T.A., Majumdar, R., Stoelinga, M.: The element of surprise in timed games. In: Amadio, R.M., Lugiez, D. (eds.) CONCUR 2003. LNCS, vol. 2761, pp. 144–158. Springer, Heidelberg (2003)

    Google Scholar 

  15. Henzinger, T.A., Prabhu, V.S.: Timed alternating-time temporal logic. In: Asarin, E., Bouyer, P. (eds.) FORMATS 2006. LNCS, vol. 4202, pp. 1–17. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  16. Jurdziński, M., Laroussinie, F., Sproston, J.: Model checking probabilistic timed automata with one or two clocks. In: TACAS 2007. LNCS, vol. 4424, pp. 170–184. Springer, Heidelberg (2007)

    Google Scholar 

  17. Puterman, M.L.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley, Chichester (1994)

    MATH  Google Scholar 

  18. Rasmussen, J.I., Larsen, K.G., Subramani, K.: On using priced timed automata to achieve optimal scheduling. Form. Method. Syst. Des. 29, 97–114 (2006)

    Article  MATH  Google Scholar 

  19. Vöge, J., Jurdziński, M.: A discrete strategy improvement algorithm for solving parity games. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 202–215. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, University of Warwick, UK

    Marcin Jurdziński & Ashutosh Trivedi

Authors
  1. Marcin Jurdziński
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Ashutosh Trivedi
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Lars Arge Christian Cachin Tomasz Jurdziński Andrzej Tarlecki

Rights and permissions

Reprints and permissions

Copyright information

© 2007 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Jurdziński, M., Trivedi, A. (2007). Reachability-Time Games on Timed Automata. In: Arge, L., Cachin, C., Jurdziński, T., Tarlecki, A. (eds) Automata, Languages and Programming. ICALP 2007. Lecture Notes in Computer Science, vol 4596. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-73420-8_72

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-73420-8_72

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-73419-2

  • Online ISBN: 978-3-540-73420-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation