Adding Negative Prices to Priced Timed Games

  • Thomas Brihaye
  • Gilles Geeraerts
  • Shankara Narayanan Krishna
  • Lakshmi Manasa
  • Benjamin Monmege
  • Ashutosh Trivedi
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8704)


Priced timed games (PTGs) are two-player zero-sum games played on the infinite graph of configurations of priced timed automata where two players take turns to choose transitions in order to optimize cost to reach target states. Bouyer et al. and Alur, Bernadsky, and Madhusudan independently proposed algorithms to solve PTGs with nonnegative prices under certain divergence restriction over prices. Brihaye, Bruyère, and Raskin later provided a justification for such a restriction by showing the undecidability of the optimal strategy synthesis problem in the absence of this divergence restriction. This problem for PTGs with one clock has long been conjectured to be in polynomial time, however the current best known algorithm, by Hansen, Ibsen-Jensen, and Miltersen, is exponential. We extend this picture by studying PTGs with both negative and positive prices. We refine the undecidability results for optimal strategy synthesis problem, and show undecidability for several variants of optimal reachability cost objectives including reachability cost, time-bounded reachability cost, and repeated reachability cost objectives. We also identify a subclass with bi-valued price-rates and give a pseudo-polynomial (polynomial when prices are nonnegative) algorithm to partially answer the conjecture on the complexity of one-clock PTGs.


Polynomial Time Hybrid Automaton Game Graph Counter Machine Clock Constraint 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    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)CrossRefGoogle Scholar
  2. 2.
    Alur, R., Dill, D.L.: A theory of timed automata. TCS 126(2), 183–235 (1994)CrossRefzbMATHMathSciNetGoogle Scholar
  3. 3.
    Alur, R., La Torre, S., Pappas, G.J.: Optimal paths in weighted timed automata. TCS 318(3), 297–322 (2004)CrossRefzbMATHGoogle Scholar
  4. 4.
    Behrmann, G., Fehnker, A., Hune, T., Larsen, K.G., Pettersson, P., Romijn, J.M.T., 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)Google Scholar
  5. 5.
    Berendsen, J., Chen, T., Jansen, D.N.: Undecidability of cost-bounded reachability in priced probabilistic timed automata. In: Chen, J., Cooper, S.B. (eds.) TAMC 2009. LNCS, vol. 5532, pp. 128–137. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  6. 6.
    Bouyer, P., Brihaye, T., Bruyère, V., Raskin, J.-F.: On the optimal reachability problem of weighted timed automata. FMSD 31(2), 135–175 (2007)zbMATHGoogle Scholar
  7. 7.
    Bouyer, P., Brihaye, T., Markey, N.: Improved undecidability results on weighted timed automata. IPL 98(5), 188–194 (2006)CrossRefzbMATHMathSciNetGoogle Scholar
  8. 8.
    Bouyer, P., Brinksma, E., Larsen, K.G.: Optimal infinite scheduling for multi-priced timed automata. FMSD 32(1), 3–23 (2008)zbMATHGoogle Scholar
  9. 9.
    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
  10. 10.
    Bouyer, P., Larsen, K.G., Markey, N., Rasmussen, J.I.: Almost optimal strategies in one-clock priced timed games. In: Arun-Kumar, S., Garg, N. (eds.) FSTTCS 2006. LNCS, vol. 4337, pp. 345–356. Springer, Heidelberg (2006)Google Scholar
  11. 11.
    Brihaye, T., Bruyère, V., Raskin, J.-F.: On optimal timed strategies. In: Pettersson, P., Yi, W. (eds.) FORMATS 2005. LNCS, vol. 3829, pp. 49–64. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  12. 12.
    Brihaye, T., Doyen, L., Geeraerts, G., Ouaknine, J., Raskin, J.-F., Worrell, J.: Time-bounded reachability for monotonic hybrid automata: Complexity and fixed points. In: Van Hung, D., Ogawa, M. (eds.) ATVA 2013. LNCS, vol. 8172, pp. 55–70. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  13. 13.
    Brihaye, T., Geeraerts, G., Krishna, S.N., Manasa, L., Monmege, B., Trivedi, A.: Reachability-cost games with negative weights. Technical report (2014),
  14. 14.
    Brihaye, T., Geeraerts, G., Monmege, B.: Reachability-cost games with negative weights. Technical report (2014),
  15. 15.
    Hansen, T.D., Ibsen-Jensen, R., Miltersen, P.B.: A faster algorithm for solving one-clock priced timed games. In: D’Argenio, P.R., Melgratti, H. (eds.) CONCUR 2013 – Concurrency Theory. LNCS, vol. 8052, pp. 531–545. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  16. 16.
    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)CrossRefGoogle Scholar
  17. 17.
    Minsky, M.L.: Computation: Finite and infinite machines. Prentice-Hall, Inc. (1967)Google Scholar
  18. 18.
    Ouaknine, J., Worrell, J.: Towards a theory of time-bounded verification. In: Abramsky, S., Gavoille, C., Kirchner, C., Meyer auf der Heide, F., Spirakis, P.G. (eds.) ICALP 2010. LNCS, vol. 6199, pp. 22–37. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  19. 19.
    Ramadge, P.J., Wonham, W.M.: The control of discrete event systems. IEEE 77, 81–98 (1989)CrossRefGoogle Scholar
  20. 20.
    Rutkowski, M.: Two-player reachability-price games on single-clock timed automata. In: QAPL 2011. EPTCS, vol. 57, pp. 31–46 (2011)Google Scholar
  21. 21.
    Zwick, U., Paterson, M.: The complexity of mean payoff games on graphs. TCS 158, 343–359 (1996)CrossRefzbMATHMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2014

Authors and Affiliations

  • Thomas Brihaye
    • 1
  • Gilles Geeraerts
    • 2
  • Shankara Narayanan Krishna
    • 3
  • Lakshmi Manasa
    • 3
  • Benjamin Monmege
    • 2
  • Ashutosh Trivedi
    • 3
  1. 1.Université de MonsBelgium
  2. 2.Université libre de BruxellesBelgium
  3. 3.IIT BombayIndia

Personalised recommendations