Game theory; Priced timed games; Real-time systems; Arbitrary integer; Integer weights; Optimal values; Polynomial-time; Priced timed game; Real - Time system; Simple++; Target location; Timed Automata; Zero-sum game; Theoretical Computer Science; Computer Science (all); General Computer Science
Abstract :
[en] Priced timed games are two-player zero-sum games played on priced timed automata (whose locations and transitions are labeled by weights modelling the cost of spending time in a state and executing an action, respectively). The goals of the players are to minimise and maximise the cost to reach a target location, respectively. We consider priced timed games with one clock and arbitrary integer weights and show that, for an important subclass of them (the so-called simple priced timed games), one can compute, in pseudo-polynomial time, the optimal values that the players can achieve, with their associated optimal strategies. As side results, we also show that one-clock priced timed games are determined and that we can use our result on simple priced timed games to solve the more general class of so-called negative-reset-acyclic priced timed games (with arbitrary integer weights and one clock). The decidability status of the full class of priced timed games with one-clock and arbitrary integer weights still remains open.
Disciplines :
Computer science Mathematics
Author, co-author :
Brihaye, Thomas ; Université de Mons - UMONS > Faculté des Sciences > Service de Mathématiques effectives
Geeraerts, Gilles; Université libre de Bruxelles, Belgium
Haddad, Axel; Université de Mons, Belgium
Lefaucheux, Engel; Max-Planck Institute for Software Systems, Germany
Monmege, Benjamin; Aix Marseille Univ, LIS, CNRS, Marseille, France
Language :
English
Title :
ONE-CLOCK PRICED TIMED GAMES WITH NEGATIVE WEIGHTS
R150 - Institut de Recherche sur les Systèmes Complexes
Funding text :
A preliminary version of this work has been published in the proceedings of FSTTCS 2015 [BGH+15]. The research leading to these results was funded by the European Union Seventh Framework Programme (FP7/2007-2013) under Grant Agreement no601148 (CASSTING). This work was also partly supported by the Fonds de la Recherche Scientifique - FNRS under grant noT.0027.21. During part of the preparation of this article, the last author was (partially) funded by the ANR project DeLTA (ANR-16-CE40-0007) and the ANR project Ticktac (ANR-18-CE40-0015).A preliminary version of this work has been published in the proceedings of FSTTCS 2015 [BGH15]. The research leading to these results was funded by the European Union Seventh Framework Programme (FP7/2007-2013) under Grant Agreement no 601148 (CASSTING). This work was also partly supported by the Fonds de la Recherche Scientifique-FNRS under grant no T.0027.21. During part of the preparation of this article, the last author was (partially) funded by the ANR project DeLTA (ANR-16-CE40-0007) and the ANR project Ticktac (ANR-18-CE40-0015).
[ABM04] Rajeev Alur, Mikhail Bernadsky, and P. Madhusudan. Optimal reachability for weighted timed games. In Proceedings of the 31st International Colloquium on Automata, Languages and Programming (ICALP’04), volume 3142 of Lecture Notes in Computer Science, pages 122–133. Springer, 2004. doi:10.1007/978-3-540-27836-8_13.
[AD94] Rajeev Alur and David L. Dill. A theory of timed automata. Theoretical Computer Science, 126(2):183–235, 1994. doi:10.1016/0304-3975(94)90010-8.
[ALTP04] Rajeev Alur, Salvatore La Torre, and George J. Pappas. Optimal paths in weighted timed automata. Theoretical Computer Science, 318(3):297–322, 2004. doi:10.1016/j.tcs.2003.10. 038.
[BBBR07] Patricia Bouyer, Thomas Brihaye, Véronique Bruyère, and Jean-François Raskin. On the optimal reachability problem of weighted timed automata. Formal Methods in System Design, 31(2):135– 175, 2007. doi:10.1007/s10703-007-0035-4.
[BBC06] Patricia Bouyer, Thomas Brihaye, and Fabrice Chevalier. Control in o-minimal hybrid systems. In Proceedings of the Twenty-first Annual IEEE Symposium on Logic In Computer Science (LICS’06), pages 367–378. IEEE Computer Society Press, 2006. doi:10.1109/LICS.2006.22.
[BBJ+ 08] Patricia Bouyer, Thomas Brihaye, Marcin Jurdziński, Ranko Lazić, and Michal Rutkowski. Average-price and reachability-price games on hybrid automata with strong resets. In Proceedings of the 6th international conference on Formal Modeling and Analysis of Timed Systems (FOR-MATS’08), volume 5215 of Lecture Notes in Computer Science, pages 63–77. Springer, 2008. doi:10.1007/978-3-540-85778-5_6.
[BBM06] Patricia Bouyer, Thomas Brihaye, and Nicolas Markey. Improved undecidability results on weighted timed automata. Information Processing Letters, 98(5):188–194, 2006. doi:10.1016/j. ipl.2006.01.012.
[BBR05] Thomas Brihaye, Véronique Bruyère, and Jean-François Raskin. On optimal timed strategies. In Proceedings of the Third international conference on Formal Modeling and Analysis of Timed Systems (FORMATS’05), volume 3829 of Lecture Notes in Computer Science, pages 49–64. Springer, 2005. doi:10.1007/11603009_5.
[BCFL04] Patricia Bouyer, Franck Cassez, Emmanuel Fleury, and Kim G. Larsen. Optimal strategies in priced timed game automata. In Proceedings of the 24th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS’04), volume 3328 of Lecture Notes in Computer Science, pages 148–160. Springer, 2004. doi:10.1007/978-3-540-30538-5_13.
[BCJ09] J. Berendsen, T. Chen, and D. Jansen. Undecidability of cost-bounded reachability in priced probabilistic timed automata. In Theory and Applications of Models of Computation, volume 5532 of Lecture Notes in Computer Science, pages 128–137. Springer, 2009. doi:10.1007/978-3-642-02017-9_16.
[BCR14] Romain Brenguier, Franck Cassez, and Jean-François Raskin. Energy and mean-payoff timed games. In Proceedings of the 17th International Conference on Hybrid Systems: Computation and Control, HSCC’14, Berlin, Germany, April 15-17, pages 283–292. Association for Computing Machinery, 2014. doi:10.1145/2562059.2562116.
[BDG+ 16] Thomas Brihaye, Amit Kumar Dhar, Gilles Geeraerts, Axel Haddad, and Benjamin Monmege. Efficient energy distribution in a smart grid using multi-player games. In Thomas Brihaye, Benoît Delahaye, Nicolas Markey, and Jiří Srba, editors, Proceedings of the Cassting Workshop on Games for the Synthesis of Complex Systems (Cassting’16) and the 3rd International Workshop on Synthesis of Complex Parameters (SynCoP’16), volume 220, pages 1–12, Eindhoven, Netherlands, April 2016. EPTCS. doi:10.4204/EPTCS.220.1.
[BFH+ 01] Gerd Behrmann, Ansgar Fehnker, Thomas Hune, Kim G. Larsen, Judi Romijn, and Frits W. Vaandrager. Minimum-cost reachability for priced timed automata. In Proceedings of the 4th International Workshop on Hybrid Systems: Computation and Control (HSCC’01), volume 2034 of Lecture Notes in Computer Science, pages 147–161. Springer, 2001. doi:10.1007/3-540-45351-2_15.
[BGH+ 15] Thomas Brihaye, Gilles Geeraerts, Axel Haddad, Engel Lefaucheux, and Benjamin Monmege. Simple priced timed games are not that simple. In Prahladh Harsha and G. Ramalingam, editors, Proceedings of the 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS’15), volume 45 of Leibniz International Proceedings in Informatics (LIPIcs), pages 278–292. Schloss Dagstuhl–Leibniz-Zentrum für Informatik, December 2015. doi:10.4230/LIPIcs.FSTTCS.2015.278.
[BGHM15] Thomas Brihaye, Gilles Geeraerts, Axel Haddad, and Benjamin Monmege. To reach or not to reach? Efficient algorithms for total-payoff games. In Luca Aceto and David de Frutos Escrig, editors, Proceedings of the 26th International Conference on Concurrency Theory (CONCUR’15), volume 42 of LIPIcs, pages 297–310. Schloss Dagstuhl–Leibniz-Zentrum für Informatik, September 2015. doi:10.4230/LIPIcs.CONCUR.2015.297.
[BGHM16] Thomas Brihaye, Gilles Geeraerts, Axel Haddad, and Benjamin Monmege. Pseudopolynomial iterative algorithm to solve total-payoff games and min-cost reachability games. Acta Informatica, 2016. doi:10.1007/s00236-016-0276-z.
[BGK+ 14] Thomas Brihaye, Gilles Geeraerts, Shankara Narayanan Krishna, Lakshmi Manasa, Benjamin Monmege, and Ashutosh Trivedi. Adding Negative Prices to Priced Timed Games. In Proceedings of the 25th International Conference on Concurrency Theory (CONCUR’13), volume 8704 of Lecture Notes in Computer Science, pages 560–575. Springer, 2014. doi: 10.1007/978-3-662-44584-6_38.
[BGMR17] Damien Busatto-Gaston, Benjamin Monmege, and Pierre-Alain Reynier. Optimal reachability in divergent weighted timed games. In Javier Esparza and Andrzej S. Murawski, editors, Proceedings of the 20th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS’17), volume 10203 of Lecture Notes in Computer Science, pages 162–178, Uppsala, Sweden, April 2017. Springer. doi:10.1007/978-3-662-54458-7_10.
[BJM14] Patricia Bouyer, Samy Jaziri, and Nicolas Markey. On the value problem in weighted timed games. Research Report LSV-14-12, Laboratoire Spécification et Vérification, ENS Cachan, France, October 2014. 24 pages. URL: http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2014-12.pdf.
[BLMR06] Patricia Bouyer, Kim G. Larsen, Nicolas Markey, and Jacob Illum Rasmussen. Almost optimal strategies in one-clock priced timed games. In Proceedings of the 26th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS’06), volume 4337 of Lecture Notes in Computer Science, pages 345–356. Springer, 2006. doi:10.1007/11944836_32.
[Bou15] Patricia Bouyer. On the optimal reachability problem in weighted timed automata and games. In Proceedings of the 7th Workshop on Non-Classical Models of Automata and Applications (NCMA’15), volume 318 of books@ocg.at, pages 11–36. Austrian Computer Society, 2015.
[dAHM01] Luca de Alfaro, Thomas A. Henzinger, and Rupak Majumdar. Symbolic algorithms for infinite-state games. In Proceedings of the 12th International Conference on Concurrecy Theory (CON-CUR’01), volume 2154 of Lecture Notes in Computer Science, pages 536–550. Springer, 2001. doi:10.1007/3-540-44685-0_36.
[FIJS20] John Fearnley, Rasmus Ibsen-Jensen, and Rahul Savani. One-clock priced timed games are PSPACE-hard. In Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Sciences (LICS’20), pages 397–409. ACM, 2020. doi:10.1145/3373718.3394772.
[HIJM13] Thomas Dueholm Hansen, Rasmus Ibsen-Jensen, and Peter Bro Miltersen. A faster algorithm for solving one-clock priced timed games. In Proceedings of the 24th International Conference on Concurrency Theory (CONCUR’13), volume 8052 of Lecture Notes in Computer Science, pages 531–545. Springer, 2013. doi:10.1007/978-3-642-40184-8_37.
[Mar75] Donald A. Martin. Borel determinacy. Annals of Mathematics, 102(2):363–371, 1975. doi: 10.2307/1971035.
[MPS95] Oded Maler, Amir Pnueli, and Joseph Sifakis. On the synthesis of discrete controllers for timed systems. In Proceedings of the 12th Annual Symposium on Theoretical Aspects of Computer Science (STACS’95), volume 900 of Lecture Notes in Computer Science, pages 229–242. Springer, 1995. doi:10.1007/3-540-59042-0_76.
[Rut11] Michal Rutkowski. Two-player reachability-price games on single-clock timed automata. In Proceedings of the 9th Workshop on Quantitative Aspects of Programming Languages (QAPL’11), volume 57 of Electronic Proceedings in Theoretical Computer Science, pages 31–46, 2011.
[WT97] Howard Wong-Toi. The synthesis of controllers for linear hybrid automata. In Proceedings of the 36th IEEE Conference on Decision and Control (CDC’97), pages 4607–4612. IEEE Computer Society Press, 1997. doi:10.1109/CDC.1997.649708.
