Skip to main content

2017 | OriginalPaper | Buchkapitel

Admissible Strategies in Timed Games

verfasst von : Nicolas Basset, Jean-François Raskin, Ocan Sankur

Erschienen in: Models, Algorithms, Logics and Tools

Verlag: Springer International Publishing

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

In this paper, we study the notion of admissibility in timed games. First, we show that admissible strategies may not exist in timed games with a continuous semantics of time, even for safety objectives. Second, we show that the discrete time semantics of timed games is better behaved w.r.t. admissibility: the existence of admissible strategies is guaranteed in that semantics. Third, we provide symbolic algorithms to solve the model-checking problem under admissibility and the assume-admissible synthesis problem for real-time non-zero sum n-player games for safety objectives.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Literatur
2.
Zurück zum Zitat Asarin, E., Maler, O.: As soon as possible: time optimal control for timed automata. In: Vaandrager, F.W., Schuppen, J.H. (eds.) HSCC 1999. LNCS, vol. 1569, pp. 19–30. Springer, Heidelberg (1999). doi:10.1007/3-540-48983-5_6 CrossRef Asarin, E., Maler, O.: As soon as possible: time optimal control for timed automata. In: Vaandrager, F.W., Schuppen, J.H. (eds.) HSCC 1999. LNCS, vol. 1569, pp. 19–30. Springer, Heidelberg (1999). doi:10.​1007/​3-540-48983-5_​6 CrossRef
3.
Zurück zum Zitat Baier, C., Katoen, J.: Principles of Model Checking. MIT Press, Cambridge (2008)MATH Baier, C., Katoen, J.: Principles of Model Checking. MIT Press, Cambridge (2008)MATH
4.
Zurück zum Zitat Basset, N., Geeraerts, G., Raskin, J., Sankur, O.: Admissibility in concurrent games. CoRR, abs/1702.06439 (2017) Basset, N., Geeraerts, G., Raskin, J., Sankur, O.: Admissibility in concurrent games. CoRR, abs/1702.06439 (2017)
5.
Zurück zum Zitat 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). doi:10.1007/978-3-540-73368-3_14 CrossRef 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). doi:10.​1007/​978-3-540-73368-3_​14 CrossRef
6.
Zurück zum Zitat Bengtsson, J., Yi, W.: Timed automata: semantics, algorithms and tools. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) ACPN 2003. LNCS, vol. 3098, pp. 87–124. Springer, Heidelberg (2004). doi:10.1007/978-3-540-27755-2_3 CrossRef Bengtsson, J., Yi, W.: Timed automata: semantics, algorithms and tools. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) ACPN 2003. LNCS, vol. 3098, pp. 87–124. Springer, Heidelberg (2004). doi:10.​1007/​978-3-540-27755-2_​3 CrossRef
8.
Zurück zum Zitat Bouyer, P., Brenguier, R., Markey, N.: Computing equilibria in two-player timed games via turn-based finite games. In: Chatterjee, K., Henzinger, T.A. (eds.) FORMATS 2010. LNCS, vol. 6246, pp. 62–76. Springer, Heidelberg (2010). doi:10.1007/978-3-642-15297-9_7 CrossRef Bouyer, P., Brenguier, R., Markey, N.: Computing equilibria in two-player timed games via turn-based finite games. In: Chatterjee, K., Henzinger, T.A. (eds.) FORMATS 2010. LNCS, vol. 6246, pp. 62–76. Springer, Heidelberg (2010). doi:10.​1007/​978-3-642-15297-9_​7 CrossRef
9.
Zurück zum Zitat 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). doi:10.1007/978-3-642-15375-4_14 CrossRef 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). doi:10.​1007/​978-3-642-15375-4_​14 CrossRef
10.
Zurück zum Zitat Brenguier, R., Clemente, L., Hunter, P., Pérez, G.A., Randour, M., Raskin, J.-F., Sankur, O., Sassolas, M.: Non-zero sum games for reactive synthesis. In: Dediu, A.-H., Janoušek, J., Martín-Vide, C., Truthe, B. (eds.) LATA 2016. LNCS, vol. 9618, pp. 3–23. Springer, Cham (2016). doi:10.1007/978-3-319-30000-9_1 CrossRef Brenguier, R., Clemente, L., Hunter, P., Pérez, G.A., Randour, M., Raskin, J.-F., Sankur, O., Sassolas, M.: Non-zero sum games for reactive synthesis. In: Dediu, A.-H., Janoušek, J., Martín-Vide, C., Truthe, B. (eds.) LATA 2016. LNCS, vol. 9618, pp. 3–23. Springer, Cham (2016). doi:10.​1007/​978-3-319-30000-9_​1 CrossRef
11.
Zurück zum Zitat Brenguier, R., Pérez, G.A., Raskin, J., Sankur, O.: Admissibility in quantitative graph games. In: 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2016, Chennai, India, 13–15 December 2016. LIPIcs, vol. 65, pp. 42:1–42:14. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2016) Brenguier, R., Pérez, G.A., Raskin, J., Sankur, O.: Admissibility in quantitative graph games. In: 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2016, Chennai, India, 13–15 December 2016. LIPIcs, vol. 65, pp. 42:1–42:14. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2016)
12.
Zurück zum Zitat Brenguier, R., Raskin, J.-F., Sankur, O.: Assume-admissible synthesis. In: Proceedings of the CONCUR. LIPIcs, vol. 42, pp. 100–113. Schloss Dagstuhl-LZI (2015) Brenguier, R., Raskin, J.-F., Sankur, O.: Assume-admissible synthesis. In: Proceedings of the CONCUR. LIPIcs, vol. 42, pp. 100–113. Schloss Dagstuhl-LZI (2015)
13.
Zurück zum Zitat Brenguier, R., Raskin, J.-F., Sassolas, M.: The complexity of admissibility in omega-regular games. In: Proceedings of the CSL-LICS, pp. 23:1–23:10. ACM (2014) Brenguier, R., Raskin, J.-F., Sassolas, M.: The complexity of admissibility in omega-regular games. In: Proceedings of the CSL-LICS, pp. 23:1–23:10. ACM (2014)
14.
Zurück zum Zitat Brihaye, T., Bruyere, V., Meunier, N., Raskin, J.-F.: Weak subgame perfect equilibria and their application to quantitative reachability. In: Kreutzer, S. (ed.) 24th EACSL Annual Conference on Computer Science Logic (CSL 2015), Leibniz International Proceedings in Informatics (LIPIcs), vol. 41, pp. 504–518. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Dagstuhl (2015) Brihaye, T., Bruyere, V., Meunier, N., Raskin, J.-F.: Weak subgame perfect equilibria and their application to quantitative reachability. In: Kreutzer, S. (ed.) 24th EACSL Annual Conference on Computer Science Logic (CSL 2015), Leibniz International Proceedings in Informatics (LIPIcs), vol. 41, pp. 504–518. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Dagstuhl (2015)
15.
Zurück zum Zitat 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). doi:10.1007/11603009_5 CrossRef 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). doi:10.​1007/​11603009_​5 CrossRef
16.
Zurück zum Zitat Brihaye, T., Henzinger, T.A., Prabhu, V.S., Raskin, J.-F.: Minimum-time reachability in timed games. In: Arge, L., Cachin, C., Jurdziński, T., Tarlecki, A. (eds.) ICALP 2007. LNCS, vol. 4596, pp. 825–837. Springer, Heidelberg (2007). doi:10.1007/978-3-540-73420-8_71 CrossRef Brihaye, T., Henzinger, T.A., Prabhu, V.S., Raskin, J.-F.: Minimum-time reachability in timed games. In: Arge, L., Cachin, C., Jurdziński, T., Tarlecki, A. (eds.) ICALP 2007. LNCS, vol. 4596, pp. 825–837. Springer, Heidelberg (2007). doi:10.​1007/​978-3-540-73420-8_​71 CrossRef
17.
Zurück zum Zitat 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., Alfaro, L. (eds.) CONCUR 2005. LNCS, vol. 3653, pp. 66–80. Springer, Heidelberg (2005). doi:10.1007/11539452_9 CrossRef 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., Alfaro, L. (eds.) CONCUR 2005. LNCS, vol. 3653, pp. 66–80. Springer, Heidelberg (2005). doi:10.​1007/​11539452_​9 CrossRef
19.
21.
Zurück zum Zitat Condurache, R., Filiot, E., Gentilini, R., Raskin, J.: The complexity of rational synthesis. In: 43rd International Colloquium on Automata, Languages, Programming, ICALP 2016, 11–15 July 2016, Rome, Italy. LIPIcs, vol. 55, pp. 121:1–121:15. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2016) Condurache, R., Filiot, E., Gentilini, R., Raskin, J.: The complexity of rational synthesis. In: 43rd International Colloquium on Automata, Languages, Programming, ICALP 2016, 11–15 July 2016, Rome, Italy. LIPIcs, vol. 55, pp. 121:1–121:15. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2016)
22.
25.
Zurück zum Zitat Jensen, P.G., Larsen, K.G., Srba, J.: Real-time strategy synthesis for timed-arc petri net games via discretization. In: Bošnački, D., Wijs, A. (eds.) SPIN 2016. LNCS, vol. 9641, pp. 129–146. Springer, Cham (2016). doi:10.1007/978-3-319-32582-8_9 CrossRef Jensen, P.G., Larsen, K.G., Srba, J.: Real-time strategy synthesis for timed-arc petri net games via discretization. In: Bošnački, D., Wijs, A. (eds.) SPIN 2016. LNCS, vol. 9641, pp. 129–146. Springer, Cham (2016). doi:10.​1007/​978-3-319-32582-8_​9 CrossRef
26.
Zurück zum Zitat Kupferman, O., Perelli, G., Vardi, M.Y.: Synthesis with rational environments. In: Bulling, N. (ed.) EUMAS 2014. LNCS (LNAI), vol. 8953, pp. 219–235. Springer, Cham (2015). doi:10.1007/978-3-319-17130-2_15 Kupferman, O., Perelli, G., Vardi, M.Y.: Synthesis with rational environments. In: Bulling, N. (ed.) EUMAS 2014. LNCS (LNAI), vol. 8953, pp. 219–235. Springer, Cham (2015). doi:10.​1007/​978-3-319-17130-2_​15
27.
Zurück zum Zitat Maler, O., Pnueli, A., Sifakis, J.: On the synthesis of discrete controllers for timed systems. In: Mayr, E.W., Puech, C. (eds.) STACS 1995. LNCS, vol. 900, pp. 229–242. Springer, Heidelberg (1995). doi:10.1007/3-540-59042-0_76 CrossRef Maler, O., Pnueli, A., Sifakis, J.: On the synthesis of discrete controllers for timed systems. In: Mayr, E.W., Puech, C. (eds.) STACS 1995. LNCS, vol. 900, pp. 229–242. Springer, Heidelberg (1995). doi:10.​1007/​3-540-59042-0_​76 CrossRef
28.
Zurück zum Zitat Mogavero, F., Murano, A., Vardi, M.Y.: Reasoning about strategies. In: Proceedings of the FSTTCS. LIPIcs, vol. 8, pp. 133–144. Schloss Dagstuhl - LZI (2010) Mogavero, F., Murano, A., Vardi, M.Y.: Reasoning about strategies. In: Proceedings of the FSTTCS. LIPIcs, vol. 8, pp. 133–144. Schloss Dagstuhl - LZI (2010)
29.
Zurück zum Zitat 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). doi:10.1007/11944836_21 CrossRef 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). doi:10.​1007/​11944836_​21 CrossRef
Metadaten
Titel
Admissible Strategies in Timed Games
verfasst von
Nicolas Basset
Jean-François Raskin
Ocan Sankur
Copyright-Jahr
2017
DOI
https://doi.org/10.1007/978-3-319-63121-9_20