Time Flies When Looking out of the Window: Timed Games with Window Parity Objectives

Authors James C. A. Main, Mickael Randour, Jeremy Sproston



PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2021.25.pdf
  • Filesize: 0.68 MB
  • 16 pages

Document Identifiers

Author Details

James C. A. Main
  • UMONS - Université de Mons, Belgium
Mickael Randour
  • F.R.S.-FNRS & UMONS - Université de Mons, Belgium
Jeremy Sproston
  • University of Torino, Italy

Cite AsGet BibTex

James C. A. Main, Mickael Randour, and Jeremy Sproston. Time Flies When Looking out of the Window: Timed Games with Window Parity Objectives. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 25:1-25:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.CONCUR.2021.25

Abstract

The window mechanism was introduced by Chatterjee et al. to reinforce mean-payoff and total-payoff objectives with time bounds in two-player turn-based games on graphs [Krishnendu Chatterjee et al., 2015]. It has since proved useful in a variety of settings, including parity objectives in games [Véronique Bruyère et al., 2016] and both mean-payoff and parity objectives in Markov decision processes [Thomas Brihaye et al., 2020]. We study window parity objectives in timed automata and timed games: given a bound on the window size, a path satisfies such an objective if, in all states along the path, we see a sufficiently small window in which the smallest priority is even. We show that checking that all time-divergent paths of a timed automaton satisfy such a window parity objective can be done in polynomial space, and that the corresponding timed games can be solved in exponential time. This matches the complexity class of timed parity games, while adding the ability to reason about time bounds. We also consider multi-dimensional objectives and show that the complexity class does not increase. To the best of our knowledge, this is the first study of the window mechanism in a real-time setting.

Subject Classification

ACM Subject Classification
  • Theory of computation → Formal languages and automata theory
Keywords
  • Window objectives
  • timed automata
  • timed games
  • parity games

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads

References

  1. Rajeev Alur, Costas Courcoubetis, and David L. Dill. Model-checking in dense real-time. Inf. Comput., 104(1):2-34, 1993. URL: https://doi.org/10.1006/inco.1993.1024.
  2. Rajeev Alur and David L. Dill. A theory of timed automata. Theor. Comput. Sci., 126(2):183-235, 1994. URL: https://doi.org/10.1016/0304-3975(94)90010-8.
  3. Christel Baier. Reasoning about cost-utility constraints in probabilistic models. In Mikolaj Bojanczyk, Slawomir Lasota, and Igor Potapov, editors, Reachability Problems - 9th International Workshop, RP 2015, Warsaw, Poland, September 21-23, 2015, Proceedings, volume 9328 of Lecture Notes in Computer Science, pages 1-6. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-24537-9_1.
  4. Christel Baier and Joost-Pieter Katoen. Principles of model checking. MIT Press, 2008. Google Scholar
  5. Christel Baier, Joachim Klein, Sascha Klüppelholz, and Sascha Wunderlich. Weight monitoring with linear temporal logic: complexity and decidability. In Thomas A. Henzinger and Dale Miller, editors, Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS '14, Vienna, Austria, July 14-18, 2014, pages 11:1-11:10. ACM, 2014. URL: https://doi.org/10.1145/2603088.2603162.
  6. Theodore P. Baker, John Gill, and Robert Solovay. Relativizations of the P =? NP question. SIAM J. Comput., 4(4):431-442, 1975. URL: https://doi.org/10.1137/0204037.
  7. Raphaël Berthon, Mickael Randour, and Jean-François Raskin. Threshold constraints with guarantees for parity objectives in Markov decision processes. In Ioannis Chatzigiannakis, Piotr Indyk, Fabian Kuhn, and Anca Muscholl, editors, 44th International Colloquium on Automata, Languages, and Programming, ICALP 2017, July 10-14, 2017, Warsaw, Poland, volume 80 of LIPIcs, pages 121:1-121:15. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2017. URL: https://doi.org/10.4230/LIPIcs.ICALP.2017.121.
  8. Benjamin Bordais, Shibashis Guha, and Jean-François Raskin. Expected window mean-payoff. In Arkadev Chattopadhyay and Paul Gastin, editors, 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2019, December 11-13, 2019, Bombay, India, volume 150 of LIPIcs, pages 32:1-32:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2019.32.
  9. Patricia Bouyer, Thomas Brihaye, Mickael Randour, Cédric Rivière, and Pierre Vandenhove. Decisiveness of stochastic systems and its application to hybrid models. In Jean-François Raskin and Davide Bresolin, editors, Proceedings 11th International Symposium on Games, Automata, Logics, and Formal Verification, GandALF 2020, Brussels, Belgium, September 21-22, 2020, volume 326 of EPTCS, pages 149-165, 2020. URL: https://doi.org/10.4204/EPTCS.326.10.
  10. Tomás Brázdil, Krishnendu Chatterjee, Vojtech Forejt, and Antonín Kucera. Trading performance for stability in Markov decision processes. J. Comput. Syst. Sci., 84:144-170, 2017. URL: https://doi.org/10.1016/j.jcss.2016.09.009.
  11. Tomás Brázdil, Vojtech Forejt, Antonín Kucera, and Petr Novotný. Stability in graphs and games. In Josée Desharnais and Radha Jagadeesan, editors, 27th International Conference on Concurrency Theory, CONCUR 2016, August 23-26, 2016, Québec City, Canada, volume 59 of LIPIcs, pages 10:1-10:14. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2016. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2016.10.
  12. Thomas Brihaye, Florent Delgrange, Youssouf Oualhadj, and Mickael Randour. Life is random, time is not: Markov decision processes with window objectives. Log. Methods Comput. Sci., 16(4), 2020. URL: https://lmcs.episciences.org/6975.
  13. Véronique Bruyère, Emmanuel Filiot, Mickael Randour, and Jean-François Raskin. Meet your expectations with guarantees: Beyond worst-case synthesis in quantitative games. Inf. Comput., 254:259-295, 2017. URL: https://doi.org/10.1016/j.ic.2016.10.011.
  14. Véronique Bruyère, Quentin Hautem, and Mickael Randour. Window parity games: an alternative approach toward parity games with time bounds. In Domenico Cantone and Giorgio Delzanno, editors, Proceedings of the Seventh International Symposium on Games, Automata, Logics and Formal Verification, GandALF 2016, Catania, Italy, 14-16 September 2016, volume 226 of EPTCS, pages 135-148, 2016. URL: https://doi.org/10.4204/EPTCS.226.10.
  15. Véronique Bruyère, Quentin Hautem, and Jean-François Raskin. On the complexity of heterogeneous multidimensional games. In Josée Desharnais and Radha Jagadeesan, editors, 27th International Conference on Concurrency Theory, CONCUR 2016, August 23-26, 2016, Québec City, Canada, volume 59 of LIPIcs, pages 11:1-11:15. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2016. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2016.11.
  16. Cristian S. Calude, Sanjay Jain, Bakhadyr Khoussainov, Wei Li, and Frank Stephan. Deciding parity games in quasipolynomial time. In Hamed Hatami, Pierre McKenzie, and Valerie King, editors, Proceedings of the 49th Annual ACM SIGACT Symposium on Theory of Computing, STOC 2017, Montreal, QC, Canada, June 19-23, 2017, pages 252-263. ACM, 2017. URL: https://doi.org/10.1145/3055399.3055409.
  17. Krishnendu Chatterjee, Laurent Doyen, Mickael Randour, and Jean-François Raskin. Looking at mean-payoff and total-payoff through windows. Inf. Comput., 242:25-52, 2015. URL: https://doi.org/10.1016/j.ic.2015.03.010.
  18. Krishnendu Chatterjee, Thomas A. Henzinger, and Florian Horn. Finitary winning in omega-regular games. ACM Trans. Comput. Log., 11(1):1:1-1:27, 2009. URL: https://doi.org/10.1145/1614431.1614432.
  19. Krishnendu Chatterjee, Thomas A. Henzinger, and Vinayak S. Prabhu. Timed parity games: Complexity and robustness. Log. Methods Comput. Sci., 7(4), 2011. URL: https://doi.org/10.2168/LMCS-7(4:8)2011.
  20. Luca de Alfaro, Marco Faella, Thomas A. Henzinger, Rupak Majumdar, and Mariëlle Stoelinga. The element of surprise in timed games. In Roberto M. Amadio and Denis Lugiez, editors, CONCUR 2003 - Concurrency Theory, 14th International Conference, Marseille, France, September 3-5, 2003, Proceedings, volume 2761 of Lecture Notes in Computer Science, pages 142-156. Springer, 2003. URL: https://doi.org/10.1007/978-3-540-45187-7_9.
  21. Thomas A. Henzinger and Peter W. Kopke. Discrete-time control for rectangular hybrid automata. Theor. Comput. Sci., 221(1-2):369-392, 1999. URL: https://doi.org/10.1016/S0304-3975(99)00038-9.
  22. Paul Hunter, Guillermo A. Pérez, and Jean-François Raskin. Looking at mean payoff through foggy windows. Acta Inf., 55(8):627-647, 2018. URL: https://doi.org/10.1007/s00236-017-0304-7.
  23. James C. A. Main, Mickael Randour, and Jeremy Sproston. Time flies when looking out of the window: Timed games with window parity objectives. CoRR, abs/2105.06686, 2021. URL: http://arxiv.org/abs/2105.06686.
  24. Oded Maler, Amir Pnueli, and Joseph Sifakis. On the synthesis of discrete controllers for timed systems (an extended abstract). In Ernst W. Mayr and Claude Puech, editors, STACS 95, 12th Annual Symposium on Theoretical Aspects of Computer Science, Munich, Germany, March 2-4, 1995, Proceedings, volume 900 of Lecture Notes in Computer Science, pages 229-242. Springer, 1995. URL: https://doi.org/10.1007/3-540-59042-0_76.
  25. Mickael Randour. Automated synthesis of reliable and efficient systems through game theory: A case study. In Proc. of ECCS 2012, Springer Proceedings in Complexity XVII, pages 731-738. Springer, 2013. URL: https://doi.org/10.1007/978-3-319-00395-5_90.
  26. Stéphane Le Roux, Arno Pauly, and Mickael Randour. Extending finite-memory determinacy by Boolean combination of winning conditions. In Sumit Ganguly and Paritosh K. Pandya, editors, 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2018, December 11-13, 2018, Ahmedabad, India, volume 122 of LIPIcs, pages 38:1-38:20. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2018. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2018.38.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail