Advertisement

Reachability-Time Games on Timed Automata

(Extended Abstract)
  • Marcin Jurdziński
  • Ashutosh Trivedi
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 4596)

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.

Keywords

Strategy Improvement Optimality Equation Positional Strategy Reachability Problem Time Automaton 
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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Abdeddaïm, Y., Asarin, E., Maler, O.: Scheduling with timed automata. Theor. Comput. Sci. 354(2), 272–300 (2006)zbMATHCrossRefGoogle Scholar
  2. 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. 3.
    Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183–235 (1994)zbMATHCrossRefMathSciNetGoogle Scholar
  4. 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)CrossRefGoogle Scholar
  5. 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. 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)CrossRefGoogle Scholar
  7. 7.
    Bouyer, P.: Weighted timed automata: model-checking and games. Electr. Notes Theor. Comput. Sci. 158, 3–17 (2006)CrossRefGoogle Scholar
  8. 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. 9.
    Bouyer, P., Brihaye, T., Markey, N.: Improved undecidability results on weighted timed automata. Information Processing Letters 98(5), 188–194 (2006)CrossRefMathSciNetGoogle Scholar
  10. 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. 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)CrossRefGoogle Scholar
  12. 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. 13.
    Courcoubetis, C., Yannakakis, M.: Minimum and maximum delay problems in real-time systems. Form. Method. Syst. Des. 1, 385–415 (1992)zbMATHCrossRefGoogle Scholar
  14. 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. 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)CrossRefGoogle Scholar
  16. 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. 17.
    Puterman, M.L.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley, Chichester (1994)zbMATHGoogle Scholar
  18. 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)zbMATHCrossRefGoogle Scholar
  19. 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)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2007

Authors and Affiliations

  • Marcin Jurdziński
    • 1
  • Ashutosh Trivedi
    • 1
  1. 1.Department of Computer Science, University of WarwickUK

Personalised recommendations