On Subgame Perfect Equilibria in Turn-Based Reachability Timed Games

[en] We study multiplayer turn-based timed games with reachability objectives. In particular, we are interested in the notion of subgame perfect equilibrium (SPE). We prove that deciding the constrained existence of an SPE in this setting is EXPTIME-complete.

Research center :

CREMMI - Modélisation mathématique et informatique

Disciplines :

Computer science
Mathematics

Author, co-author :

Brihaye, Thomas ; Université de Mons > Faculté des Sciences > Service de Mathématiques effectives

Goeminne, Aline ; Université de Mons > Faculté des Sciences > Service de Mathématiques effectives

Language :

English

Title :

On Subgame Perfect Equilibria in Turn-Based Reachability Timed Games

Publication date :

01 September 2020

Event name :

18th International Conference on Formal Modeling and Analysis of Timed Systems

Event place :

Vienna, Austria

Event date :

2020

Audience :

International

Main work title :

18th International Conference, FORMATS 2020 Vienna, Austria, September 1–3, 2020 Proceedings

Publisher :

Springer

ISBN/EAN :

978-3-030-57627-1

Collection ISSN :

0302-9743

Peer reviewed :

Peer reviewed

Research unit :

S820 - Mathématiques effectives

Research institute :

R150 - Institut de Recherche sur les Systèmes Complexes

Available on ORBi UMONS :

since 14 December 2020

Statistics

Number of views

23 (7 by UMONS)

Number of downloads

0 (0 by UMONS)

More statistics

Scopus citations^®

Scopus citations^®
without self-citations

OpenCitations

OpenAlex citations

Bibliography

de Alfaro, L., Faella, M., Henzinger, T.A., Majumdar, R., Stoelinga, M.: The element of surprise in timed games. In: Amadio, R., Lugiez, D. (eds.) CONCUR 2003. LNCS, vol. 2761, pp. 144–158. Springer, Heidelberg (2003). https://doi.org/10.1007/978-3-540-45187-7 9
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). https://doi.org/10.1007/3-540-48983-5 6
Baier, C., Katoen, J.P.: Principles of Model Checking. The MIT Press, Cambridge (2008)
Behrmann, G., Cougnard, A., David, A., Fleury, E., Larsen, K.G., Lime, D.: UPPAAL-tiga: time for playing games!. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 121–125. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-73368-3 14
Bouyer, P., Brenguier, R., Markey, N.: Nash equilibria for reachability objectives in multi-player timed games. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol. 6269, pp. 192–206. Springer, Heidelberg (2010). https://doi.org/10. 1007/978-3-642-15375-4 14
Larsen, K.G., Pettersson, P., Yi, W.: Model-checking for real-time systems. In: Reichel, H. (ed.) FCT 1995. LNCS, vol. 965, pp. 62–88. Springer, Heidelberg (1995). https://doi.org/10.1007/3-540-60249-6 41
Brenguier, R.: Nash equilibria in concurrent games: application to timed games. Theses, École normale supérieure de Cachan-ENS Cachan, November 2012. https://tel.archives-ouvertes.fr/tel-00827027
Brihaye, T., Bruyère, V., Goeminne, A., Raskin, J.: Constrained existence problem for weak subgame perfect equilibria with ω-regular boolean objectives. GandALF 2018, 16–29 (2018)
Brihaye, T., Bruyère, V., Goeminne, A., Raskin, J., van den Bogaard, M.: The complexity of subgame perfect equilibria in quantitative reachability games. In: CONCUR 2019, pp. 13:1–13:16 (2019)
Bruyère, V.: Computer aided synthesis: a game-theoretic approach. In: DLT, pp. 3–35 (2017)
Cassez, F., David, A., Fleury, E., Larsen, K.G., Lime, D.: Efficient on-the-fly algorithms for the analysis of timed games. In: Abadi, M., de Alfaro, L. (eds.) CONCUR 2005. LNCS, vol. 3653, pp. 66–80. Springer, Heidelberg (2005). https://doi.org/10. 1007/11539452 9
Condurache, R., Filiot, E., Gentilini, R., Raskin, J.: The complexity of rational synthesis. In: Chatzigiannakis, I., Mitzenmacher, M., Rabani, Y., Sangiorgi, D. (eds.) ICALP 2016. LIPIcs, vol. 55, pp. 121:1–121:15. Schloss Dagstuhl-Leibniz-Zentrum für Informatik (2016)
Grädel, E., Ummels, M.: Solution concepts and algorithms for infinite multiplayer games. In: New Perspectives on Games and Interaction. vol. 4, pp. 151–178. Amsterdam University Press (2008)
Jurdziński, M., Trivedi, A.: Reachability-time games on timed automata. In: Arge, L., Cachin, C., Jurdziński, T., Tarlecki, A. (eds.) ICALP 2007. LNCS, vol. 4596, pp. 838–849. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-73420-8 72
Kwiatkowska, M., Norman, G., Parker, D.: Verification and control of turn-based probabilistic real-time games. In: The Art of Modelling Computational Systems: A Journey from Logic and Concurrency to Security and Privacy-Essays Dedicated to Catuscia Palamidessi on the Occasion of Her 60th Birthday, pp. 379–396 (2019)
Nash, J.F.: Equilibrium points in n-person games. In: PNAS, vol. 36, pp. 48–49. National Academy of Sciences (1950)
Osborne, M.: An Introduction to Game Theory. Oxford University Press, Oxford (2004)
Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: POPL, pp. 179– 190. ACM Press (1989)
Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126, 183– 235 (1994)
Ummels, M.: Rational behaviour and strategy construction in infinite multiplayer games. In: Arun-Kumar, S., Garg, N. (eds.) FSTTCS 2006. LNCS, vol. 4337, pp. 212–223. Springer, Heidelberg (2006). https://doi.org/10.1007/11944836 21